text:
import .lovelib

/-! # LoVe Exercise 3: Forward Proofs -/

set_option pp.beta true
set_option pp.generalized_field_notation false

namespace LoVe

/-! ## Question 1: Connectives and Quantifiers

1.1. Supply structured proofs of the following lemmas. -/

lemma I (a : Prop) :
  a → a :=
sorry

lemma K (a b : Prop) :
  a → b → b :=
sorry

lemma C (a b c : Prop) :
  (a → b → c) → b → a → c :=
sorry

lemma proj_1st (a : Prop) :
  a → a → a :=
sorry

/-! Please give a different answer than for `proj_1st`. -/

lemma proj_2nd (a : Prop) :
  a → a → a :=
sorry

lemma some_nonsense (a b c : Prop) :
  (a → b → c) → a → (a → c) → b → c :=
sorry

/-! 1.2. Supply a structured proof of the contraposition rule. -/

lemma contrapositive (a b : Prop) :
  (a → b) → ¬ b → ¬ a :=
sorry

/-! 1.3. Supply a structured proof of the distributivity of `∀` over `∧`. -/

lemma forall_and {α : Type} (p q : α → Prop) :
  (∀x, p x ∧ q x) ↔ (∀x, p x) ∧ (∀x, q x) :=
sorry

/-! 1.4 (**optional**). Reuse, if possible, the lemma `forall_and` from question
1.3 to prove the following instance of the lemma. -/

lemma forall_and_inst {α : Type} (r s : α → α → Prop) :
  (∀x, r x x ∧ s x x) ↔ (∀x, r x x) ∧ (∀x, s x x) :=
sorry

/-! 1.5. Supply a structured proof of the following property, which can be used
pull a `∀`-quantifier past an `∃`-quantifier. -/

lemma forall_exists_of_exists_forall {α : Type} (p : α → α → Prop) :
  (∃x, ∀y, p x y) → (∀y, ∃x, p x y) :=
sorry

/-! ## Question 2: Chain of Equalities

2.1. Write the following proof using `calc`.

      (a + b) * (a + b)
    = a * (a + b) + b * (a + b)
    = a * a + a * b + b * a + b * b
    = a * a + a * b + a * b + b * b
    = a * a + 2 * a * b + b * b

Hint: You might need the tactics `simp` and `cc` and the lemmas `mul_add`,
`add_mul`, and `two_mul`. -/

lemma binomial_square (a b : ℕ) :
  (a + b) * (a + b) = a * a + 2 * a * b + b * b :=
sorry

/-! 2.2 (**optional**). Prove the same argument again, this time as a structured
proof, with `have` steps corresponding to the `calc` equations. Try to reuse as
much of the above proof idea as possible, proceeding mechanically. -/

lemma binomial_square₂ (a b : ℕ) :
  (a + b) * (a + b) = a * a + 2 * a * b + b * b :=
sorry

/-! 2.3. Prove the same lemma again, this time using tactics. -/

lemma binomial_square₃ (a b : ℕ) :
  (a + b) * (a + b) = a * a + 2 * a * b + b * b :=
begin
  sorry
end

/-! ## Question 3 (**optional**): One-Point Rules

3.1 (**optional**). Prove that the following wrong formulation of the one-point
rule for `∀` is inconsistent, using a structured proof. -/

axiom forall.one_point_wrong {α : Type} {t : α} {p : α → Prop} :
  (∀x : α, x = t ∧ p x) ↔ p t

lemma proof_of_false :
  false :=
sorry

/-! 3.2 (**optional**). Prove that the following wrong formulation of the
one-point rule for `∃` is inconsistent, using a tactical or structured proof. -/

axiom exists.one_point_wrong {α : Type} {t : α} {p : α → Prop} :
  (∃x : α, x = t → p x) ↔ p t

lemma proof_of_false₂ :
  false :=
sorry

end LoVe

author: blanchette


import cohomology
import G_module.hom

variables {G : Type*} [group G]
variables {M : Type*}[add_comm_group M] [G_module G M]
variables {N : Type*} [add_comm_group N] [G_module G N]
variables {n : ℕ}
def cochain.map (f : M →[G] N) : cochain n G M → cochain n G N :=
λ b c, f (b c)

theorem d_map (f : M →[G] N) (c : cochain n G M) :
cochain.map f (d.to_fun c) = d.to_fun (cochain.map f c) :=
begin
  ext gs,
  unfold d.to_fun,
  unfold cochain.map,
  rw f.map_add,
  rw f.map_smul,
  rw f.map_sum,
  congr',
  ext x,
  show (f.f) _ = _,
  exact add_monoid_hom.map_gsmul _ _ _,
end

def cocycle.map (f : M →[G] N) : cocycle n G M → cocycle n G N :=
λ c, ⟨cochain.map f c.1, begin
    show d.to_fun (cochain.map f c.val) = 0,
    rw ←d_map,
    have h0 : d.to_fun c.val = 0,
      exact c.property,
    rw h0,
    ext i,
    apply add_monoid_hom.map_zero,
  end⟩

def coboundary.map (f : M →[G] N) : coboundary n G M → coboundary n G N:=
 λ c, ⟨cochain.map f c.1, begin
  unfold coboundary,
unfold add_group_hom.range,
unfold add_group_hom.map,
dsimp,
rw set.mem_image,
have h0: ∃ (x : cochain n G M), d.to_fun x = c.val,
sorry,
rcases h0 with ⟨ y, hy1⟩,
use cochain.map f y,
split,
trivial,
rw <-hy1,
exact (d_map f y).symm,
  end⟩

def cochain.hom (f : M →[G] N) : cochain n G M →+ cochain n G N :=
{ to_fun := cochain.map f,
  map_zero' := begin unfold cochain.map, ext, apply add_monoid_hom.map_zero, end,
  map_add' := begin intros, unfold cochain.map, funext, apply add_monoid_hom.map_add,end }

lemma cocycle.map_incl (f : M →[G] N): set.image (cochain.hom f).to_fun (cohomology n G M).top.carrier ⊆ (cohomology n G N).top.carrier:= begin
unfold cochain.hom,
unfold cohomology,
unfold set.image,
intros  x hx,
show d.to_fun x = 0,
cases hx with a ha,
have h2: cochain.map f a=x, exact and.right ha,
rw <-h2,
rw ←d_map,
have h0 : d.to_fun a = 0,
exact and.left ha,
rw h0,
ext i,
apply add_monoid_hom.map_zero,
end

lemma coboundary.map_incl (f : M →[G] N): set.image (cochain.hom f).to_fun (cohomology n G M).bottom.carrier ⊆ (cohomology n G N).bottom.carrier:=
begin
unfold cochain.hom,
unfold cohomology,
unfold set.image,
dsimp,
rintros x ⟨ a, ha1, h2⟩ ,
rw <-h2,

unfold coboundary,
unfold add_group_hom.range,
unfold add_group_hom.map,
dsimp,
rw set.mem_image,

unfold coboundary at ha1,
unfold add_group_hom.range at ha1,
unfold add_group_hom.map at ha1,
dsimp at ha1,
rw set.mem_image at ha1,
rcases ha1 with ⟨ y, hy1, hy2⟩,
use cochain.map f y,
split,
trivial,
rw <-hy2,
exact (d_map f y).symm,
end

def cohomology.map (f : M →[G] N) : cohomology n G M →+ cohomology n G N:=
add_subquotient.to_add_monoid_hom (cocycle.map_incl f) (coboundary.map_incl f)

/-

Need:

If M → P is a G-module map then there's an induced map H^n(M) → H^n(P)

this is cohomology.map (what about n)
-/


text:
/-
Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov
-/
import order.filter.basic
import data.set.countable

/-!
# Filters with countable intersection property

In this file we define `countable_Inter_filter` to be the class of filters with the following
property: for any countable collection of sets `s ∈ l` their intersection belongs to `l` as well.

Two main examples are the `residual` filter defined in `topology.metric_space.baire` and
the `measure.ae` filter defined in `measure_theory.measure_space`.

We reformulate the definition in terms of indexed intersection and in terms of `filter.eventually`
and provide instances for some basic constructions (`⊥`, `⊤`, `filter.principal`, `filter.map`,
`filter.comap`, `has_inf.inf`). We also provide a custom constructor `filter.of_countable_Inter`
that deduces two axioms of a `filter` from the countable intersection property.

## Tags
filter, countable
-/

open set filter
open_locale filter

variables {ι α β : Type*}

/-- A filter `l` has the countable intersection property if for any countable collection
of sets `s ∈ l` their intersection belongs to `l` as well. -/
class countable_Inter_filter (l : filter α) : Prop :=
(countable_sInter_mem' :
  ∀ {S : set (set α)} (hSc : countable S) (hS : ∀ s ∈ S, s ∈ l), ⋂₀ S ∈ l)

variables {l : filter α} [countable_Inter_filter l]

lemma countable_sInter_mem {S : set (set α)} (hSc : countable S) :
  ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l :=
⟨λ hS s hs, mem_of_superset hS (sInter_subset_of_mem hs),
  countable_Inter_filter.countable_sInter_mem' hSc⟩

lemma countable_Inter_mem [encodable ι] {s : ι → set α} :
  (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l :=
sInter_range s ▸ (countable_sInter_mem (countable_range _)).trans forall_range_iff

lemma countable_bInter_mem {S : set ι} (hS : countable S) {s : Π i ∈ S, set α} :
  (⋂ i ∈ S, s i ‹_›) ∈ l ↔  ∀ i ∈ S, s i ‹_› ∈ l :=
begin
  rw [bInter_eq_Inter],
  haveI := hS.to_encodable,
  exact countable_Inter_mem.trans subtype.forall
end

lemma eventually_countable_forall [encodable ι] {p : α → ι → Prop} :
  (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i :=
by simpa only [filter.eventually, set_of_forall]
  using @countable_Inter_mem _ _ l _ _ (λ i, {x | p x i})

lemma eventually_countable_ball {S : set ι} (hS : countable S) {p : Π (x : α) (i ∈ S), Prop} :
  (∀ᶠ x in l, ∀ i ∈ S, p x i ‹_›) ↔ ∀ i ∈ S, ∀ᶠ x in l, p x i ‹_› :=
by simpa only [filter.eventually, set_of_forall]
  using @countable_bInter_mem _ _ l _ _ hS (λ i hi, {x | p x i hi})

lemma eventually_le.countable_Union [encodable ι] {s t : ι → set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
  (⋃ i, s i) ≤ᶠ[l] ⋃ i, t i :=
(eventually_countable_forall.2 h).mono $ λ x hst hs, mem_Union.2 $
  (mem_Union.1 hs).imp hst

lemma eventually_eq.countable_Union [encodable ι] {s t : ι → set α} (h : ∀ i, s i =ᶠ[l] t i) :
  (⋃ i, s i) =ᶠ[l] ⋃ i, t i :=
(eventually_le.countable_Union (λ i, (h i).le)).antisymm
  (eventually_le.countable_Union (λ i, (h i).symm.le))

lemma eventually_le.countable_bUnion {S : set ι} (hS : countable S) {s t : Π i ∈ S, set α}
  (h : ∀ i ∈ S, s i ‹_› ≤ᶠ[l] t i ‹_›) : (⋃ i ∈ S, s i ‹_›) ≤ᶠ[l] ⋃ i ∈ S, t i ‹_› :=
begin
  simp only [bUnion_eq_Union],
  haveI := hS.to_encodable,
  exact eventually_le.countable_Union (λ i, h i i.2)
end

lemma eventually_eq.countable_bUnion {S : set ι} (hS : countable S) {s t : Π i ∈ S, set α}
  (h : ∀ i ∈ S, s i ‹_› =ᶠ[l] t i ‹_›) : (⋃ i ∈ S, s i ‹_›) =ᶠ[l] ⋃ i ∈ S, t i ‹_› :=
(eventually_le.countable_bUnion hS (λ i hi, (h i hi).le)).antisymm
  (eventually_le.countable_bUnion hS (λ i hi, (h i hi).symm.le))

lemma eventually_le.countable_Inter [encodable ι] {s t : ι → set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
  (⋂ i, s i) ≤ᶠ[l] ⋂ i, t i :=
(eventually_countable_forall.2 h).mono $ λ x hst hs, mem_Inter.2 $ λ i, hst _ (mem_Inter.1 hs i)

lemma eventually_eq.countable_Inter [encodable ι] {s t : ι → set α} (h : ∀ i, s i =ᶠ[l] t i) :
  (⋂ i, s i) =ᶠ[l] ⋂ i, t i :=
(eventually_le.countable_Inter (λ i, (h i).le)).antisymm
  (eventually_le.countable_Inter (λ i, (h i).symm.le))

lemma eventually_le.countable_bInter {S : set ι} (hS : countable S) {s t : Π i ∈ S, set α}
  (h : ∀ i ∈ S, s i ‹_› ≤ᶠ[l] t i ‹_›) : (⋂ i ∈ S, s i ‹_›) ≤ᶠ[l] ⋂ i ∈ S, t i ‹_› :=
begin
  simp only [bInter_eq_Inter],
  haveI := hS.to_encodable,
  exact eventually_le.countable_Inter (λ i, h i i.2)
end

lemma eventually_eq.countable_bInter {S : set ι} (hS : countable S) {s t : Π i ∈ S, set α}
  (h : ∀ i ∈ S, s i ‹_› =ᶠ[l] t i ‹_›) : (⋂ i ∈ S, s i ‹_›) =ᶠ[l] ⋂ i ∈ S, t i ‹_› :=
(eventually_le.countable_bInter hS (λ i hi, (h i hi).le)).antisymm
  (eventually_le.countable_bInter hS (λ i hi, (h i hi).symm.le))

/-- Construct a filter with countable intersection property. This constructor deduces
`filter.univ_sets` and `filter.inter_sets` from the countable intersection property. -/
def filter.of_countable_Inter (l : set (set α))
  (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l)
  (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
  filter α :=
{ sets := l,
  univ_sets := @sInter_empty α ▸ hp _ countable_empty (empty_subset _),
  sets_of_superset := h_mono,
  inter_sets := λ s t hs ht, sInter_pair s t ▸
    hp _ ((countable_singleton _).insert _) (insert_subset.2 ⟨hs, singleton_subset_iff.2 ht⟩) }

instance filter.countable_Inter_of_countable_Inter (l : set (set α))
  (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l)
  (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
  countable_Inter_filter (filter.of_countable_Inter l hp h_mono) := ⟨hp⟩

@[simp] lemma filter.mem_of_countable_Inter {l : set (set α)}
  (hp : ∀ S : set (set α), countable S → S ⊆ l → (⋂₀ S) ∈ l)
  (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) {s : set α} :
  s ∈ filter.of_countable_Inter l hp h_mono ↔ s ∈ l :=
iff.rfl

instance countable_Inter_filter_principal (s : set α) : countable_Inter_filter (𝓟 s) :=
⟨λ S hSc hS, subset_sInter hS⟩

instance countable_Inter_filter_bot : countable_Inter_filter (⊥ : filter α) :=
by { rw ← principal_empty, apply countable_Inter_filter_principal }

instance countable_Inter_filter_top : countable_Inter_filter (⊤ : filter α) :=
by { rw ← principal_univ, apply countable_Inter_filter_principal }

instance (l : filter β) [countable_Inter_filter l] (f : α → β) :
  countable_Inter_filter (comap f l) :=
begin
  refine ⟨λ S hSc hS, _⟩,
  choose! t htl ht using hS,
  have : (⋂ s ∈ S, t s) ∈ l, from (countable_bInter_mem hSc).2 htl,
  refine ⟨_, this, _⟩,
  simpa [preimage_Inter] using (Inter₂_mono ht)
end

instance (l : filter α) [countable_Inter_filter l] (f : α → β) :
  countable_Inter_filter (map f l) :=
begin
  constructor, intros S hSc hS,
  simp only [mem_map, sInter_eq_bInter, preimage_Inter₂] at hS ⊢,
  exact (countable_bInter_mem hSc).2 hS
end

/-- Infimum of two `countable_Inter_filter`s is a `countable_Inter_filter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
instance countable_Inter_filter_inf (l₁ l₂ : filter α) [countable_Inter_filter l₁]
  [countable_Inter_filter l₂] :
  countable_Inter_filter (l₁ ⊓ l₂) :=
begin
  refine ⟨λ S hSc hS, _⟩,
  choose s hs t ht hst using hS,
  replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs,
  replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem hSc).2 ht,
  refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter $ λ i hi, _),
  rw hst i hi,
  apply inter_subset_inter ; exact Inter_subset_of_subset i (Inter_subset _ _)
end

/-- Supremum of two `countable_Inter_filter`s is a `countable_Inter_filter`. -/
instance countable_Inter_filter_sup (l₁ l₂ : filter α) [countable_Inter_filter l₁]
  [countable_Inter_filter l₂] :
  countable_Inter_filter (l₁ ⊔ l₂) :=
begin
  refine ⟨λ S hSc hS, ⟨_, _⟩⟩; refine (countable_sInter_mem hSc).2 (λ s hs, _),
  exacts [(hS s hs).1, (hS s hs).2]
end

author: Mel-TunaRoll

repo: Lean-Mordell-Weil-Mel-Branch


text:
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Kevin Kappelmann
-/
import tactic.abel
import tactic.linarith

/-!
# Floor and ceil

## Summary

We define the natural- and integer-valued floor and ceil functions on linearly ordered rings.

## Main Definitions

* `floor_semiring`: A linearly ordered semiring with natural-valued floor and ceil.
* `nat.floor a`: Greatest natural `n` such that `n ≤ a`. Equal to `0` if `a < 0`.
* `nat.ceil a`: Least natural `n` such that `a ≤ n`.

* `floor_ring`: A linearly ordered ring with integer-valued floor and ceil.
* `int.floor a`: Greatest integer `z` such that `z ≤ a`.
* `int.ceil a`: Least integer `z` such that `a ≤ z`.
* `int.fract a`: Fractional part of `a`, defined as `a - floor a`.

## Notations

* `⌊a⌋₊` is `nat.floor a`.
* `⌈a⌉₊` is `nat.ceil a`.
* `⌊a⌋` is `int.floor a`.
* `⌈a⌉` is `int.ceil a`.

The index `₊` in the notations for `nat.floor` and `nat.ceil` is used in analogy to the notation
for `nnnorm`.

## TODO

Some `nat.floor` and `nat.ceil` lemmas require `linear_ordered_ring α`. Is `has_ordered_sub` enough?

`linear_ordered_ring`/`linear_ordered_semiring` can be relaxed to `order_ring`/`order_semiring` in
many lemmas.

## Tags

rounding, floor, ceil
-/

open set
variables {α : Type*}

/-! ### Floor semiring -/

/-- A `floor_semiring` is a linear ordered semiring over `α` with a function
`floor : α → ℕ` satisfying `∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x)`. -/
class floor_semiring (α) [ordered_semiring α] :=
(floor : α → ℕ)
(ceil : α → ℕ)
(floor_of_neg {a : α} (ha : a < 0) : floor a = 0)
(gc_floor {a : α} {n : ℕ} (ha : 0 ≤ a) : n ≤ floor a ↔ (n : α) ≤ a)
(gc_ceil : galois_connection ceil coe)

instance : floor_semiring ℕ :=
{ floor := id,
  ceil := id,
  floor_of_neg := λ a ha, (a.not_lt_zero ha).elim,
  gc_floor := λ n a ha, by { rw nat.cast_id, refl },
  gc_ceil := λ n a, by { rw nat.cast_id, refl } }

namespace nat
section linear_ordered_semiring
variables [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : ℕ}

/-- `⌊a⌋₊` is the greatest natural `n` such that `n ≤ a`. If `a` is negative, then `⌊a⌋₊ = 0`. -/
def floor : α → ℕ := floor_semiring.floor

/-- `⌈a⌉₊` is the least natural `n` such that `a ≤ n` -/
def ceil : α → ℕ := floor_semiring.ceil

notation `⌊` a `⌋₊` := nat.floor a
notation `⌈` a `⌉₊` := nat.ceil a

lemma le_floor_iff (ha : 0 ≤ a) : n ≤ ⌊a⌋₊ ↔ (n : α) ≤ a := floor_semiring.gc_floor ha

lemma le_floor (h : (n : α) ≤ a) : n ≤ ⌊a⌋₊ := (le_floor_iff $ n.cast_nonneg.trans h).2 h

lemma floor_lt (ha : 0 ≤ a) : ⌊a⌋₊ < n ↔ a < n := lt_iff_lt_of_le_iff_le $ le_floor_iff ha

lemma lt_of_floor_lt (h : ⌊a⌋₊ < n) : a < n := lt_of_not_ge' $ λ h', (le_floor h').not_lt h

lemma floor_le (ha : 0 ≤ a) : (⌊a⌋₊ : α) ≤ a := (le_floor_iff ha).1 le_rfl

lemma lt_succ_floor (a : α) : a < ⌊a⌋₊.succ := lt_of_floor_lt $ nat.lt_succ_self _

lemma lt_floor_add_one (a : α) : a < ⌊a⌋₊ + 1 := lt_succ_floor a

@[simp] lemma floor_coe (n : ℕ) : ⌊(n : α)⌋₊ = n :=
eq_of_forall_le_iff $ λ a, by { rw [le_floor_iff, nat.cast_le], exact n.cast_nonneg }

@[simp] lemma floor_zero : ⌊(0 : α)⌋₊ = 0 := floor_coe 0

@[simp] lemma floor_one : ⌊(1 : α)⌋₊ = 1 := by rw [←nat.cast_one, floor_coe]

lemma floor_of_nonpos (ha : a ≤ 0) : ⌊a⌋₊ = 0 :=
ha.lt_or_eq.elim floor_semiring.floor_of_neg $ by { rintro rfl, exact floor_zero }

lemma floor_mono : monotone (floor : α → ℕ) := λ a b h, begin
  obtain ha | ha := le_total a 0,
  { rw floor_of_nonpos ha,
    exact nat.zero_le _ },
  { exact le_floor ((floor_le ha).trans h) }
end

lemma le_floor_iff' (hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ (n : α) ≤ a :=
begin
  obtain ha | ha := le_total a 0,
  { rw floor_of_nonpos ha,
    exact iff_of_false (nat.pos_of_ne_zero hn).not_le
      (not_le_of_lt $ ha.trans_lt $ cast_pos.2 $ nat.pos_of_ne_zero hn) },
  { exact le_floor_iff ha }
end

lemma floor_lt' (hn : n ≠ 0) : ⌊a⌋₊ < n ↔ a < n := lt_iff_lt_of_le_iff_le $ le_floor_iff' hn

lemma floor_pos : 0 < ⌊a⌋₊ ↔ 1 ≤ a :=
by { convert le_floor_iff' nat.one_ne_zero, exact cast_one.symm }

lemma pos_of_floor_pos (h : 0 < ⌊a⌋₊) : 0 < a :=
(le_or_lt a 0).resolve_left (λ ha, lt_irrefl 0 $ by rwa floor_of_nonpos ha at h)

lemma lt_of_lt_floor (h : n < ⌊a⌋₊) : ↑n < a :=
(nat.cast_lt.2 h).trans_le $ floor_le (pos_of_floor_pos $ (nat.zero_le n).trans_lt h).le

lemma floor_le_of_le (h : a ≤ n) : ⌊a⌋₊ ≤ n := le_imp_le_iff_lt_imp_lt.2 lt_of_lt_floor h

@[simp] lemma floor_eq_zero : ⌊a⌋₊ = 0 ↔ a < 1 :=
by { rw [←lt_one_iff, ←@cast_one α], exact floor_lt' nat.one_ne_zero }

lemma floor_eq_iff (ha : 0 ≤ a) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 :=
by rw [←le_floor_iff ha, ←nat.cast_one, ←nat.cast_add, ←floor_lt ha, nat.lt_add_one_iff,
  le_antisymm_iff, and.comm]

lemma floor_eq_iff' (hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 :=
by rw [← le_floor_iff' hn, ← nat.cast_one, ← nat.cast_add, ← floor_lt' (nat.add_one_ne_zero n),
  nat.lt_add_one_iff, le_antisymm_iff, and.comm]

lemma floor_eq_on_Ico (n : ℕ) : ∀ a ∈ (set.Ico n (n+1) : set α), ⌊a⌋₊ = n :=
λ a ⟨h₀, h₁⟩, (floor_eq_iff $ n.cast_nonneg.trans h₀).mpr ⟨h₀, h₁⟩

@[simp] lemma preimage_floor_zero : (floor : α → ℕ) ⁻¹' {0} = Iio 1 :=
ext $ λ a, floor_eq_zero

lemma preimage_floor_of_ne_zero {n : ℕ} (hn : n ≠ 0) : (floor : α → ℕ) ⁻¹' {n} = Ico n (n + 1) :=
ext $ λ a, floor_eq_iff' hn

/-! #### Ceil -/

lemma gc_ceil_coe : galois_connection (ceil : α → ℕ) coe := floor_semiring.gc_ceil

@[simp] lemma ceil_le : ⌈a⌉₊ ≤ n ↔ a ≤ n := gc_ceil_coe _ _

lemma lt_ceil : n < ⌈a⌉₊ ↔ (n : α) < a := lt_iff_lt_of_le_iff_le ceil_le

lemma le_ceil (a : α) : a ≤ ⌈a⌉₊ := ceil_le.1 le_rfl

lemma ceil_mono : monotone (ceil : α → ℕ) := gc_ceil_coe.monotone_l

@[simp] lemma ceil_coe (n : ℕ) : ⌈(n : α)⌉₊ = n :=
eq_of_forall_ge_iff $ λ a, ceil_le.trans nat.cast_le

@[simp] lemma ceil_zero : ⌈(0 : α)⌉₊ = 0 := ceil_coe 0

@[simp] lemma ceil_eq_zero : ⌈a⌉₊ = 0 ↔ a ≤ 0 := le_zero_iff.symm.trans ceil_le

lemma lt_of_ceil_lt (h : ⌈a⌉₊ < n) : a < n := (le_ceil a).trans_lt (nat.cast_lt.2 h)

lemma le_of_ceil_le (h : ⌈a⌉₊ ≤ n) : a ≤ n := (le_ceil a).trans (nat.cast_le.2 h)

lemma floor_le_ceil (a : α) : ⌊a⌋₊ ≤ ⌈a⌉₊ :=
begin
  obtain ha | ha := le_total a 0,
  { rw floor_of_nonpos ha,
    exact nat.zero_le _ },
  { exact cast_le.1 ((floor_le ha).trans $ le_ceil _) }
end

lemma floor_lt_ceil_of_lt_of_pos {a b : α} (h : a < b) (h' : 0 < b) : ⌊a⌋₊ < ⌈b⌉₊ :=
begin
  rcases le_or_lt 0 a with ha|ha,
  { rw floor_lt ha, exact h.trans_le (le_ceil _) },
  { rwa [floor_of_nonpos ha.le, lt_ceil] }
end

lemma ceil_eq_iff (hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n :=
by rw [← ceil_le, ← not_le, ← ceil_le, not_le,
  tsub_lt_iff_right (nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), nat.lt_add_one_iff,
  le_antisymm_iff, and.comm]

@[simp] lemma preimage_ceil_zero : (nat.ceil : α → ℕ) ⁻¹' {0} = Iic 0 :=
ext $ λ x, ceil_eq_zero

lemma preimage_ceil_of_ne_zero (hn : n ≠ 0) : (nat.ceil : α → ℕ) ⁻¹' {n} = Ioc ↑(n - 1) n :=
ext $ λ x, ceil_eq_iff hn

end linear_ordered_semiring

section linear_ordered_ring
variables [linear_ordered_ring α] [floor_semiring α] {a : α} {n : ℕ}

lemma floor_add_nat (ha : 0 ≤ a) (n : ℕ) : ⌊a + n⌋₊ = ⌊a⌋₊ + n :=
eq_of_forall_le_iff $ λ b, begin
  rw [le_floor_iff (add_nonneg ha n.cast_nonneg), ←sub_le_iff_le_add],
  obtain hb | hb := le_total n b,
  { rw [←cast_sub hb, ←tsub_le_iff_right],
    exact (le_floor_iff ha).symm },
  { exact iff_of_true ((sub_nonpos_of_le $ cast_le.2 hb).trans ha) (le_add_left hb) }
end

lemma floor_add_one (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1 :=
by { convert floor_add_nat ha 1, exact cast_one.symm }

lemma floor_sub_nat (a : α) (n : ℕ) : ⌊a - n⌋₊ = ⌊a⌋₊ - n :=
begin
  obtain ha | ha := le_total a 0,
  { rw [floor_of_nonpos ha, floor_of_nonpos (sub_nonpos_of_le (ha.trans n.cast_nonneg)),
      zero_tsub] },
  cases le_total a n,
  { rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le],
    exact nat.cast_le.1 ((nat.floor_le ha).trans h) },
  { rw [eq_tsub_iff_add_eq_of_le (le_floor h), ←floor_add_nat (sub_nonneg_of_le h),
      sub_add_cancel] }
end

lemma sub_one_lt_floor (a : α) : a - 1 < ⌊a⌋₊ := sub_lt_iff_lt_add.2 $ lt_floor_add_one a

lemma ceil_add_nat (ha : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
eq_of_forall_ge_iff $ λ b, begin
  rw [←not_lt, ←not_lt, not_iff_not],
  rw [lt_ceil],
  obtain hb | hb := le_or_lt n b,
  { rw [←tsub_lt_iff_right hb, ←sub_lt_iff_lt_add, ←cast_sub hb],
    exact lt_ceil.symm },
  { exact iff_of_true (lt_add_of_nonneg_of_lt ha $ cast_lt.2 hb) (lt_add_left _ _ _ hb) }
end

lemma ceil_add_one (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1 :=
by { convert ceil_add_nat ha 1, exact cast_one.symm }

lemma ceil_lt_add_one (ha : 0 ≤ a) : (⌈a⌉₊ : α) < a + 1 :=
lt_ceil.1 $ (nat.lt_succ_self _).trans_le (ceil_add_one ha).ge

end linear_ordered_ring

section linear_ordered_field
variables [linear_ordered_field α] [floor_semiring α]

lemma floor_div_nat (a : α) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n :=
begin
  cases le_total a 0 with ha ha,
  { rw [floor_of_nonpos, floor_of_nonpos ha],
    { simp },
    apply div_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg },
  obtain rfl | hn := n.eq_zero_or_pos,
  { rw [cast_zero, div_zero, nat.div_zero, floor_zero] },
  refine (floor_eq_iff _).2 _,
  { exact div_nonneg ha n.cast_nonneg },
  split,
  { exact cast_div_le.trans (div_le_div_of_le_of_nonneg (floor_le ha) n.cast_nonneg) },
  rw [div_lt_iff, add_mul, one_mul, ←cast_mul, ←cast_add, ←floor_lt ha],
  { exact lt_div_mul_add hn },
  { exact (cast_pos.2 hn) }
end

/-- Natural division is the floor of field division. -/
lemma floor_div_eq_div (m n : ℕ) : ⌊(m : α) / n⌋₊ = m / n :=
by { convert floor_div_nat (m : α) n, rw m.floor_coe }

end linear_ordered_field
end nat

/-- There exists at most one `floor_semiring` structure on a linear ordered semiring. -/
lemma subsingleton_floor_semiring {α} [linear_ordered_semiring α] :
  subsingleton (floor_semiring α) :=
begin
  refine ⟨λ H₁ H₂, _⟩,
  have : H₁.ceil = H₂.ceil,
    from funext (λ a, H₁.gc_ceil.l_unique H₂.gc_ceil $ λ n, rfl),
  have : H₁.floor = H₂.floor,
  { ext a,
    cases lt_or_le a 0,
    { rw [H₁.floor_of_neg, H₂.floor_of_neg]; exact h },
    { refine eq_of_forall_le_iff (λ n, _),
      rw [H₁.gc_floor, H₂.gc_floor]; exact h } },
  cases H₁, cases H₂, congr; assumption
end

/-! ### Floor rings -/

/--
A `floor_ring` is a linear ordered ring over `α` with a function
`floor : α → ℤ` satisfying `∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a)`.
-/
class floor_ring (α) [linear_ordered_ring α] :=
(floor : α → ℤ)
(ceil : α → ℤ)
(gc_coe_floor : galois_connection coe floor)
(gc_ceil_coe : galois_connection ceil coe)

instance : floor_ring ℤ :=
{ floor := id,
  ceil := id,
  gc_coe_floor := λ a b, by { rw int.cast_id, refl },
  gc_ceil_coe := λ a b, by { rw int.cast_id, refl } }

/-- A `floor_ring` constructor from the `floor` function alone. -/
def floor_ring.of_floor (α) [linear_ordered_ring α] (floor : α → ℤ)
  (gc_coe_floor : galois_connection coe floor) : floor_ring α :=
{ floor := floor,
  ceil := λ a, -floor (-a),
  gc_coe_floor := gc_coe_floor,
  gc_ceil_coe := λ a z, by rw [neg_le, ←gc_coe_floor, int.cast_neg, neg_le_neg_iff] }

/-- A `floor_ring` constructor from the `ceil` function alone. -/
def floor_ring.of_ceil (α) [linear_ordered_ring α] (ceil : α → ℤ)
  (gc_ceil_coe : galois_connection ceil coe) : floor_ring α :=
{ floor := λ a, -ceil (-a),
  ceil := ceil,
  gc_coe_floor := λ a z, by rw [le_neg, gc_ceil_coe, int.cast_neg, neg_le_neg_iff],
  gc_ceil_coe := gc_ceil_coe }

namespace int
variables [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α}

/-- `int.floor a` is the greatest integer `z` such that `z ≤ a`. It is denoted with `⌊a⌋`. -/
def floor : α → ℤ := floor_ring.floor

/-- `int.ceil a` is the smallest integer `z` such that `a ≤ z`. It is denoted with `⌈a⌉`. -/
def ceil : α → ℤ := floor_ring.ceil

/-- `int.fract a`, the fractional part of `a`, is `a` minus its floor. -/
def fract (a : α) : α := a - floor a

notation `⌊` a `⌋` := int.floor a
notation `⌈` a `⌉` := int.ceil a
-- Mathematical notation for `fract a` is usually `{a}`. Let's not even go there.

@[simp] lemma floor_ring_floor_eq : @floor_ring.floor = @int.floor := rfl

@[simp] lemma floor_ring_ceil_eq : @floor_ring.ceil = @int.ceil := rfl

/-! #### Floor -/

lemma gc_coe_floor : galois_connection (coe : ℤ → α) floor := floor_ring.gc_coe_floor

lemma le_floor : z ≤ ⌊a⌋ ↔ (z : α) ≤ a := (gc_coe_floor z a).symm

lemma floor_lt : ⌊a⌋ < z ↔ a < z := lt_iff_lt_of_le_iff_le le_floor

lemma floor_le (a : α) : (⌊a⌋ : α) ≤ a := gc_coe_floor.l_u_le a

lemma floor_nonneg : 0 ≤ ⌊a⌋ ↔ 0 ≤ a := le_floor

lemma floor_nonpos (ha : a ≤ 0) : ⌊a⌋ ≤ 0 :=
begin
  rw ←@cast_le α,
  exact (floor_le a).trans ha,
end

lemma lt_succ_floor (a : α) : a < ⌊a⌋.succ := floor_lt.1 $ int.lt_succ_self _

lemma lt_floor_add_one (a : α) : a < ⌊a⌋ + 1 :=
by simpa only [int.succ, int.cast_add, int.cast_one] using lt_succ_floor a

lemma sub_one_lt_floor (a : α) : a - 1 < ⌊a⌋ := sub_lt_iff_lt_add.2 (lt_floor_add_one a)

@[simp] lemma floor_coe (z : ℤ) : ⌊(z : α)⌋ = z :=
eq_of_forall_le_iff $ λ a, by rw [le_floor, int.cast_le]

@[simp] lemma floor_zero : ⌊(0 : α)⌋ = 0 := floor_coe 0

@[simp] lemma floor_one : ⌊(1 : α)⌋ = 1 := by rw [← int.cast_one, floor_coe]

@[mono] lemma floor_mono : monotone (floor : α → ℤ) := gc_coe_floor.monotone_u

lemma floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a :=
by { convert le_floor, exact cast_one.symm }

@[simp] lemma floor_add_int (a : α) (z : ℤ) : ⌊a + z⌋ = ⌊a⌋ + z :=
eq_of_forall_le_iff $ λ a, by rw [le_floor,
  ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, int.cast_sub]

lemma floor_add_one (a : α) : ⌊a + 1⌋ = ⌊a⌋ + 1 :=
by { convert floor_add_int a 1, exact cast_one.symm }

@[simp] lemma floor_int_add (z : ℤ) (a : α) : ⌊↑z + a⌋ = z + ⌊a⌋ :=
by simpa only [add_comm] using floor_add_int a z

@[simp] lemma floor_add_nat (a : α) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n := floor_add_int a n

@[simp] lemma floor_nat_add (n : ℕ) (a : α) : ⌊↑n + a⌋ = n + ⌊a⌋ := floor_int_add n a

@[simp] lemma floor_sub_int (a : α) (z : ℤ) : ⌊a - z⌋ = ⌊a⌋ - z :=
eq.trans (by rw [int.cast_neg, sub_eq_add_neg]) (floor_add_int _ _)

@[simp] lemma floor_sub_nat (a : α) (n : ℕ) : ⌊a - n⌋ = ⌊a⌋ - n := floor_sub_int a n

lemma abs_sub_lt_one_of_floor_eq_floor {α : Type*} [linear_ordered_comm_ring α] [floor_ring α]
  {a b : α} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1 :=
begin
  have : a < ⌊a⌋ + 1     := lt_floor_add_one a,
  have : b < ⌊b⌋ + 1     := lt_floor_add_one b,
  have : (⌊a⌋ : α) = ⌊b⌋ := int.cast_inj.2 h,
  have : (⌊a⌋ : α) ≤ a   := floor_le a,
  have : (⌊b⌋ : α) ≤ b   := floor_le b,
  exact abs_sub_lt_iff.2 ⟨by linarith, by linarith⟩
end

lemma floor_eq_iff : ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < z + 1 :=
by rw [le_antisymm_iff, le_floor, ←int.lt_add_one_iff, floor_lt, int.cast_add, int.cast_one,
  and.comm]

lemma floor_eq_on_Ico (n : ℤ) : ∀ a ∈ set.Ico (n : α) (n + 1), ⌊a⌋ = n :=
λ a ⟨h₀, h₁⟩, floor_eq_iff.mpr ⟨h₀, h₁⟩

lemma floor_eq_on_Ico' (n : ℤ) : ∀ a ∈ set.Ico (n : α) (n + 1), (⌊a⌋ : α) = n :=
λ a ha, congr_arg _ $ floor_eq_on_Ico n a ha

@[simp] lemma preimage_floor_singleton (m : ℤ) : (floor : α → ℤ) ⁻¹' {m} = Ico m (m + 1) :=
ext $ λ x, floor_eq_iff

/-! #### Fractional part -/

@[simp] lemma self_sub_floor (a : α) : a - ⌊a⌋ = fract a := rfl

@[simp] lemma floor_add_fract (a : α) : (⌊a⌋ : α) + fract a = a := add_sub_cancel'_right _ _

@[simp] lemma fract_add_floor (a : α) : fract a + ⌊a⌋ = a := sub_add_cancel _ _

@[simp] lemma fract_add_int (a : α) (m : ℤ) : fract (a + m) = fract a :=
by { rw fract, simp }

@[simp] lemma fract_sub_int (a : α) (m : ℤ) : fract (a - m) = fract a :=
by { rw fract, simp }

@[simp] lemma fract_int_add (m : ℤ) (a : α) : fract (↑m + a) = fract a :=
by rw [add_comm, fract_add_int]

@[simp] lemma self_sub_fract (a : α) : a - fract a = ⌊a⌋ := sub_sub_cancel _ _

@[simp] lemma fract_sub_self (a : α) : fract a - a = -⌊a⌋ := sub_sub_cancel_left _ _

lemma fract_nonneg (a : α) : 0 ≤ fract a := sub_nonneg.2 $ floor_le _

lemma fract_lt_one (a : α) : fract a < 1 := sub_lt.1 $ sub_one_lt_floor _

@[simp] lemma fract_zero : fract (0 : α) = 0 := by rw [fract, floor_zero, cast_zero, sub_self]

@[simp] lemma fract_coe (z : ℤ) : fract (z : α) = 0 :=
by { unfold fract, rw floor_coe, exact sub_self _ }

@[simp] lemma fract_floor (a : α) : fract (⌊a⌋ : α) = 0 := fract_coe _

@[simp] lemma floor_fract (a : α) : ⌊fract a⌋ = 0 :=
floor_eq_iff.2 ⟨fract_nonneg _, by { rw [int.cast_zero, zero_add], exact fract_lt_one a }⟩

lemma fract_eq_iff {a b : α} : fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ z : ℤ, a - b = z :=
⟨λ h, by { rw ←h, exact ⟨fract_nonneg _, fract_lt_one _, ⟨⌊a⌋, sub_sub_cancel _ _⟩⟩},
  begin
    rintro ⟨h₀, h₁, z, hz⟩,
    show a - ⌊a⌋ = b, apply eq.symm,
    rw [eq_sub_iff_add_eq, add_comm, ←eq_sub_iff_add_eq],
    rw [hz, int.cast_inj, floor_eq_iff, ←hz],
    clear hz, split; simpa [sub_eq_add_neg, add_assoc]
  end⟩

lemma fract_eq_fract {a b : α} : fract a = fract b ↔ ∃ z : ℤ, a - b = z :=
⟨λ h, ⟨⌊a⌋ - ⌊b⌋, begin
  unfold fract at h, rw [int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h],
 end⟩, begin
  rintro ⟨z, hz⟩,
  refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, _⟩,
  rw [eq_add_of_sub_eq hz, add_comm, int.cast_add],
  exact add_sub_sub_cancel _ _ _,
end⟩

@[simp] lemma fract_eq_self {a : α} : fract a = a ↔ 0 ≤ a ∧ a < 1 :=
fract_eq_iff.trans $ and.assoc.symm.trans $ and_iff_left ⟨0, sub_self a⟩

@[simp] lemma fract_fract (a : α) : fract (fract a) = fract a :=
fract_eq_self.2 ⟨fract_nonneg _, fract_lt_one _⟩

lemma fract_add (a b : α) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by { unfold fract, simp [sub_eq_add_neg], abel }⟩

lemma fract_mul_nat (a : α) (b : ℕ) : ∃ z : ℤ, fract a * b - fract (a * b) = z :=
begin
  induction b with c hc,
    use 0, simp,
  rcases hc with ⟨z, hz⟩,
  rw [nat.succ_eq_add_one, nat.cast_add, mul_add, mul_add, nat.cast_one, mul_one, mul_one],
  rcases fract_add (a * c) a with ⟨y, hy⟩,
  use z - y,
  rw [int.cast_sub, ←hz, ←hy],
  abel
end

lemma preimage_fract (s : set α) : fract ⁻¹' s = ⋃ m : ℤ, (λ x, x - m) ⁻¹' (s ∩ Ico (0 : α) 1) :=
begin
  ext x,
  simp only [mem_preimage, mem_Union, mem_inter_eq],
  refine ⟨λ h, ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, _⟩,
  rintro ⟨m, hms, hm0, hm1⟩,
  obtain rfl : ⌊x⌋ = m, from floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩,
  exact hms
end

lemma image_fract (s : set α) : fract '' s = ⋃ m : ℤ, (λ x, x - m) '' s ∩ Ico 0 1 :=
begin
  ext x,
  simp only [mem_image, mem_inter_eq, mem_Union], split,
  { rintro ⟨y, hy, rfl⟩,
    exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩ },
  { rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩,
    obtain rfl : ⌊y⌋ = m, from floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩,
    exact ⟨y, hys, rfl⟩ }
end

/-! #### Ceil -/

lemma gc_ceil_coe : galois_connection ceil (coe : ℤ → α) := floor_ring.gc_ceil_coe

lemma ceil_le : ⌈a⌉ ≤ z ↔ a ≤ z := gc_ceil_coe a z

lemma floor_neg : ⌊-a⌋ = -⌈a⌉ :=
eq_of_forall_le_iff (λ z, by rw [le_neg, ceil_le, le_floor, int.cast_neg, le_neg])

lemma ceil_neg : ⌈-a⌉ = -⌊a⌋ :=
eq_of_forall_ge_iff (λ z, by rw [neg_le, ceil_le, le_floor, int.cast_neg, neg_le])

lemma lt_ceil : z < ⌈a⌉ ↔ (z : α) < a := lt_iff_lt_of_le_iff_le ceil_le

lemma ceil_le_floor_add_one (a : α) : ⌈a⌉ ≤ ⌊a⌋ + 1 :=
by { rw [ceil_le, int.cast_add, int.cast_one], exact (lt_floor_add_one a).le }

lemma le_ceil (a : α) : a ≤ ⌈a⌉ := gc_ceil_coe.le_u_l a

@[simp] lemma ceil_coe (z : ℤ) : ⌈(z : α)⌉ = z :=
eq_of_forall_ge_iff $ λ a, by rw [ceil_le, int.cast_le]

lemma ceil_mono : monotone (ceil : α → ℤ) := gc_ceil_coe.monotone_l

@[simp] lemma ceil_add_int (a : α) (z : ℤ) : ⌈a + z⌉ = ⌈a⌉ + z :=
by rw [←neg_inj, neg_add', ←floor_neg, ←floor_neg, neg_add', floor_sub_int]

@[simp] lemma ceil_add_one (a : α) : ⌈a + 1⌉ = ⌈a⌉ + 1 :=
by { convert ceil_add_int a (1 : ℤ), exact cast_one.symm }

@[simp] lemma ceil_sub_int (a : α) (z : ℤ) : ⌈a - z⌉ = ⌈a⌉ - z :=
eq.trans (by rw [int.cast_neg, sub_eq_add_neg]) (ceil_add_int _ _)

@[simp] lemma ceil_sub_one (a : α) : ⌈a - 1⌉ = ⌈a⌉ - 1 :=
by rw [eq_sub_iff_add_eq, ← ceil_add_one, sub_add_cancel]

lemma ceil_lt_add_one (a : α) : (⌈a⌉ : α) < a + 1 :=
by { rw [← lt_ceil, ← int.cast_one, ceil_add_int], apply lt_add_one }

lemma ceil_pos : 0 < ⌈a⌉ ↔ 0 < a := lt_ceil

@[simp] lemma ceil_zero : ⌈(0 : α)⌉ = 0 := ceil_coe 0

lemma ceil_nonneg (ha : 0 ≤ a) : 0 ≤ ⌈a⌉ :=
by exact_mod_cast ha.trans (le_ceil a)

lemma ceil_eq_iff : ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ z :=
by rw [←ceil_le, ←int.cast_one, ←int.cast_sub, ←lt_ceil, int.sub_one_lt_iff, le_antisymm_iff,
  and.comm]

lemma ceil_eq_on_Ioc (z : ℤ) : ∀ a ∈ set.Ioc (z - 1 : α) z, ⌈a⌉ = z :=
λ a ⟨h₀, h₁⟩, ceil_eq_iff.mpr ⟨h₀, h₁⟩

lemma ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ set.Ioc (z - 1 : α) z, (⌈a⌉ : α) = z :=
λ a ha, by exact_mod_cast ceil_eq_on_Ioc z a ha

lemma floor_le_ceil (a : α) : ⌊a⌋ ≤ ⌈a⌉ := cast_le.1 $ (floor_le _).trans $ le_ceil _

lemma floor_lt_ceil_of_lt {a b : α} (h : a < b) : ⌊a⌋ < ⌈b⌉ :=
cast_lt.1 $ (floor_le a).trans_lt $ h.trans_le $ le_ceil b

@[simp] lemma preimage_ceil_singleton (m : ℤ) : (ceil : α → ℤ) ⁻¹' {m} = Ioc (m - 1) m :=
ext $ λ x, ceil_eq_iff

/-! #### Intervals -/

@[simp] lemma preimage_Ioo {a b : α} : ((coe : ℤ → α) ⁻¹' (set.Ioo a b)) = set.Ioo ⌊a⌋ ⌈b⌉ :=
by { ext, simp [floor_lt, lt_ceil] }

@[simp] lemma preimage_Ico {a b : α} : ((coe : ℤ → α) ⁻¹' (set.Ico a b)) = set.Ico ⌈a⌉ ⌈b⌉ :=
by { ext, simp [ceil_le, lt_ceil] }

@[simp] lemma preimage_Ioc {a b : α} : ((coe : ℤ → α) ⁻¹' (set.Ioc a b)) = set.Ioc ⌊a⌋ ⌊b⌋ :=
by { ext, simp [floor_lt, le_floor] }

@[simp] lemma preimage_Icc {a b : α} : ((coe : ℤ → α) ⁻¹' (set.Icc a b)) = set.Icc ⌈a⌉ ⌊b⌋ :=
by { ext, simp [ceil_le, le_floor] }

@[simp] lemma preimage_Ioi : ((coe : ℤ → α) ⁻¹' (set.Ioi a)) = set.Ioi ⌊a⌋ :=
by { ext, simp [floor_lt] }

@[simp] lemma preimage_Ici : ((coe : ℤ → α) ⁻¹' (set.Ici a)) = set.Ici ⌈a⌉ :=
by { ext, simp [ceil_le] }

@[simp] lemma preimage_Iio : ((coe : ℤ → α) ⁻¹' (set.Iio a)) = set.Iio ⌈a⌉ :=
by { ext, simp [lt_ceil] }

@[simp] lemma preimage_Iic : ((coe : ℤ → α) ⁻¹' (set.Iic a)) = set.Iic ⌊a⌋ :=
by { ext, simp [le_floor] }

end int

variables {α} [linear_ordered_ring α] [floor_ring α]

/-! #### A floor ring as a floor semiring -/

@[priority 100] -- see Note [lower instance priority]
instance _root_.floor_ring.to_floor_semiring : floor_semiring α :=
{ floor := λ a, ⌊a⌋.to_nat,
  ceil := λ a, ⌈a⌉.to_nat,
  floor_of_neg := λ a ha, int.to_nat_of_nonpos (int.floor_nonpos ha.le),
  gc_floor := λ a n ha, by { rw [int.le_to_nat_iff (int.floor_nonneg.2 ha), int.le_floor], refl },
  gc_ceil := λ a n, by { rw [int.to_nat_le, int.ceil_le], refl } }

lemma int.floor_to_nat (a : α) : ⌊a⌋.to_nat = ⌊a⌋₊ := rfl

lemma int.ceil_to_nat  (a : α) : ⌈a⌉.to_nat = ⌈a⌉₊ := rfl

variables {a : α}

lemma nat.cast_floor_eq_int_floor (ha : 0 ≤ a) : (⌊a⌋₊ : ℤ) = ⌊a⌋ :=
by rw [←int.floor_to_nat, int.to_nat_of_nonneg (int.floor_nonneg.2 ha)]

lemma nat.cast_floor_eq_cast_int_floor (ha : 0 ≤ a) : (⌊a⌋₊ : α) = ⌊a⌋ :=
by rw [←nat.cast_floor_eq_int_floor ha, int.cast_coe_nat]

lemma nat.cast_ceil_eq_int_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉ :=
by { rw [←int.ceil_to_nat, int.to_nat_of_nonneg (int.ceil_nonneg ha)] }

lemma nat.cast_ceil_eq_cast_int_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : α) = ⌈a⌉ :=
by rw [←nat.cast_ceil_eq_int_ceil ha, int.cast_coe_nat]

/-- There exists at most one `floor_ring` structure on a given linear ordered ring. -/
lemma subsingleton_floor_ring {α} [linear_ordered_ring α] :
  subsingleton (floor_ring α) :=
begin
  refine ⟨λ H₁ H₂, _⟩,
  have : H₁.floor = H₂.floor := funext (λ a, H₁.gc_coe_floor.u_unique H₂.gc_coe_floor $ λ _, rfl),
  have : H₁.ceil = H₂.ceil := funext (λ a, H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe $ λ _, rfl),
  cases H₁, cases H₂, congr; assumption
end


import data.real.irrational
import topology.basic
import algebra.order.floor

--OUTPUT 1
theorem irrational_orbit_dense {α : ℝ} (hα_irrat : irrational α) : closure ((λ m : ℤ, int.fract (α * ↑m)) '' (@set.univ ℤ)) = set.Icc 0 1 :=
begin
  have h1 : ∀ i j : ℤ, i ≠ j → int.fract (α * ↑i) ≠ int.fract (α * ↑j), from assume (i j : ℤ) (hneq : i ≠ j),
    have h2 : α ≠ (int.fract (α * ↑i) - int.fract (α * ↑j)) / (i - j), from by {
      assume h3 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) / (i - j),
      have h4 : (i - j) ≠ 0, from by {
        assume h5 : (i - j) = 0,
        have h6 : i = j, from by {
          rw [h5,sub_self] at hneq,
          exact hneq,
        },
        exact hneq h6,
      },
      have h7 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h8 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h9 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h10 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h11 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h12 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h13 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h14 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h15 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h16 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h17 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h18 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h19 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h20 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h21 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h22 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h23 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h24 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h25 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h26 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h27 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h28 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h29 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h30 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h31 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h32 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h33 : α = (int.fract (α * ↑i) - int.fract (α * ↑j)) * (i - j)⁻¹, from by {
        rw [h3,div_mul_cancel h4],
      },
      have h34 : α = (int.fract (α * ↑i) - int
end --Needs more than 2000 tokens!

/- FEW SHOT PROMPTS TO CODEX(START)
/--`theorem`
Power Set is Closed under Intersection
Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:
:$\forall A, B \in \powerset S: A \cap B \in \powerset S$
`proof`
Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.
{{qed}}
-/
theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈ 𝒫 S, (A ∩ B) ∈ 𝒫 S :=
begin
  assume (A : set α) (hA : A ∈ 𝒫 S) (B : set α) (hB : B ∈ 𝒫 S),
  have h1 : (A ⊆ S) ∧ (B ⊆ S), from by {split,apply set.subset_of_mem_powerset,exact hA,apply set.subset_of_mem_powerset,exact hB},
  have h2 : (A ∩ B) ⊆ A, from by apply set.inter_subset_left,
  have h3 : (A ∩ B) ⊆ S, from by {apply set.subset.trans h2 h1.left},
  show (A ∩ B) ∈  𝒫 S, from by {apply set.mem_powerset h3},
end

/--`theorem`
Square of Sum
 :$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$
`proof`
Follows from the distribution of multiplication over addition:

{{begin-eqn}}
{{eqn | l = \left({x + y}\right)^2
      | r = \left({x + y}\right) \cdot \left({x + y}\right)
}}
{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x^2 + 2xy + y^2
      | c =
}}
{{end-eqn}}
{{qed}}
-/
theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2) :=
begin
  calc (x + y)^2 = (x+y)*(x+y) : by rw sq
  ... = x*(x+y) + y*(x+y) : by rw add_mul
  ... = x*x + x*y + y*x + y*y : by {rw [mul_comm x (x+y),mul_comm y (x+y)], rw [add_mul,add_mul], ring}
  ... = x^2 + 2*x*y + y^2 : by {repeat {rw ← sq}, rw mul_comm y x, ring}
end

/--`theorem`
Identity of Group is Unique
Let $\struct {G, \circ}$ be a group. Then there is a unique identity element $e \in G$.
`proof`
From Group has Latin Square Property, there exists a unique $x \in G$ such that:
:$a x = b$

and there exists a unique $y \in G$ such that:
:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:
:$a x = a$

and there exists a unique $y \in G$ such that:
:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.
{{qed}}
-/
theorem group_identity_unique {G : Type*} [group G] : ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a :=
begin
  have h1 : ∀ a b : G, ∃! x : G, a * x = b, from by {
    assume a b : G, use a⁻¹ * b, obviously, },
  have h2 : ∀ a b : G, ∃! y : G, y * a = b, from by {
    assume a b : G, use b * a⁻¹, obviously, },

  have h3 : ∀ a : G, ∃! x : G, a * x = a, from
    assume a : G, h1 a a,
  have h4 : ∀ a : G, ∃! y : G, y * a = a, from
    assume a : G, h2 a a,

  have h5 : ∀ a : G, classical.some (h3 a).exists = (1 : G), from assume a :G,
    exists_unique.unique (h3 a) (classical.some_spec (exists_unique.exists (h3 a)))
    (mul_one a),
  have h6 : ∀ a : G, classical.some (h4 a).exists = (1 : G), from assume a : G,
    exists_unique.unique (h4 a) (classical.some_spec (exists_unique.exists (h4 a))) (one_mul a),

  show ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a, from by {
    use (1 : G),
    have h7 : ∀ e : G, (∀ a : G, e * a = a ∧ a * e = a) → e = 1, from by {
      assume (e : G) (hident : ∀ a : G, e * a = a ∧ a * e = a),
      have h8 : ∀ a : G, e = classical.some (h3 a).exists, from assume (a : G),
        exists_unique.unique (h3 a) (hident a).right
        (classical.some_spec (exists_unique.exists (h3 a))),
      have h9 : ∀ a : G, e = classical.some (h4 a).exists, from assume (a : G),
        exists_unique.unique (h4 a) (hident a).left
        (classical.some_spec (exists_unique.exists (h4 a))),
      show e = (1 : G), from eq.trans (h9 e) (h6 _),
    },
    exact ⟨by obviously, h7⟩,
  }
end

/--`theorem`
Density of irrational orbit
The fractional parts of the integer multiples of an irrational number form a dense subset of the unit interval
`proof`
Let $\alpha$ be an irrational number. Then for distinct $i, j \in \mathbb{Z}$, we must have $\{i \alpha\} \neq\{j \alpha\}$. If this were not true, then
$$
i \alpha-\lfloor i \alpha\rfloor=\{i \alpha\}=\{j \alpha\}=j \alpha-\lfloor j \alpha\rfloor,
$$
which yields the false statement $\alpha=\frac{\lfloor i \alpha\rfloor-\lfloor j \alpha\rfloor}{i-j} \in \mathbb{Q}$. Hence,
$$
S:=\{\{i \alpha\} \mid i \in \mathbb{Z}\}
$$
is an infinite subset of $\left[0,1\right]$.

By the Bolzano-Weierstrass theorem, $S$ has a limit point in $[0, 1]$. One can thus find pairs of elements of $S$ that are arbitrarily close. Since (the absolute value of) the difference of any two elements of $S$ is also an element of $S$, it follows that $0$ is a limit point of $S$.

To show that $S$ is dense in $[0, 1]$, consider $y \in[0,1]$, and $\epsilon>0$. Then by selecting $x \in S$ such that $\{x\}<\epsilon$ (which exists as $0$ is a limit point), and $N$ such that $N \cdot\{x\} \leq y<(N+1) \cdot\{x\}$, we get: $|y-\{N x\}|<\epsilon$.

QED
-/
theorem  irrational_orbit_dense {α : ℝ} (hα_irrat : irrational α) : closure ((λ m : ℤ, int.fract (α * ↑m)) '' (@set.univ ℤ)) = set.Icc 0 1 :=
FEW SHOT PROMPTS TO CODEX(END)-/


text:
/-
Copyright (c) 2020 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/
import measure_theory.measure.regular
import measure_theory.group.measurable_equiv
import measure_theory.measure.open_pos

/-!
# Measures on Groups

We develop some properties of measures on (topological) groups

* We define properties on measures: measures that are left or right invariant w.r.t. multiplication.
* We define the measure `μ.inv : A ↦ μ(A⁻¹)` and show that it is right invariant iff
  `μ` is left invariant.
* We define a class `is_haar_measure μ`, requiring that the measure `μ` is left-invariant, finite
  on compact sets, and positive on open sets.

We also give analogues of all these notions in the additive world.
-/

noncomputable theory

open_locale ennreal pointwise big_operators
open has_inv set function measure_theory.measure

variables {G : Type*} [measurable_space G]

namespace measure_theory
namespace measure

/-- A measure `μ` on a measurable additive group is left invariant
  if the measure of left translations of a set are equal to the measure of the set itself. -/
class is_add_left_invariant [has_add G] (μ : measure G) : Prop :=
( map_add_left_eq_self : ∀ g : G, map ((+) g) μ = μ)

/-- A measure `μ` on a measurable group is left invariant
  if the measure of left translations of a set are equal to the measure of the set itself. -/
@[to_additive] class is_mul_left_invariant [has_mul G] (μ : measure G) : Prop :=
( map_mul_left_eq_self : ∀ g : G, map ((*) g) μ = μ)

/-- A measure `μ` on a measurable additive group is right invariant
  if the measure of right translations of a set are equal to the measure of the set itself. -/
class is_add_right_invariant [has_add G] (μ : measure G) : Prop :=
(map_add_right_eq_self : ∀ g : G, map (+ g) μ = μ)

/-- A measure `μ` on a measurable group is right invariant
  if the measure of right translations of a set are equal to the measure of the set itself. -/
@[to_additive] class is_mul_right_invariant [has_mul G] (μ : measure G) : Prop :=
(map_mul_right_eq_self : ∀ g : G, map (* g) μ = μ)

end measure
open measure

section mul

variables [has_mul G] {μ : measure G}

@[to_additive]
lemma map_mul_left_eq_self (μ : measure G) [is_mul_left_invariant μ] (g : G) : map ((*) g) μ = μ :=
is_mul_left_invariant.map_mul_left_eq_self g

@[to_additive]
lemma map_mul_right_eq_self (μ : measure G) [is_mul_right_invariant μ] (g : G) : map (* g) μ = μ :=
is_mul_right_invariant.map_mul_right_eq_self g

/-- An alternative way to prove that `μ` is left invariant under multiplication. -/
@[to_additive]
lemma forall_measure_preimage_mul_iff [has_measurable_mul G] (μ : measure G) :
  (∀ (g : G) (A : set G), measurable_set A → μ ((λ h, g * h) ⁻¹' A) = μ A) ↔
  is_mul_left_invariant μ :=
begin
  transitivity ∀ g, map ((*) g) μ = μ,
  { simp_rw [measure.ext_iff],
    refine forall_congr (λ g, forall_congr $ λ A, forall_congr $ λ hA, _),
    rw [map_apply (measurable_const_mul g) hA] },
  exact ⟨λ h, ⟨h⟩, λ h, h.1⟩
end

/-- An alternative way to prove that `μ` is left invariant under multiplication. -/
@[to_additive]
lemma forall_measure_preimage_mul_right_iff [has_measurable_mul G] (μ : measure G) :
  (∀ (g : G) (A : set G), measurable_set A → μ ((λ h, h * g) ⁻¹' A) = μ A) ↔
  is_mul_right_invariant μ :=
begin
  transitivity ∀ g, map (* g) μ = μ,
  { simp_rw [measure.ext_iff],
    refine forall_congr (λ g, forall_congr $ λ A, forall_congr $ λ hA, _),
    rw [map_apply (measurable_mul_const g) hA] },
  exact ⟨λ h, ⟨h⟩, λ h, h.1⟩
end

@[to_additive]
instance [is_mul_left_invariant μ] (c : ℝ≥0∞) : is_mul_left_invariant (c • μ) :=
⟨λ g, by rw [map_smul, map_mul_left_eq_self]⟩

@[to_additive]
instance [is_mul_right_invariant μ] (c : ℝ≥0∞) : is_mul_right_invariant (c • μ) :=
⟨λ g, by rw [map_smul, map_mul_right_eq_self]⟩

end mul

section group

variables [group G]

@[to_additive]
lemma map_div_right_eq_self (μ : measure G) [is_mul_right_invariant μ] (g : G) :
  map (/ g) μ = μ :=
by simp_rw [div_eq_mul_inv, map_mul_right_eq_self μ g⁻¹]

variables [has_measurable_mul G]

/-- We shorten this from `measure_preimage_mul_left`, since left invariant is the preferred option
  for measures in this formalization. -/
@[simp, to_additive]
lemma measure_preimage_mul (μ : measure G) [is_mul_left_invariant μ] (g : G) (A : set G) :
  μ ((λ h, g * h) ⁻¹' A) = μ A :=
calc μ ((λ h, g * h) ⁻¹' A) = map (λ h, g * h) μ A :
  ((measurable_equiv.mul_left g).map_apply A).symm
... = μ A : by rw map_mul_left_eq_self μ g

@[simp, to_additive]
lemma measure_preimage_mul_right (μ : measure G) [is_mul_right_invariant μ] (g : G) (A : set G) :
  μ ((λ h, h * g) ⁻¹' A) = μ A :=
calc μ ((λ h, h * g) ⁻¹' A) = map (λ h, h * g) μ A :
  ((measurable_equiv.mul_right g).map_apply A).symm
... = μ A : by rw map_mul_right_eq_self μ g

end group

namespace measure

/-- The measure `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`. -/
@[to_additive "The measure `A ↦ μ (- A)`, where `- A` is the pointwise negation of `A`."]
protected def inv [has_inv G] (μ : measure G) : measure G :=
measure.map inv μ

/-- A measure is invariant under negation if `- μ = μ`. Equivalently, this means that for all
measurable `A` we have `μ (- A) = μ A`, where `- A` is the pointwise negation of `A`. -/
class is_neg_invariant [has_neg G] (μ : measure G) : Prop :=
(neg_eq_self : μ.neg = μ)

/-- A measure is invariant under inversion if `μ⁻¹ = μ`. Equivalently, this means that for all
measurable `A` we have `μ (A⁻¹) = μ A`, where `A⁻¹` is the pointwise inverse of `A`. -/
@[to_additive] class is_inv_invariant [has_inv G] (μ : measure G) : Prop :=
(inv_eq_self : μ.inv = μ)

section inv

variables [has_inv G]

@[simp, to_additive]
lemma inv_eq_self (μ : measure G) [is_inv_invariant μ] : μ.inv = μ :=
is_inv_invariant.inv_eq_self

@[simp, to_additive]
lemma map_inv_eq_self (μ : measure G) [is_inv_invariant μ] : map has_inv.inv μ = μ :=
is_inv_invariant.inv_eq_self

end inv

section has_involutive_inv

variables [has_involutive_inv G] [has_measurable_inv G]

@[simp, to_additive]
lemma inv_apply (μ : measure G) (s : set G) : μ.inv s = μ s⁻¹ :=
(measurable_equiv.inv G).map_apply s

@[simp, to_additive]
protected lemma inv_inv (μ : measure G) : μ.inv.inv = μ :=
(measurable_equiv.inv G).map_symm_map

@[simp, to_additive]
lemma measure_inv (μ : measure G) [is_inv_invariant μ] (A : set G) : μ A⁻¹ = μ A :=
by rw [← inv_apply, inv_eq_self]

@[to_additive]
lemma measure_preimage_inv (μ : measure G) [is_inv_invariant μ] (A : set G) :
  μ (has_inv.inv ⁻¹' A) = μ A :=
μ.measure_inv A

@[to_additive]
instance (μ : measure G) [sigma_finite μ] : sigma_finite μ.inv :=
(measurable_equiv.inv G).sigma_finite_map ‹_›

end has_involutive_inv

section mul_inv
variables [group G] [has_measurable_mul G] [has_measurable_inv G] {μ : measure G}

@[to_additive]
instance [is_mul_left_invariant μ] : is_mul_right_invariant μ.inv :=
begin
  constructor,
  intro g,
  conv_rhs { rw [← map_mul_left_eq_self μ g⁻¹] },
  simp_rw [measure.inv, map_map (measurable_mul_const g) measurable_inv,
    map_map measurable_inv (measurable_const_mul g⁻¹), function.comp, mul_inv_rev, inv_inv]
end

@[to_additive]
instance [is_mul_right_invariant μ] : is_mul_left_invariant μ.inv :=
begin
  constructor,
  intro g,
  conv_rhs { rw [← map_mul_right_eq_self μ g⁻¹] },
  simp_rw [measure.inv, map_map (measurable_const_mul g) measurable_inv,
    map_map measurable_inv (measurable_mul_const g⁻¹), function.comp, mul_inv_rev, inv_inv]
end

@[to_additive]
lemma map_div_left_eq_self (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ] (g : G) :
  map (λ t, g / t) μ = μ :=
begin
  simp_rw [div_eq_mul_inv],
  conv_rhs { rw [← map_mul_left_eq_self μ g, ← map_inv_eq_self μ] },
  exact (map_map (measurable_const_mul g) measurable_inv).symm
end

@[to_additive]
lemma map_mul_right_inv_eq_self (μ : measure G) [is_inv_invariant μ] [is_mul_left_invariant μ]
  (g : G) : map (λ t, (g * t)⁻¹) μ = μ :=
begin
  conv_rhs { rw [← map_inv_eq_self μ, ← map_mul_left_eq_self μ g] },
  exact (map_map measurable_inv (measurable_const_mul g)).symm
end

end mul_inv

end measure

section topological_group

variables [topological_space G] [borel_space G] {μ : measure G}
variables [group G] [topological_group G]

@[to_additive]
instance measure.regular.inv [t2_space G] [regular μ] : regular μ.inv :=
regular.map (homeomorph.inv G)

@[to_additive]
lemma regular_inv_iff [t2_space G] : μ.inv.regular ↔ μ.regular :=
begin
  split,
  { introI h, rw ← μ.inv_inv, exact measure.regular.inv },
  { introI h, exact measure.regular.inv }
end

variables [is_mul_left_invariant μ]
/-- If a left-invariant measure gives positive mass to a compact set, then
it gives positive mass to any open set. -/
@[to_additive]
lemma is_open_pos_measure_of_mul_left_invariant_of_compact
  (K : set G) (hK : is_compact K) (h : μ K ≠ 0) :
  is_open_pos_measure μ :=
begin
  refine ⟨λ U hU hne, _⟩,
  contrapose! h,
  rw ← nonpos_iff_eq_zero,
  rw ← hU.interior_eq at hne,
  obtain ⟨t, hKt⟩ : ∃ (t : finset G), K ⊆ ⋃ (g : G) (H : g ∈ t), (λ (h : G), g * h) ⁻¹' U :=
    compact_covered_by_mul_left_translates hK hne,
  calc μ K ≤ μ (⋃ (g : G) (H : g ∈ t), (λ (h : G), g * h) ⁻¹' U) : measure_mono hKt
  ... ≤ ∑ g in t, μ ((λ (h : G), g * h) ⁻¹' U) : measure_bUnion_finset_le _ _
  ... = 0 : by simp [measure_preimage_mul, h]
end

/-- A nonzero left-invariant regular measure gives positive mass to any open set. -/
@[to_additive]
lemma is_open_pos_measure_of_mul_left_invariant_of_regular [regular μ] (h₀ : μ ≠ 0) :
  is_open_pos_measure μ :=
let ⟨K, hK, h2K⟩ := regular.exists_compact_not_null.mpr h₀
in is_open_pos_measure_of_mul_left_invariant_of_compact K hK h2K

@[to_additive]
lemma null_iff_of_is_mul_left_invariant [regular μ]
  {s : set G} (hs : is_open s) :
  μ s = 0 ↔ s = ∅ ∨ μ = 0 :=
begin
  by_cases h3μ : μ = 0, { simp [h3μ] },
  { haveI := is_open_pos_measure_of_mul_left_invariant_of_regular h3μ,
    simp only [h3μ, or_false, hs.measure_eq_zero_iff μ] },
end

@[to_additive]
lemma measure_ne_zero_iff_nonempty_of_is_mul_left_invariant [regular μ]
  (hμ : μ ≠ 0) {s : set G} (hs : is_open s) :
  μ s ≠ 0 ↔ s.nonempty :=
by simpa [null_iff_of_is_mul_left_invariant hs, hμ] using ne_empty_iff_nonempty

@[to_additive]
lemma measure_pos_iff_nonempty_of_is_mul_left_invariant [regular μ]
  (h3μ : μ ≠ 0) {s : set G} (hs : is_open s) :
  0 < μ s ↔ s.nonempty :=
pos_iff_ne_zero.trans $ measure_ne_zero_iff_nonempty_of_is_mul_left_invariant h3μ hs

/-- If a left-invariant measure gives finite mass to a nonempty open set, then
it gives finite mass to any compact set. -/
@[to_additive]
lemma measure_lt_top_of_is_compact_of_is_mul_left_invariant
  (U : set G) (hU : is_open U) (h'U : U.nonempty) (h : μ U ≠ ∞) {K : set G} (hK : is_compact K) :
  μ K < ∞ :=
begin
  rw ← hU.interior_eq at h'U,
  obtain ⟨t, hKt⟩ : ∃ (t : finset G), K ⊆ ⋃ (g : G) (H : g ∈ t), (λ (h : G), g * h) ⁻¹' U :=
    compact_covered_by_mul_left_translates hK h'U,
  calc μ K ≤ μ (⋃ (g : G) (H : g ∈ t), (λ (h : G), g * h) ⁻¹' U) : measure_mono hKt
  ... ≤ ∑ g in t, μ ((λ (h : G), g * h) ⁻¹' U) : measure_bUnion_finset_le _ _
  ... = finset.card t * μ U : by simp only [measure_preimage_mul, finset.sum_const, nsmul_eq_mul]
  ... < ∞ : ennreal.mul_lt_top ennreal.coe_nat_ne_top h
end

/-- If a left-invariant measure gives finite mass to a set with nonempty interior, then
it gives finite mass to any compact set. -/
@[to_additive]
lemma measure_lt_top_of_is_compact_of_is_mul_left_invariant'
  {U : set G} (hU : (interior U).nonempty) (h : μ U ≠ ∞) {K : set G} (hK : is_compact K) :
  μ K < ∞ :=
measure_lt_top_of_is_compact_of_is_mul_left_invariant (interior U) is_open_interior hU
  ((measure_mono (interior_subset)).trans_lt (lt_top_iff_ne_top.2 h)).ne hK

end topological_group

section comm_group

variables [comm_group G]

/-- In an abelian group every left invariant measure is also right-invariant.
  We don't declare the converse as an instance, since that would loop type-class inference, and
  we use `is_mul_left_invariant` as default hypotheses in abelian groups. -/
@[priority 100, to_additive]
instance is_mul_left_invariant.is_mul_right_invariant {μ : measure G} [is_mul_left_invariant μ] :
  is_mul_right_invariant μ :=
⟨λ g, by simp_rw [mul_comm, map_mul_left_eq_self]⟩

end comm_group

section haar

namespace measure

/-- A measure on an additive group is an additive Haar measure if it is left-invariant, and gives
finite mass to compact sets and positive mass to open sets. -/
class is_add_haar_measure {G : Type*} [add_group G] [topological_space G] [measurable_space G]
  (μ : measure G)
  extends is_finite_measure_on_compacts μ, is_add_left_invariant μ, is_open_pos_measure μ : Prop

/-- A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact
sets and positive mass to open sets. -/
@[to_additive]
class is_haar_measure {G : Type*} [group G] [topological_space G] [measurable_space G]
  (μ : measure G)
  extends is_finite_measure_on_compacts μ, is_mul_left_invariant μ, is_open_pos_measure μ : Prop

/- Record that a Haar measure on a locally compact space is locally finite. This is needed as the
fact that a measure which is finite on compacts is locally finite is not registered as an instance,
to avoid an instance loop. -/
@[priority 100, to_additive] -- see Note [lower instance priority]
instance is_locally_finite_measure_of_is_haar_measure {G : Type*}
  [group G] [measurable_space G] [topological_space G] [locally_compact_space G]
  (μ : measure G) [is_haar_measure μ] :
  is_locally_finite_measure μ :=
is_locally_finite_measure_of_is_finite_measure_on_compacts

section

variables [group G] [topological_space G] (μ : measure G) [is_haar_measure μ]

@[simp, to_additive]
lemma haar_singleton [topological_group G] [borel_space G] (g : G) :
  μ {g} = μ {(1 : G)} :=
begin
  convert measure_preimage_mul μ (g⁻¹) _,
  simp only [mul_one, preimage_mul_left_singleton, inv_inv],
end

@[to_additive measure_theory.measure.is_add_haar_measure.smul]
lemma is_haar_measure.smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) :
  is_haar_measure (c • μ) :=
{ lt_top_of_is_compact := λ K hK, ennreal.mul_lt_top ctop hK.measure_lt_top.ne,
  to_is_open_pos_measure := is_open_pos_measure_smul μ cpos }

/-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then
it is a Haar measure -/
@[to_additive]
lemma is_haar_measure_of_is_compact_nonempty_interior [topological_group G] [borel_space G]
  (μ : measure G) [is_mul_left_invariant μ]
  (K : set G) (hK : is_compact K) (h'K : (interior K).nonempty) (h : μ K ≠ 0) (h' : μ K ≠ ∞) :
  is_haar_measure μ :=
{ lt_top_of_is_compact :=
    λ L hL, measure_lt_top_of_is_compact_of_is_mul_left_invariant' h'K h' hL,
  to_is_open_pos_measure := is_open_pos_measure_of_mul_left_invariant_of_compact K hK h }

/-- The image of a Haar measure under a group homomorphism which is also a homeomorphism is again
a Haar measure. -/
@[to_additive]
lemma is_haar_measure_map [borel_space G] [topological_group G] {H : Type*} [group H]
  [topological_space H] [measurable_space H] [borel_space H] [t2_space H] [topological_group H]
  (f : G ≃* H) (hf : continuous f) (hfsymm : continuous f.symm) :
  is_haar_measure (measure.map f μ) :=
{ to_is_mul_left_invariant := begin
    constructor,
    assume h,
    rw map_map (continuous_mul_left h).measurable hf.measurable,
    conv_rhs { rw ← map_mul_left_eq_self μ (f.symm h) },
    rw map_map hf.measurable (continuous_mul_left _).measurable,
    congr' 2,
    ext y,
    simp only [mul_equiv.apply_symm_apply, comp_app, mul_equiv.map_mul],
  end,
  lt_top_of_is_compact := begin
    assume K hK,
    rw map_apply hf.measurable hK.measurable_set,
    have : f.symm '' K = f ⁻¹' K := equiv.image_eq_preimage _ _,
    rw ← this,
    exact is_compact.measure_lt_top (hK.image hfsymm)
  end,
  to_is_open_pos_measure := hf.is_open_pos_measure_map f.surjective }

/-- A Haar measure on a sigma-compact space is sigma-finite. -/
@[priority 100, to_additive] -- see Note [lower instance priority]
instance is_haar_measure.sigma_finite [sigma_compact_space G] : sigma_finite μ :=
⟨⟨{ set := compact_covering G,
  set_mem := λ n, mem_univ _,
  finite := λ n, is_compact.measure_lt_top $ is_compact_compact_covering G n,
  spanning := Union_compact_covering G }⟩⟩

open_locale topological_space
open filter

/-- If the neutral element of a group is not isolated, then a Haar measure on this group has
no atom.

This applies in particular to show that an additive Haar measure on a nontrivial
finite-dimensional real vector space has no atom. -/
@[priority 100, to_additive]
instance is_haar_measure.has_no_atoms [topological_group G] [borel_space G]
  [t1_space G] [locally_compact_space G] [(𝓝[≠] (1 : G)).ne_bot]
  (μ : measure G) [μ.is_haar_measure] :
  has_no_atoms μ :=
begin
  suffices H : μ {(1 : G)} ≤ 0, by { constructor, simp [le_bot_iff.1 H] },
  obtain ⟨K, K_compact, K_int⟩ : ∃ (K : set G), is_compact K ∧ (1 : G) ∈ interior K,
  { rcases exists_compact_subset is_open_univ (mem_univ (1 : G)) with ⟨K, hK⟩,
    exact ⟨K, hK.1, hK.2.1⟩ },
  have K_inf : set.infinite K := infinite_of_mem_nhds (1 : G) (mem_interior_iff_mem_nhds.1 K_int),
  have μKlt : μ K ≠ ∞ := K_compact.measure_lt_top.ne,
  have I : ∀ (n : ℕ), μ {(1 : G)} ≤ μ K / n,
  { assume n,
    obtain ⟨t, tK, tn⟩ : ∃ (t : finset G), ↑t ⊆ K ∧ t.card = n := K_inf.exists_subset_card_eq n,
    have A : μ t ≤ μ K := measure_mono tK,
    have B : μ t = n * μ {(1 : G)},
    { rw ← bUnion_of_singleton ↑t,
      change μ (⋃ (x ∈ t), {x}) = n * μ {1},
      rw @measure_bUnion_finset G G _ μ t (λ i, {i}),
      { simp only [tn, finset.sum_const, nsmul_eq_mul, haar_singleton] },
      { assume x hx y hy xy,
        simp only [on_fun, xy.symm, mem_singleton_iff, not_false_iff, disjoint_singleton_right] },
      { assume b hb, exact measurable_set_singleton b } },
    rw B at A,
    rwa [ennreal.le_div_iff_mul_le _ (or.inr μKlt), mul_comm],
    right,
    apply (measure_pos_of_nonempty_interior μ ⟨_, K_int⟩).ne' },
  have J : tendsto (λ (n : ℕ),  μ K / n) at_top (𝓝 (μ K / ∞)) :=
    ennreal.tendsto.const_div ennreal.tendsto_nat_nhds_top (or.inr μKlt),
  simp only [ennreal.div_top] at J,
  exact ge_of_tendsto' J I,
end

/- The above instance applies in particular to show that an additive Haar measure on a nontrivial
finite-dimensional real vector space has no atom. -/
example {E : Type*} [normed_group E] [normed_space ℝ E] [nontrivial E] [finite_dimensional ℝ E]
  [measurable_space E] [borel_space E] (μ : measure E) [is_add_haar_measure μ] :
  has_no_atoms μ := by apply_instance

end

end measure
end haar

end measure_theory

author: saisurbehera

repo: mathProof


text:
/-  Math40001 : Introduction to university mathematics.

Problem Sheet 1, October 2019.

This is a Lean file. It can be read with the Lean theorem prover.

You can work on this file online at
https://tinyurl.com/Lean-M40001-Example-Sheet-1

or you can install Lean and its maths library following the
instructions at
https://github.com/leanprover-community/mathlib#installation

There are advantages to installing Lean on your own computer
(for example it's faster), but it's more hassle than
just using it online.

In the below, delete "sorry" and replace it with some
tactics which prove the result.

-/

/- Question 1.

Let P and Q be Propositions (that is, true/false statements).
Prove that P ∧ Q → Q ∧ P.

-/

lemma question_one (P Q : Prop) : P ∧ Q → Q ∧ P :=
begin
  sorry
end
/-

For question 2, comment out one option (or just delete it)
and prove the other one.
-/

-- Part (a): is → symmetric?

lemma question_2a_true : ∀ P Q : Prop, (P → Q) → (Q → P) :=
begin
  sorry
end

lemma question_2a_false : ¬ (∀ P Q : Prop, (P → Q) → (Q → P)) :=
begin
  sorry
end

-- Part (b) : is ↔ symmetric?

lemma question_2b_true (P Q : Prop) : (P ↔ Q) → (Q ↔ P) :=
begin
  sorry
end

lemma question_2b_false : ¬ (∀ P Q : Prop, (P ↔ Q) → (Q ↔ P)) :=
begin
  sorry
end

/- Question 3.

Say P, Q and R are propositions, and we know:
1) if Q is true then P is true
2) If Q is false then R is false.

Can we deduce that R implies P? Comment out one
option and prove the other. Hint: if you're stuck,
"apply classical.by_contradiction" sometimes helps.
classical.by_contradiction is the theorem that ¬ ¬ P → P.
-/

lemma question_3_true (P Q R : Prop)
  (h1 : Q → P)
  (h2 : ¬ Q → ¬ R) :
R → P :=
begin
  sorry
end

lemma question_3_false : ¬ (∀ P Q R : Prop,
  (Q → P) →
  (¬ Q → ¬ R) →
  R → P) :=
begin
  sorry
end

/- Question 4.

   Your friend is thinking of three true-false statements P, Q and R,
   and they tell you the following facts:
   a) P → (Q ∧ R)
   b) Q → (R ∧ ¬ P)
   c) R → (P ∧ ¬ Q)

   What can you deduce?

In this question you must *change the conclusion* to explain
   what you deduced.
-/

lemma question_4 (P Q R : Prop)
  (h1 : P → (Q ∧ R))
  (h2 : Q → (R ∧ ¬ P))
  (h3 : R → (P ∧ ¬ Q)) :
P ∨ Q  -- replace this line with your conclusion
:=
begin
  sorry
end

/- Question 5.

  Say that for every integer n we have a proposition P n.
  Say we know P n → P (n + 8) for all n, and
  P n → P (n -3) for all n. Prove that the P n are either
  all true, or all false.

This question is harder than the others.
-/
lemma question_5 (P : ℤ → Prop) (h8 : ∀ n, P n → P (n + 8)) (h3 : ∀ n, P n → P (n - 3)) :
(∀ n, P n) ∨ (∀ n, ¬ (P n)) :=
begin
  sorry
end

/-
The first four of these questions can be solved using only the following
tactics:

intro
apply (or, better, refine)
left, right, cases, split
assumption (or, better, exact)
have,
simp
contradiction (or, better, false.elim)

The fifth question is harder.
-/

author: ImperialCollegeLondon


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
-/
import group_theory.group_action.defs
import group_theory.group_action.group
import group_theory.quotient_group
import data.setoid.basic
import data.fintype.card

/-!
# Basic properties of group actions
-/

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

open_locale big_operators pointwise
open function

namespace mul_action

variables (α) [monoid α] [mul_action α β]

/-- The orbit of an element under an action. -/
@[to_additive "The orbit of an element under an action."]
def orbit (b : β) := set.range (λ x : α, x • b)

variable {α}

@[to_additive] lemma mem_orbit_iff {b₁ b₂ : β} : b₂ ∈ orbit α b₁ ↔ ∃ x : α, x • b₁ = b₂ :=
iff.rfl

@[simp, to_additive] lemma mem_orbit (b : β) (x : α) : x • b ∈ orbit α b :=
⟨x, rfl⟩

@[simp, to_additive] lemma mem_orbit_self (b : β) : b ∈ orbit α b :=
⟨1, by simp [mul_action.one_smul]⟩

@[to_additive] lemma orbit_nonempty (b : β) : set.nonempty (orbit α b) := set.range_nonempty _

@[to_additive] lemma maps_to_smul_orbit (a : α) (b : β) :
  set.maps_to ((•) a) (orbit α b) (orbit α b) :=
set.range_subset_iff.2 $ λ a', ⟨a * a', mul_smul _ _ _⟩

@[to_additive] lemma smul_orbit_subset (a : α) (b : β) : a • orbit α b ⊆ orbit α b :=
(maps_to_smul_orbit a b).image_subset

@[to_additive] lemma orbit_smul_subset (a : α) (b : β) : orbit α (a • b) ⊆ orbit α b :=
set.range_subset_iff.2 $ λ a', mul_smul a' a b ▸ mem_orbit _ _

@[to_additive] instance {b : β} : mul_action α (orbit α b) :=
{ smul := λ a, (maps_to_smul_orbit a b).restrict _ _ _,
  one_smul := λ a, subtype.ext (one_smul α a),
  mul_smul := λ a a' b', subtype.ext (mul_smul a a' b') }

@[simp, to_additive] lemma orbit.coe_smul {b : β} {a : α} {b' : orbit α b} :
  ↑(a • b') = a • (b' : β) :=
rfl

variables (α) (β)

/-- The set of elements fixed under the whole action. -/
@[to_additive "The set of elements fixed under the whole action."]
def fixed_points : set β := {b : β | ∀ x : α, x • b = b}

/-- `fixed_by g` is the subfield of elements fixed by `g`. -/
@[to_additive "`fixed_by g` is the subfield of elements fixed by `g`."]
def fixed_by (g : α) : set β :=
{ x | g • x = x }

@[to_additive] theorem fixed_eq_Inter_fixed_by : fixed_points α β = ⋂ g : α, fixed_by α β g :=
set.ext $ λ x, ⟨λ hx, set.mem_Inter.2 $ λ g, hx g, λ hx g, by exact (set.mem_Inter.1 hx g : _)⟩

variables {α} (β)

@[simp, to_additive] lemma mem_fixed_points {b : β} :
  b ∈ fixed_points α β ↔ ∀ x : α, x • b = b := iff.rfl

@[simp, to_additive] lemma mem_fixed_by {g : α} {b : β} :
  b ∈ fixed_by α β g ↔ g • b = b := iff.rfl

@[to_additive] lemma mem_fixed_points' {b : β} : b ∈ fixed_points α β ↔
  (∀ b', b' ∈ orbit α b → b' = b) :=
⟨λ h b h₁, let ⟨x, hx⟩ := mem_orbit_iff.1 h₁ in hx ▸ h x,
λ h b, h _ (mem_orbit _ _)⟩

variables (α) {β}

/-- The stabilizer of a point `b` as a submonoid of `α`. -/
@[to_additive "The stabilizer of a point `b` as an additive submonoid of `α`."]
def stabilizer.submonoid (b : β) : submonoid α :=
{ carrier := { a | a • b = b },
  one_mem' := one_smul _ b,
  mul_mem' := λ a a' (ha : a • b = b) (hb : a' • b = b),
    show (a * a') • b = b, by rw [←smul_smul, hb, ha] }

@[simp, to_additive] lemma mem_stabilizer_submonoid_iff {b : β} {a : α} :
  a ∈ stabilizer.submonoid α b ↔ a • b = b := iff.rfl

@[to_additive] lemma orbit_eq_univ [is_pretransitive α β] (x : β) :
  orbit α x = set.univ :=
(surjective_smul α x).range_eq

end mul_action

namespace mul_action
variable (α)
variables [group α] [mul_action α β]

/-- The stabilizer of an element under an action, i.e. what sends the element to itself.
A subgroup. -/
@[to_additive "The stabilizer of an element under an action, i.e. what sends the element to itself.
An additive subgroup."]
def stabilizer (b : β) : subgroup α :=
{ inv_mem' := λ a (ha : a • b = b), show a⁻¹ • b = b, by rw [inv_smul_eq_iff, ha]
  ..stabilizer.submonoid α b }

variables {α} {β}

@[simp, to_additive] lemma mem_stabilizer_iff {b : β} {a : α} :
  a ∈ stabilizer α b ↔ a • b = b := iff.rfl

@[simp, to_additive] lemma smul_orbit (a : α) (b : β) :
  a • orbit α b = orbit α b :=
(smul_orbit_subset a b).antisymm $
  calc orbit α b = a • a⁻¹ • orbit α b : (smul_inv_smul _ _).symm
             ... ⊆ a • orbit α b       : set.image_subset _ (smul_orbit_subset _ _)

@[simp, to_additive] lemma orbit_smul (a : α) (b : β) : orbit α (a • b) = orbit α b :=
(orbit_smul_subset a b).antisymm $
  calc orbit α b = orbit α (a⁻¹ • a • b) : by rw inv_smul_smul
             ... ⊆ orbit α (a • b)       : orbit_smul_subset _ _

/-- The action of a group on an orbit is transitive. -/
@[to_additive "The action of an additive group on an orbit is transitive."]
instance (x : β) : is_pretransitive α (orbit α x) :=
⟨by { rintro ⟨_, a, rfl⟩ ⟨_, b, rfl⟩, use b * a⁻¹, ext1, simp [mul_smul] }⟩

@[to_additive] lemma orbit_eq_iff {a b : β} :
   orbit α a = orbit α b ↔ a ∈ orbit α b:=
⟨λ h, h ▸ mem_orbit_self _, λ ⟨c, hc⟩, hc ▸ orbit_smul _ _⟩

@[to_additive] lemma mem_fixed_points_iff_card_orbit_eq_one {a : β}
  [fintype (orbit α a)] : a ∈ fixed_points α β ↔ fintype.card (orbit α a) = 1 :=
begin
  rw [fintype.card_eq_one_iff, mem_fixed_points],
  split,
  { exact λ h, ⟨⟨a, mem_orbit_self _⟩, λ ⟨b, ⟨x, hx⟩⟩, subtype.eq $ by simp [h x, hx.symm]⟩ },
  { assume h x,
    rcases h with ⟨⟨z, hz⟩, hz₁⟩,
    calc x • a = z : subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩)
      ... = a : (subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm }
end

variables (α) {β}

@[to_additive] lemma mem_orbit_smul (g : α) (a : β) : a ∈ orbit α (g • a) :=
by simp only [orbit_smul, mem_orbit_self]

@[to_additive] lemma smul_mem_orbit_smul (g h : α) (a : β) : g • a ∈ orbit α (h • a) :=
by simp only [orbit_smul, mem_orbit]

variables (α) (β)
/-- The relation 'in the same orbit'. -/
@[to_additive "The relation 'in the same orbit'."]
def orbit_rel : setoid β :=
{ r := λ a b, a ∈ orbit α b,
  iseqv := ⟨mem_orbit_self, λ a b, by simp [orbit_eq_iff.symm, eq_comm],
    λ a b, by simp [orbit_eq_iff.symm, eq_comm] {contextual := tt}⟩ }

local notation `Ω` := (quotient $ orbit_rel α β)

/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action.
This version works with any right inverse to `quotient.mk'` in order to stay computable. In most
cases you'll want to use `quotient.out'`, so we provide `mul_action.self_equiv_sigma_orbits` as
a special case. -/
@[to_additive "Decomposition of a type `X` as a disjoint union of its orbits under an additive group
action. This version works with any right inverse to `quotient.mk'` in order to stay computable.
In most cases you'll want to use `quotient.out'`, so we provide `add_action.self_equiv_sigma_orbits`
as a special case."]
def self_equiv_sigma_orbits' {φ : Ω → β} (hφ : right_inverse φ quotient.mk') :
  β ≃ Σ (ω : Ω), orbit α (φ ω) :=
calc  β
    ≃ Σ (ω : Ω), {b // quotient.mk' b = ω} : (equiv.sigma_preimage_equiv quotient.mk').symm
... ≃ Σ (ω : Ω), orbit α (φ ω) :
        equiv.sigma_congr_right (λ ω, equiv.subtype_equiv_right $
          λ x, by {rw [← hφ ω, quotient.eq', hφ ω], refl })

/-- Decomposition of a type `X` as a disjoint union of its orbits under a group action. -/
@[to_additive "Decomposition of a type `X` as a disjoint union of its orbits under an additive group
action."]
noncomputable def self_equiv_sigma_orbits : β ≃ Σ (ω : Ω), orbit α ω.out' :=
self_equiv_sigma_orbits' α β quotient.out_eq'

variables {α β}

/-- If the stabilizer of `x` is `S`, then the stabilizer of `g • x` is `gSg⁻¹`. -/
lemma stabilizer_smul_eq_stabilizer_map_conj (g : α) (x : β) :
  (stabilizer α (g • x) = (stabilizer α x).map (mul_aut.conj g).to_monoid_hom) :=
begin
  ext h,
  rw [mem_stabilizer_iff, ← smul_left_cancel_iff g⁻¹, smul_smul, smul_smul, smul_smul, mul_left_inv,
      one_smul, ← mem_stabilizer_iff, subgroup.mem_map_equiv, mul_aut.conj_symm_apply]
end

/-- A bijection between the stabilizers of two elements in the same orbit. -/
noncomputable def stabilizer_equiv_stabilizer_of_orbit_rel {x y : β} (h : (orbit_rel α β).rel x y) :
  stabilizer α x ≃* stabilizer α y :=
let g : α := classical.some h in
have hg : g • y = x := classical.some_spec h,
have this : stabilizer α x = (stabilizer α y).map (mul_aut.conj g).to_monoid_hom,
  by rw [← hg, stabilizer_smul_eq_stabilizer_map_conj],
(mul_equiv.subgroup_congr this).trans ((mul_aut.conj g).subgroup_equiv_map $ stabilizer α y).symm

end mul_action

namespace add_action

variables [add_group α] [add_action α β]

/-- If the stabilizer of `x` is `S`, then the stabilizer of `g +ᵥ x` is `g + S + (-g)`. -/
lemma stabilizer_vadd_eq_stabilizer_map_conj (g : α) (x : β) :
  (stabilizer α (g +ᵥ x) = (stabilizer α x).map (add_aut.conj g).to_add_monoid_hom) :=
begin
  ext h,
  rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g) , vadd_vadd, vadd_vadd, vadd_vadd,
      add_left_neg, zero_vadd, ← mem_stabilizer_iff, add_subgroup.mem_map_equiv,
      add_aut.conj_symm_apply]
end

/-- A bijection between the stabilizers of two elements in the same orbit. -/
noncomputable def stabilizer_equiv_stabilizer_of_orbit_rel {x y : β}
  (h : (orbit_rel α β).rel x y) :
  stabilizer α x ≃+ stabilizer α y :=
let g : α := classical.some h in
have hg : g +ᵥ y = x := classical.some_spec h,
have this : stabilizer α x = (stabilizer α y).map (add_aut.conj g).to_add_monoid_hom,
  by rw [← hg, stabilizer_vadd_eq_stabilizer_map_conj],
(add_equiv.add_subgroup_congr this).trans
  ((add_aut.conj g).add_subgroup_equiv_map $ stabilizer α y).symm

end add_action

namespace mul_action

variables [group α] [mul_action α β]

open quotient_group

/-- Action on left cosets. -/
@[to_additive "Action on left cosets."]
def mul_left_cosets (H : subgroup α)
  (x : α) (y : α ⧸ H) : α ⧸ H :=
quotient.lift_on' y (λ y, quotient_group.mk ((x : α) * y))
  (λ a b (hab : _ ∈ H), quotient_group.eq.2
    (by rwa [mul_inv_rev, ← mul_assoc, mul_assoc (a⁻¹), inv_mul_self, mul_one]))

@[to_additive] instance quotient (H : subgroup α) : mul_action α (α ⧸ H) :=
{ smul := mul_left_cosets H,
  one_smul := λ a, quotient.induction_on' a (λ a, quotient_group.eq.2
    (by simp [subgroup.one_mem])),
  mul_smul := λ x y a, quotient.induction_on' a (λ a, quotient_group.eq.2
    (by simp [mul_inv_rev, subgroup.one_mem, mul_assoc])) }

@[simp, to_additive] lemma quotient.smul_mk (H : subgroup α) (a x : α) :
  (a • quotient_group.mk x : α ⧸ H) = quotient_group.mk (a * x) := rfl

@[simp, to_additive] lemma quotient.smul_coe (H : subgroup α) (a x : α) :
  (a • x : α ⧸ H) = ↑(a * x) := rfl

@[to_additive] instance mul_left_cosets_comp_subtype_val (H I : subgroup α) :
  mul_action I (α ⧸ H) :=
mul_action.comp_hom (α ⧸ H) (subgroup.subtype I)

variables (α) {β} (x : β)

/-- The canonical map from the quotient of the stabilizer to the set. -/
@[to_additive "The canonical map from the quotient of the stabilizer to the set. "]
def of_quotient_stabilizer (g : α ⧸ (mul_action.stabilizer α x)) : β :=
quotient.lift_on' g (•x) $ λ g1 g2 H,
calc  g1 • x
    = g1 • (g1⁻¹ * g2) • x : congr_arg _ H.symm
... = g2 • x : by rw [smul_smul, mul_inv_cancel_left]

@[simp, to_additive] theorem of_quotient_stabilizer_mk (g : α) :
  of_quotient_stabilizer α x (quotient_group.mk g) = g • x :=
rfl

@[to_additive] theorem of_quotient_stabilizer_mem_orbit (g) :
  of_quotient_stabilizer α x g ∈ orbit α x :=
quotient.induction_on' g $ λ g, ⟨g, rfl⟩

@[to_additive] theorem of_quotient_stabilizer_smul (g : α)
  (g' : α ⧸ (mul_action.stabilizer α x)) :
  of_quotient_stabilizer α x (g • g') = g • of_quotient_stabilizer α x g' :=
quotient.induction_on' g' $ λ _, mul_smul _ _ _

@[to_additive] theorem injective_of_quotient_stabilizer :
  function.injective (of_quotient_stabilizer α x) :=
λ y₁ y₂, quotient.induction_on₂' y₁ y₂ $ λ g₁ g₂ (H : g₁ • x = g₂ • x), quotient.sound' $
show (g₁⁻¹ * g₂) • x = x, by rw [mul_smul, ← H, inv_smul_smul]

/-- Orbit-stabilizer theorem. -/
@[to_additive "Orbit-stabilizer theorem."]
noncomputable def orbit_equiv_quotient_stabilizer (b : β) :
  orbit α b ≃ α ⧸ (stabilizer α b) :=
equiv.symm $ equiv.of_bijective
  (λ g, ⟨of_quotient_stabilizer α b g, of_quotient_stabilizer_mem_orbit α b g⟩)
  ⟨λ x y hxy, injective_of_quotient_stabilizer α b (by convert congr_arg subtype.val hxy),
  λ ⟨b, ⟨g, hgb⟩⟩, ⟨g, subtype.eq hgb⟩⟩

/-- Orbit-stabilizer theorem. -/
@[to_additive "Orbit-stabilizer theorem."]
noncomputable def orbit_prod_stabilizer_equiv_group (b : β) :
  orbit α b × stabilizer α b ≃ α :=
(equiv.prod_congr (orbit_equiv_quotient_stabilizer α _) (equiv.refl _)).trans
subgroup.group_equiv_quotient_times_subgroup.symm

/-- Orbit-stabilizer theorem. -/
@[to_additive "Orbit-stabilizer theorem."]
lemma card_orbit_mul_card_stabilizer_eq_card_group (b : β) [fintype α] [fintype $ orbit α b]
  [fintype $ stabilizer α b] :
  fintype.card (orbit α b) * fintype.card (stabilizer α b) = fintype.card α :=
by rw [← fintype.card_prod, fintype.card_congr (orbit_prod_stabilizer_equiv_group α b)]

@[simp, to_additive] theorem orbit_equiv_quotient_stabilizer_symm_apply (b : β) (a : α) :
  ((orbit_equiv_quotient_stabilizer α b).symm a : β) = a • b :=
rfl

@[simp, to_additive] lemma stabilizer_quotient {G} [group G] (H : subgroup G) :
  mul_action.stabilizer G ((1 : G) : G ⧸ H) = H :=
by { ext, simp [quotient_group.eq] }

variable (β)

local notation `Ω` := (quotient $ orbit_rel α β)

/-- **Class formula** : given `G` a group acting on `X` and `φ` a function mapping each orbit of `X`
under this action (that is, each element of the quotient of `X` by the relation `orbit_rel G X`) to
an element in this orbit, this gives a (noncomputable) bijection between `X` and the disjoint union
of `G/Stab(φ(ω))` over all orbits `ω`. In most cases you'll want `φ` to be `quotient.out'`, so we
provide `mul_action.self_equiv_sigma_orbits_quotient_stabilizer` as a special case. -/
@[to_additive "**Class formula** : given `G` an additive group acting on `X` and `φ` a function
mapping each orbit of `X` under this action (that is, each element of the quotient of `X` by the
relation `orbit_rel G X`) to an element in this orbit, this gives a (noncomputable) bijection
between `X` and the disjoint union of `G/Stab(φ(ω))` over all orbits `ω`. In most cases you'll want
`φ` to be `quotient.out'`, so we provide `add_action.self_equiv_sigma_orbits_quotient_stabilizer`
as a special case. "]
noncomputable def self_equiv_sigma_orbits_quotient_stabilizer' {φ : Ω → β}
  (hφ : left_inverse quotient.mk' φ) : β ≃ Σ (ω : Ω), α ⧸ (stabilizer α (φ ω)) :=
calc  β
    ≃ Σ (ω : Ω), orbit α (φ ω) : self_equiv_sigma_orbits' α β hφ
... ≃ Σ (ω : Ω), α ⧸ (stabilizer α (φ ω)) :
        equiv.sigma_congr_right (λ ω, orbit_equiv_quotient_stabilizer α (φ ω))

/-- **Class formula** for a finite group acting on a finite type. See
`mul_action.card_eq_sum_card_group_div_card_stabilizer` for a specialized version using
`quotient.out'`. -/
@[to_additive "**Class formula** for a finite group acting on a finite type. See
`add_action.card_eq_sum_card_add_group_div_card_stabilizer` for a specialized version using
`quotient.out'`."]
lemma card_eq_sum_card_group_div_card_stabilizer' [fintype α] [fintype β] [fintype Ω]
  [Π (b : β), fintype $ stabilizer α b] {φ : Ω → β} (hφ : left_inverse quotient.mk' φ) :
  fintype.card β = ∑ (ω : Ω), fintype.card α / fintype.card (stabilizer α (φ ω)) :=
begin
  classical,
  have : ∀ ω : Ω, fintype.card α / fintype.card ↥(stabilizer α (φ ω)) =
    fintype.card (α ⧸ stabilizer α (φ ω)),
  { intro ω,
    rw [fintype.card_congr (@subgroup.group_equiv_quotient_times_subgroup α _ (stabilizer α $ φ ω)),
        fintype.card_prod, nat.mul_div_cancel],
    exact fintype.card_pos_iff.mpr (by apply_instance) },
  simp_rw [this, ← fintype.card_sigma, fintype.card_congr
            (self_equiv_sigma_orbits_quotient_stabilizer' α β hφ)],
end

/-- **Class formula**. This is a special case of
`mul_action.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = quotient.out'`. -/
@[to_additive "**Class formula**. This is a special case of
`add_action.self_equiv_sigma_orbits_quotient_stabilizer'` with `φ = quotient.out'`. "]
noncomputable def self_equiv_sigma_orbits_quotient_stabilizer :
  β ≃ Σ (ω : Ω), α ⧸ (stabilizer α ω.out') :=
self_equiv_sigma_orbits_quotient_stabilizer' α β quotient.out_eq'

/-- **Class formula** for a finite group acting on a finite type. -/
@[to_additive "**Class formula** for a finite group acting on a finite type."]
lemma card_eq_sum_card_group_div_card_stabilizer [fintype α] [fintype β] [fintype Ω]
  [Π (b : β), fintype $ stabilizer α b] :
  fintype.card β = ∑ (ω : Ω), fintype.card α / fintype.card (stabilizer α ω.out') :=
card_eq_sum_card_group_div_card_stabilizer' α β quotient.out_eq'

/-- **Burnside's lemma** : a (noncomputable) bijection between the disjoint union of all
`{x ∈ X | g • x = x}` for `g ∈ G` and the product `G × X/G`, where `G` is a group acting on `X` and
`X/G`denotes the quotient of `X` by the relation `orbit_rel G X`. -/
@[to_additive "**Burnside's lemma** : a (noncomputable) bijection between the disjoint union of all
`{x ∈ X | g • x = x}` for `g ∈ G` and the product `G × X/G`, where `G` is an additive group acting
on `X` and `X/G`denotes the quotient of `X` by the relation `orbit_rel G X`. "]
noncomputable def sigma_fixed_by_equiv_orbits_prod_group :
  (Σ (a : α), (fixed_by α β a)) ≃ Ω × α :=
calc  (Σ (a : α), fixed_by α β a)
    ≃ {ab : α × β // ab.1 • ab.2 = ab.2} :
        (equiv.subtype_prod_equiv_sigma_subtype _).symm
... ≃ {ba : β × α // ba.2 • ba.1 = ba.1} :
        (equiv.prod_comm α β).subtype_equiv (λ ab, iff.rfl)
... ≃ Σ (b : β), stabilizer α b :
        equiv.subtype_prod_equiv_sigma_subtype (λ (b : β) a, a ∈ stabilizer α b)
... ≃ Σ (ωb : (Σ (ω : Ω), orbit α ω.out')), stabilizer α (ωb.2 : β) :
        (self_equiv_sigma_orbits α β).sigma_congr_left'
... ≃ Σ (ω : Ω), (Σ (b : orbit α ω.out'), stabilizer α (b : β)) :
        equiv.sigma_assoc (λ (ω : Ω) (b : orbit α ω.out'), stabilizer α (b : β))
... ≃ Σ (ω : Ω), (Σ (b : orbit α ω.out'), stabilizer α ω.out') :
        equiv.sigma_congr_right (λ ω, equiv.sigma_congr_right $
          λ ⟨b, hb⟩, (stabilizer_equiv_stabilizer_of_orbit_rel hb).to_equiv)
... ≃ Σ (ω : Ω), orbit α ω.out' × stabilizer α ω.out' :
        equiv.sigma_congr_right (λ ω, equiv.sigma_equiv_prod _ _)
... ≃ Σ (ω : Ω), α :
        equiv.sigma_congr_right (λ ω, orbit_prod_stabilizer_equiv_group α ω.out')
... ≃ Ω × α :
        equiv.sigma_equiv_prod Ω α

/-- **Burnside's lemma** : given a finite group `G` acting on a set `X`, the average number of
elements fixed by each `g ∈ G` is the number of orbits. -/
@[to_additive "**Burnside's lemma** : given a finite additive group `G` acting on a set `X`,
the average number of elements fixed by each `g ∈ G` is the number of orbits. "]
lemma sum_card_fixed_by_eq_card_orbits_mul_card_group [fintype α] [Π a, fintype $ fixed_by α β a]
  [fintype Ω] :
  ∑ (a : α), fintype.card (fixed_by α β a) = fintype.card Ω * fintype.card α :=
by rw [← fintype.card_prod, ← fintype.card_sigma,
        fintype.card_congr (sigma_fixed_by_equiv_orbits_prod_group α β)]

@[to_additive] instance is_pretransitive_quotient (G) [group G] (H : subgroup G) :
  is_pretransitive G (G ⧸ H) :=
{ exists_smul_eq := begin
    rintros ⟨x⟩ ⟨y⟩,
    refine ⟨y * x⁻¹, quotient_group.eq.mpr _⟩,
    simp only [H.one_mem, mul_left_inv, inv_mul_cancel_right],
  end }

end mul_action

section
variables [monoid α] [add_monoid β] [distrib_mul_action α β]

lemma list.smul_sum {r : α} {l : list β} :
  r • l.sum = (l.map ((•) r)).sum :=
(distrib_mul_action.to_add_monoid_hom β r).map_list_sum l

/-- `smul` by a `k : M` over a ring is injective, if `k` is not a zero divisor.
The general theory of such `k` is elaborated by `is_smul_regular`.
The typeclass that restricts all terms of `M` to have this property is `no_zero_smul_divisors`. -/
lemma smul_cancel_of_non_zero_divisor {M R : Type*} [monoid M] [ring R] [distrib_mul_action M R]
  (k : M) (h : ∀ (x : R), k • x = 0 → x = 0) {a b : R} (h' : k • a = k • b) :
  a = b :=
begin
  rw ←sub_eq_zero,
  refine h _ _,
  rw [smul_sub, h', sub_self]
end

end

section
variables [monoid α] [monoid β] [mul_distrib_mul_action α β]

lemma list.smul_prod {r : α} {l : list β} :
  r • l.prod = (l.map ((•) r)).prod :=
(mul_distrib_mul_action.to_monoid_hom β r).map_list_prod l

end

section
variables [monoid α] [add_comm_monoid β] [distrib_mul_action α β]

lemma multiset.smul_sum {r : α} {s : multiset β} :
  r • s.sum = (s.map ((•) r)).sum :=
(distrib_mul_action.to_add_monoid_hom β r).map_multiset_sum s

lemma finset.smul_sum {r : α} {f : γ → β} {s : finset γ} :
  r • ∑ x in s, f x = ∑ x in s, r • f x :=
(distrib_mul_action.to_add_monoid_hom β r).map_sum f s

end

section
variables [monoid α] [comm_monoid β] [mul_distrib_mul_action α β]

lemma multiset.smul_prod {r : α} {s : multiset β} :
  r • s.prod = (s.map ((•) r)).prod :=
(mul_distrib_mul_action.to_monoid_hom β r).map_multiset_prod s

lemma finset.smul_prod {r : α} {f : γ → β} {s : finset γ} :
  r • ∏ x in s, f x = ∏ x in s, r • f x :=
(mul_distrib_mul_action.to_monoid_hom β r).map_prod f s

end

namespace subgroup

variables {G : Type*} [group G] (H : subgroup G)

lemma normal_core_eq_ker :
  H.normal_core = (mul_action.to_perm_hom G (G ⧸ H)).ker :=
begin
  refine le_antisymm (λ g hg, equiv.perm.ext (λ q, quotient_group.induction_on q
    (λ g', (mul_action.quotient.smul_mk H g g').trans (quotient_group.eq.mpr _))))
    (subgroup.normal_le_normal_core.mpr (λ g hg, _)),
  { rw [mul_inv_rev, ←inv_inv g', inv_inv],
    exact H.normal_core.inv_mem hg g'⁻¹ },
  { rw [←H.inv_mem_iff, ←mul_one g⁻¹, ←quotient_group.eq, ←mul_one g],
    exact (mul_action.quotient.smul_mk H g 1).symm.trans (equiv.perm.ext_iff.mp hg (1 : G)) },
end

noncomputable instance fintype_quotient_normal_core [fintype (G ⧸ H)] :
  fintype (G ⧸ H.normal_core) :=
begin
  rw H.normal_core_eq_ker,
  classical,
  exact fintype.of_equiv _ (quotient_group.quotient_ker_equiv_range _).symm.to_equiv,
end

end subgroup

author: jjaassoonn