[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a a₁ a₂ b b₁ b₂ c x : α
h : a ≤ b
⊢ [[a, b]] = Icc a b
[PROOFSTEP]
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a a₁ a₂ b b₁ b₂ c x : α
h : b ≤ a
⊢ [[a, b]] = Icc b a
[PROOFSTEP]
rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α
⊢ [[a, b]] = [[b, a]]
[PROOFSTEP]
simp_rw [uIcc, inf_comm, sup_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, a]] = {a}
[PROOFSTEP]
simp [uIcc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Lattice α
inst✝ : Lattice β
a✝ a₁ a₂ b✝ b₁ b₂ c x : α
a b : α × β
⊢ [[a, b]] = [[a.fst, b.fst]] ×ˢ [[a.snd, b.snd]]
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c
[PROOFSTEP]
simpa only [uIcc_comm a] using eq_of_mem_uIcc_of_mem_uIcc
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
rw [ext_iff] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => [[b, a]]) b ↔ x ∈ (fun b => [[b, a]]) c
⊢ b = c
[PROOFSTEP]
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DistribLattice α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective (uIcc a)
[PROOFSTEP]
simpa only [uIcc_comm] using uIcc_injective_right a
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, b]] = Icc a b ∪ Icc b a
[PROOFSTEP]
rw [Icc_union_Icc', max_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ [[a, b]] = Icc (min a b) (max a b)
[PROOFSTEP]
rfl
[GOAL]
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ≤ b
[PROOFSTEP]
rfl
[GOAL]
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ≤ a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
[PROOFSTEP]
simp [uIcc_eq_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
⊢ x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]
[PROOFSTEP]
simp only [mem_uIcc, mem_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
cases' le_total a c with h1 h1
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : a ≤ c
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
cases' le_total x b with h2 h2
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : c ≤ a
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
cases' le_total x b with h2 h2
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : a ≤ c
h2 : x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : a ≤ c
h2 : b ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : c ≤ a
h2 : x ≤ b
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x✝ x : α
h1 : c ≤ a
h2 : b ≤ x
⊢ a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
rintro (hf | hf) a b c
[GOAL]
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Monotone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
[GOAL]
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Antitone f
a b c : α
⊢ c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
[GOAL]
case mp.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Monotone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (min a b)) (f (max a b))
case mp.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x : α
hf : Antitone f
a b c : α
⊢ c ∈ Icc (min a b) (max a b) → f c ∈ Icc (f (max a b)) (f (min a b))
[PROOFSTEP]
exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
[PROOFSTEP]
contrapose!
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ¬Monotone f ∧ ¬Antitone f → ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
rw [not_monotone_not_antitone_iff_exists_le_le]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ (∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) →
    ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_lt <| max_lt hfab hfcb⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b c, c ∈ [[a, b]] ∧ ¬f c ∈ [[f a, f b]]
[PROOFSTEP]
exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_lt <| lt_min hfba hfbc⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ MonotoneOn f s ∨ AntitoneOn f s ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → ∀ (c : α), c ∈ s → c ∈ [[a, b]] → f c ∈ [[f a, f b]]
[PROOFSTEP]
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, monotone_or_antitone_iff_uIcc, mem_uIcc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h : a ≤ b
⊢ Ι a b = Ioc a b
[PROOFSTEP]
simp [uIoc, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h : b < a
⊢ Ι a b = Ioc b a
[PROOFSTEP]
simp [uIoc, le_of_lt h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ Ι a b = Ioc a b ∪ Ioc b a
[PROOFSTEP]
cases le_total a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h✝ : a ≤ b
⊢ Ι a b = Ioc a b ∪ Ioc b a
[PROOFSTEP]
simp [uIoc, *]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
h✝ : b ≤ a
⊢ Ι a b = Ioc a b ∪ Ioc b a
[PROOFSTEP]
simp [uIoc, *]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
[PROOFSTEP]
rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ¬a ∈ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
[PROOFSTEP]
simp only [uIoc_eq_union, mem_union, mem_Ioc, not_lt, ← not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ι a b ↔ b < a
[PROOFSTEP]
simp [mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ι a b ↔ a < b
[PROOFSTEP]
simp [mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
P : α → Prop
⊢ (∀ (x : α), x ∈ Ι a b → P x) ↔ (∀ (x : α), x ∈ Ioc a b → P x) ∧ ∀ (x : α), x ∈ Ioc b a → P x
[PROOFSTEP]
simp only [uIoc_eq_union, mem_union, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α
⊢ Ι a b = Ι b a
[PROOFSTEP]
simp only [uIoc, min_comm a b, max_comm a b]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b
[PROOFSTEP]
simp_rw [mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b
[PROOFSTEP]
rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩)
[GOAL]
case inl.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : b < a
right✝¹ : a ≤ c
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : a < b
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact le_trans ‹_› (le_of_lt ‹_›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
⊢ b ∈ Ι a c → c ∈ Ι a b → b = c
[PROOFSTEP]
simpa only [uIoc_comm a] using eq_of_mem_uIoc_of_mem_uIoc
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
⊢ ¬a ∈ Ι b c → ¬b ∈ Ι a c → a = b
[PROOFSTEP]
simp_rw [not_mem_uIoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
⊢ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a → b ≤ a ∧ b ≤ c ∨ c < b ∧ a < b → a = b
[PROOFSTEP]
rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩)
[GOAL]
case inl.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inr.intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a = b
[PROOFSTEP]
apply le_antisymm
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inl.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : a ≤ b
right✝¹ : a ≤ c
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
exact absurd hb (not_le_of_lt ‹c < b›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact absurd hb (not_le_of_lt ‹c < b›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ a ≤ b
[PROOFSTEP]
exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inl.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : b ≤ a
right✝ : b ≤ c
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ a ≤ b
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
first
| assumption
| exact le_of_lt ‹_›
| exact absurd hb (not_le_of_lt ‹c < b›)
| exact absurd ha (not_le_of_lt ‹c < a›)
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
assumption
[GOAL]
case inr.intro.inr.intro.a
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a a₁ a₂ b b₁ b₂ c x : α
ha : a ≤ c
hb : b ≤ c
left✝¹ : c < a
right✝¹ : b < a
left✝ : c < b
right✝ : a < b
⊢ b ≤ a
[PROOFSTEP]
exact le_of_lt ‹_›
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective fun b => Ι b a
[PROOFSTEP]
rintro b c h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : (fun b => Ι b a) b = (fun b => Ι b a) c
⊢ b = c
[PROOFSTEP]
rw [ext_iff] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
⊢ b = c
[PROOFSTEP]
obtain ha | ha := le_or_lt b a
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
⊢ b = c
[PROOFSTEP]
have hb := (h b).not
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : ¬b ∈ (fun b => Ι b a) b ↔ ¬b ∈ (fun b => Ι b a) c
⊢ b = c
[PROOFSTEP]
simp only [ha, left_mem_uIoc, not_lt, true_iff_iff, not_mem_uIoc, ← not_le, and_true_iff, not_true, false_and_iff,
  not_false_iff, true_iff_iff, or_false_iff] at hb
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ≤ c
⊢ b = c
[PROOFSTEP]
refine' hb.eq_of_not_lt fun hc => _
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : b ≤ a
hb : b ≤ c
hc : b < c
⊢ False
[PROOFSTEP]
simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b = c
[PROOFSTEP]
refine' eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha) ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le _)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b✝ b₁ b₂ c✝ x a b c : α
h : ∀ (x : α), x ∈ (fun b => Ι b a) b ↔ x ∈ (fun b => Ι b a) c
ha : a < b
⊢ b ≤ c
[PROOFSTEP]
simpa [ha, ha.not_le, mem_uIoc] using h b
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ a₁ a₂ b b₁ b₂ c x a : α
⊢ Injective (Ι a)
[PROOFSTEP]
simpa only [uIoc_comm] using uIoc_injective_right a


[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ↑f '' List.prod (a :: as) = List.prod (List.map (fun s => ↑f '' s) (a :: as))
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : F
⊢ ∀ (a : List (Set α)),
    ↑f '' Multiset.prod (Quotient.mk (List.isSetoid (Set α)) a) =
      Multiset.prod (Multiset.map (fun s => ↑f '' s) (Quotient.mk (List.isSetoid (Set α)) a))
[PROOFSTEP]
simpa only [Multiset.quot_mk_to_coe, Multiset.coe_prod, Multiset.coe_map] using image_list_prod f
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Finset ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i in t, f i ↔ ∃ g x, ∏ i in t, g i = a
[PROOFSTEP]
classical
induction' t using Finset.induction_on with i is hi ih generalizing a
· simp_rw [Finset.prod_empty, Set.mem_one]
  exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.not_mem_empty _ hi), h.symm⟩, fun ⟨_, _, hf⟩ ↦ hf.symm⟩
rw [Finset.prod_insert hi, Set.mem_mul]
simp_rw [Finset.prod_insert hi]
simp_rw [ih]
constructor
· rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
  refine ⟨Function.update g i x, ?_, ?_⟩
  · intro j hj
    obtain rfl | hj := Finset.mem_insert.mp hj
    · rwa [Function.update_same]
    · rw [update_noteq (ne_of_mem_of_not_mem hj hi)]
      exact hg hj
  · rw [Finset.prod_update_of_not_mem hi, Function.update_same]
· rintro ⟨g, hg, rfl⟩
  exact ⟨g i, is.prod g, hg (is.mem_insert_self _), ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Finset ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i in t, f i ↔ ∃ g x, ∏ i in t, g i = a
[PROOFSTEP]
induction' t using Finset.induction_on with i is hi ih generalizing a
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ a : α
⊢ a ∈ ∏ i in ∅, f i ↔ ∃ g x, ∏ i in ∅, g i = a
[PROOFSTEP]
simp_rw [Finset.prod_empty, Set.mem_one]
[GOAL]
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ a : α
⊢ a = 1 ↔ ∃ g h, 1 = a
[PROOFSTEP]
exact ⟨fun h ↦ ⟨fun _ ↦ a, fun hi ↦ False.elim (Finset.not_mem_empty _ hi), h.symm⟩, fun ⟨_, _, hf⟩ ↦ hf.symm⟩
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ a ∈ ∏ i in insert i is, f i ↔ ∃ g x, ∏ i in insert i is, g i = a
[PROOFSTEP]
rw [Finset.prod_insert hi, Set.mem_mul]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ y ∈ ∏ x in is, f x ∧ x * y = a) ↔ ∃ g x, ∏ i in insert i is, g i = a
[PROOFSTEP]
simp_rw [Finset.prod_insert hi]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ y ∈ ∏ x in is, f x ∧ x * y = a) ↔ ∃ g h, g i * ∏ i in is, g i = a
[PROOFSTEP]
simp_rw [ih]
[GOAL]
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = a) ↔ ∃ g h, g i * ∏ i in is, g i = a
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = a) → ∃ g h, g i * ∏ i in is, g i = a
[PROOFSTEP]
rintro ⟨x, y, hx, ⟨g, hg, rfl⟩, rfl⟩
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∃ g_1 h, g_1 i * ∏ i in is, g_1 i = x * ∏ i in is, g i
[PROOFSTEP]
refine ⟨Function.update g i x, ?_, ?_⟩
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ ∀ {i_1 : ι}, i_1 ∈ insert i is → update g i x i_1 ∈ f i_1
[PROOFSTEP]
intro j hj
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj : j ∈ insert i is
⊢ update g i x j ∈ f j
[PROOFSTEP]
obtain rfl | hj := Finset.mem_insert.mp hj
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1.inl
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
is : Finset ι
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hi : ¬j ∈ is
hx : x ∈ f j
hj : j ∈ insert j is
⊢ update g j x j ∈ f j
[PROOFSTEP]
rwa [Function.update_same]
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1.inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ update g i x j ∈ f j
[PROOFSTEP]
rw [update_noteq (ne_of_mem_of_not_mem hj hi)]
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_1.inr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
j : ι
hj✝ : j ∈ insert i is
hj : j ∈ is
⊢ g j ∈ f j
[PROOFSTEP]
exact hg hj
[GOAL]
case insert.mp.intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
x : α
hx : x ∈ f i
g : ι → α
hg : ∀ {i : ι}, i ∈ is → g i ∈ f i
⊢ update g i x i * ∏ i_1 in is, update g i x i_1 = x * ∏ i in is, g i
[PROOFSTEP]
rw [Finset.prod_update_of_not_mem hi, Function.update_same]
[GOAL]
case insert.mpr
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a✝ : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
a : α
⊢ (∃ g h, g i * ∏ i in is, g i = a) → ∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = a
[PROOFSTEP]
rintro ⟨g, hg, rfl⟩
[GOAL]
case insert.mpr.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
a : α
i : ι
is : Finset ι
hi : ¬i ∈ is
ih : ∀ (a : α), a ∈ ∏ i in is, f i ↔ ∃ g x, ∏ i in is, g i = a
g : ι → α
hg : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1
⊢ ∃ x y, x ∈ f i ∧ (∃ g x, ∏ i in is, g i = y) ∧ x * y = g i * ∏ i in is, g i
[PROOFSTEP]
exact ⟨g i, is.prod g, hg (is.mem_insert_self _), ⟨⟨g, fun hi ↦ hg (Finset.mem_insert_of_mem hi), rfl⟩, rfl⟩⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ a ∈ ∏ i : ι, f i ↔ ∃ g x, ∏ i : ι, g i = a
[PROOFSTEP]
rw [mem_finset_prod]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
f : ι → Set α
a : α
⊢ (∃ g x, ∏ i : ι, g i = a) ↔ ∃ g x, ∏ i : ι, g i = a
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg : ∀ (i : ι), i ∈ t → g i ∈ f i
⊢ List.prod (List.map g t) ∈ List.prod (List.map f t)
[PROOFSTEP]
induction' t with h tl ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg✝ : ∀ (i : ι), i ∈ t → g i ∈ f i
hg : ∀ (i : ι), i ∈ [] → g i ∈ f i
⊢ List.prod (List.map g []) ∈ List.prod (List.map f [])
[PROOFSTEP]
simp_rw [List.map_nil, List.prod_nil, Set.mem_one]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg✝ : ∀ (i : ι), i ∈ t → g i ∈ f i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → g i ∈ f i) → List.prod (List.map g tl) ∈ List.prod (List.map f tl)
hg : ∀ (i : ι), i ∈ h :: tl → g i ∈ f i
⊢ List.prod (List.map g (h :: tl)) ∈ List.prod (List.map f (h :: tl))
[PROOFSTEP]
simp_rw [List.map_cons, List.prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f : ι → Set α
g : ι → α
hg✝ : ∀ (i : ι), i ∈ t → g i ∈ f i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → g i ∈ f i) → List.prod (List.map g tl) ∈ List.prod (List.map f tl)
hg : ∀ (i : ι), i ∈ h :: tl → g i ∈ f i
⊢ g h * List.prod (List.map g tl) ∈ f h * List.prod (List.map f tl)
[PROOFSTEP]
exact mul_mem_mul (hg h <| List.mem_cons_self _ _) (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ t) ⊆ List.prod (List.map f₂ t)
[PROOFSTEP]
induction' t with h tl ih
[GOAL]
case nil
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf✝ : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
hf : ∀ (i : ι), i ∈ [] → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ []) ⊆ List.prod (List.map f₂ [])
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf✝ : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → f₁ i ⊆ f₂ i) → List.prod (List.map f₁ tl) ⊆ List.prod (List.map f₂ tl)
hf : ∀ (i : ι), i ∈ h :: tl → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ (h :: tl)) ⊆ List.prod (List.map f₂ (h :: tl))
[PROOFSTEP]
simp_rw [List.map_cons, List.prod_cons]
[GOAL]
case cons
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : List ι
f₁ f₂ : ι → Set α
hf✝ : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
h : ι
tl : List ι
ih : (∀ (i : ι), i ∈ tl → f₁ i ⊆ f₂ i) → List.prod (List.map f₁ tl) ⊆ List.prod (List.map f₂ tl)
hf : ∀ (i : ι), i ∈ h :: tl → f₁ i ⊆ f₂ i
⊢ f₁ h * List.prod (List.map f₁ tl) ⊆ f₂ h * List.prod (List.map f₂ tl)
[PROOFSTEP]
exact mul_subset_mul (hf h <| List.mem_cons_self _ _) (ih fun i hi ↦ hf i <| List.mem_cons_of_mem _ hi)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Multiset ι
f : ι → Set α
g : ι → α
hg : ∀ (i : ι), i ∈ t → g i ∈ f i
⊢ Multiset.prod (Multiset.map g t) ∈ Multiset.prod (Multiset.map f t)
[PROOFSTEP]
induction t using Quotient.inductionOn
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → g i ∈ f i
⊢ Multiset.prod (Multiset.map g (Quotient.mk (List.isSetoid ι) a✝)) ∈
    Multiset.prod (Multiset.map f (Quotient.mk (List.isSetoid ι) a✝))
[PROOFSTEP]
simp_rw [Multiset.quot_mk_to_coe, Multiset.coe_map, Multiset.coe_prod]
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → g i ∈ f i
⊢ List.prod (List.map g a✝) ∈ List.prod (List.map f a✝)
[PROOFSTEP]
exact list_prod_mem_list_prod _ _ _ hg
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
t : Multiset ι
f₁ f₂ : ι → Set α
hf : ∀ (i : ι), i ∈ t → f₁ i ⊆ f₂ i
⊢ Multiset.prod (Multiset.map f₁ t) ⊆ Multiset.prod (Multiset.map f₂ t)
[PROOFSTEP]
induction t using Quotient.inductionOn
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → f₁ i ⊆ f₂ i
⊢ Multiset.prod (Multiset.map f₁ (Quotient.mk (List.isSetoid ι) a✝)) ⊆
    Multiset.prod (Multiset.map f₂ (Quotient.mk (List.isSetoid ι) a✝))
[PROOFSTEP]
simp_rw [Multiset.quot_mk_to_coe, Multiset.coe_map, Multiset.coe_prod]
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ (i : ι), i ∈ Quotient.mk (List.isSetoid ι) a✝ → f₁ i ⊆ f₂ i
⊢ List.prod (List.map f₁ a✝) ⊆ List.prod (List.map f₂ a✝)
[PROOFSTEP]
exact list_prod_subset_list_prod _ _ _ hf
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
l : Finset ι
S : ι → Set α
⊢ (fun f => ∏ i in l, f i) '' pi (↑l) S = ∏ i in l, S i
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
l : Finset ι
S : ι → Set α
x✝ : α
⊢ x✝ ∈ (fun f => ∏ i in l, f i) '' pi (↑l) S ↔ x✝ ∈ ∏ i in l, S i
[PROOFSTEP]
simp_rw [mem_finset_prod, mem_image, mem_pi, exists_prop, Finset.mem_coe]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : MonoidHomClass F α β
inst✝ : Fintype ι
S : ι → Set α
⊢ (fun f => ∏ i : ι, f i) '' pi univ S = ∏ i : ι, S i
[PROOFSTEP]
simpa only [Finset.coe_univ] using image_finset_prod_pi Finset.univ S


[GOAL]
a : ℤ
n : ℕ
⊢ succ^[n + 1] a = a + ↑(n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', Int.ofNat_succ, ← add_assoc]
[GOAL]
a : ℤ
n : ℕ
⊢ (succ ∘ succ^[n]) a = a + ↑n + 1
[PROOFSTEP]
exact congr_arg _ (succ_iterate a n)
[GOAL]
a : ℤ
n : ℕ
⊢ pred^[n + 1] a = a - ↑(n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', Int.ofNat_succ, ← sub_sub]
[GOAL]
a : ℤ
n : ℕ
⊢ (pred ∘ pred^[n]) a = a - ↑n - 1
[PROOFSTEP]
exact congr_arg _ (pred_iterate a n)
[GOAL]
a b : ℤ
h : a ≤ b
⊢ Order.succ^[toNat (b - a)] a = b
[PROOFSTEP]
rw [succ_eq_succ, succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel']
[GOAL]
a b : ℤ
h : a ≤ b
⊢ Order.pred^[toNat (b - a)] b = a
[PROOFSTEP]
rw [pred_eq_pred, pred_iterate, toNat_sub_of_le h, sub_sub_cancel]
[GOAL]
z : ℤ
⊢ z - 1 ⋖ z
[PROOFSTEP]
rw [Int.covby_iff_succ_eq, sub_add_cancel]
[GOAL]
a b : ℕ
⊢ ↑a ⋖ ↑b ↔ a ⋖ b
[PROOFSTEP]
rw [Nat.covby_iff_succ_eq, Int.covby_iff_succ_eq]
[GOAL]
a b : ℕ
⊢ ↑a + 1 = ↑b ↔ a + 1 = b
[PROOFSTEP]
exact Int.coe_nat_inj'


[GOAL]
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]
[PROOFSTEP]
unfold ModEq Nat.ModEq
[GOAL]
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
[PROOFSTEP]
rw [← Int.ofNat_inj]
[GOAL]
m n✝ a✝ b✝ c d : ℤ
a b n : ℕ
⊢ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
[PROOFSTEP]
simp [coe_nat_mod]
[GOAL]
m n a b c d : ℤ
⊢ a ≡ 0 [ZMOD n] ↔ n ∣ a
[PROOFSTEP]
rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]
[GOAL]
m n a b c d : ℤ
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a
[PROOFSTEP]
rw [ModEq, eq_comm]
[GOAL]
m n a b c d : ℤ
⊢ b % n = a % n ↔ n ∣ b - a
[PROOFSTEP]
simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]
[GOAL]
m n✝ a✝ b✝ c d a b n : ℤ
⊢ a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t
[PROOFSTEP]
rw [modEq_iff_dvd]
[GOAL]
m n✝ a✝ b✝ c d a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t
[PROOFSTEP]
exact exists_congr fun t => sub_eq_iff_eq_add'
[GOAL]
m n a b c d : ℤ
⊢ -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]
[PROOFSTEP]
simp [-sub_neg_eq_add, neg_sub_neg, modEq_iff_dvd, dvd_sub_comm]
[GOAL]
m n a b c d : ℤ
⊢ a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]
[PROOFSTEP]
simp [modEq_iff_dvd]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
obtain hc | rfl | hc := lt_trichotomy c 0
[GOAL]
case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
[GOAL]
case inl
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : c < 0
⊢ -c * a ≡ -c * b [ZMOD -c * n]
[PROOFSTEP]
simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
[GOAL]
case inr.inl
m n a b d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 * a ≡ 0 * b [ZMOD 0 * n]
[PROOFSTEP]
simp
[GOAL]
case inr.inr
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
hc : 0 < c
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a * c ≡ b * c [ZMOD n * c]
[PROOFSTEP]
rw [mul_comm a, mul_comm b, mul_comm n]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ c * a ≡ c * b [ZMOD c * n]
[PROOFSTEP]
exact h.mul_left'
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ n ∣ b + d - (a + c)
[PROOFSTEP]
convert dvd_add h₁.dvd h₂.dvd using 1
[GOAL]
case h.e'_4
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ b + d - (a + c) = b - a + (d - c)
[PROOFSTEP]
ring
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ d - c = b + d - (a + c) - (b - a)
[PROOFSTEP]
ring
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ d - c
[PROOFSTEP]
rw [this]
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
this : d - c = b + d - (a + c) - (b - a)
⊢ n ∣ b + d - (a + c) - (b - a)
[PROOFSTEP]
exact dvd_sub h₂.dvd h₁.dvd
[GOAL]
m n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]
[PROOFSTEP]
rw [add_comm a, add_comm b] at h₂
[GOAL]
m n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : c + a ≡ d + b [ZMOD n]
⊢ a ≡ b [ZMOD n]
[PROOFSTEP]
exact h₁.add_left_cancel h₂
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a + -a ≡ b + -b [ZMOD n]
[PROOFSTEP]
simp_rw [← sub_eq_add_neg, sub_self]
[GOAL]
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ 0 ≡ 0 [ZMOD n]
[PROOFSTEP]
rfl
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a - c ≡ b - d [ZMOD n]
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg]
[GOAL]
m n a b c d : ℤ
h₁ : a ≡ b [ZMOD n]
h₂ : c ≡ d [ZMOD n]
⊢ a + -c ≡ b + -d [ZMOD n]
[PROOFSTEP]
exact h₁.add h₂.neg
[GOAL]
m✝ n a b c d : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]
[PROOFSTEP]
induction' m with d hd
[GOAL]
case zero
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]
[PROOFSTEP]
rfl
[GOAL]
case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ Nat.succ d ≡ b ^ Nat.succ d [ZMOD n]
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a * a ^ d ≡ b * b ^ d [ZMOD n]
[PROOFSTEP]
exact h.mul hd
[GOAL]
m✝ n a b c d m : ℤ
h : a ≡ b [ZMOD m * n]
⊢ a ≡ b [ZMOD n]
[PROOFSTEP]
rw [modEq_iff_dvd] at *
[GOAL]
m✝ n a b c d m : ℤ
h : m * n ∣ b - a
⊢ n ∣ b - a
[PROOFSTEP]
exact (dvd_mul_left n m).trans h
[GOAL]
m n a b c d : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
letI d := gcd m c
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
have hmd := gcd_dvd_left m c
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
have hcd := gcd_dvd_right m c
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
[PROOFSTEP]
rw [modEq_iff_dvd] at h ⊢
  -- porting note: removed `show` due to leanprover-community/mathlib4#3305
[GOAL]
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑(gcd m c) ∣ b - a
[PROOFSTEP]
refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
[GOAL]
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ c / ↑d * (b - a)
[PROOFSTEP]
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
[GOAL]
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(gcd m c)
[PROOFSTEP]
exact Int.ediv_dvd_ediv hmd h
[GOAL]
case refine_2
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ gcd (m / ↑(gcd m c)) (c / ↑d) = 1
[PROOFSTEP]
rw [gcd_div hmd hcd, natAbs_ofNat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
[GOAL]
m n a b c d : ℤ
hm : 0 < m
h : c * a ≡ c * b [ZMOD m]
⊢ a * c ≡ b * c [ZMOD m]
[PROOFSTEP]
simpa [mul_comm] using h
[GOAL]
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [ZMOD m]
[PROOFSTEP]
convert h.mul_left'
[GOAL]
case h.e'_1
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = ?m.21777 * (m / c)
[PROOFSTEP]
rwa [Int.mul_ediv_cancel']
[GOAL]
case h.e'_2
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = c * (a / c)
[PROOFSTEP]
rwa [Int.mul_ediv_cancel']
[GOAL]
case h.e'_3
m n a b c d : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = c * (b / c)
[PROOFSTEP]
rwa [Int.mul_ediv_cancel']
[GOAL]
m n a b c d : ℤ
⊢ a ≡ b [ZMOD 0] ↔ a = b
[PROOFSTEP]
rw [ModEq, emod_zero, emod_zero]
[GOAL]
m n a b c d : ℤ
⊢ n ∣ n + a - a
[PROOFSTEP]
simp
[GOAL]
m n a b c d : ℤ
⊢ n ∣ a + n - a
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n]
⊢ a ≡ b [ZMOD m * n]
[PROOFSTEP]
rw [modEq_iff_dvd, modEq_iff_dvd] at h
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ a ≡ b [ZMOD m * n]
[PROOFSTEP]
rw [modEq_iff_dvd, ← natAbs_dvd, ← dvd_natAbs, coe_nat_dvd, natAbs_mul]
[GOAL]
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ natAbs m * natAbs n ∣ natAbs (b - a)
[PROOFSTEP]
refine' hmn.mul_dvd_of_dvd_of_dvd _ _
[GOAL]
case refine'_1
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ natAbs m ∣ natAbs (b - a)
[PROOFSTEP]
rw [← coe_nat_dvd, natAbs_dvd, dvd_natAbs]
[GOAL]
case refine'_2
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ natAbs n ∣ natAbs (b - a)
[PROOFSTEP]
rw [← coe_nat_dvd, natAbs_dvd, dvd_natAbs]
[GOAL]
case refine'_1
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ m ∣ b - a
[PROOFSTEP]
tauto
[GOAL]
case refine'_2
m✝ n✝ a✝ b✝ c d a b m n : ℤ
hmn : Nat.coprime (natAbs m) (natAbs n)
h : m ∣ b - a ∧ n ∣ b - a
⊢ n ∣ b - a
[PROOFSTEP]
tauto
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
⊢ ↑a * Nat.gcdA a b ≡ ↑(Nat.gcd a b) [ZMOD ↑b]
[PROOFSTEP]
rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
⊢ ↑a * Nat.gcdA a b + 0 ≡ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b [ZMOD ↑b]
[PROOFSTEP]
exact (dvd_mul_right _ _).zero_modEq_int.add_left _
[GOAL]
m n✝ a✝ b✝ c✝ d a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ b + 0 ≡ b [ZMOD n]
[PROOFSTEP]
rw [add_zero]
[GOAL]
m n✝ a✝ b✝ c✝ d a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ a - n * c ≡ b [ZMOD n]
[PROOFSTEP]
convert Int.modEq_add_fac (-c) ha using 1
[GOAL]
case h.e'_2
m n✝ a✝ b✝ c✝ d a b n c : ℤ
ha : a ≡ b [ZMOD n]
⊢ a - n * c = a + n * -c
[PROOFSTEP]
ring
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
hab : Nat.coprime a b
hgcd : Nat.gcd a b = 1
⊢ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b ≡ 1 [ZMOD ↑b]
[PROOFSTEP]
rw [← Nat.gcd_eq_gcd_ab, hgcd]
[GOAL]
m n a✝ b✝ c d : ℤ
a b : ℕ
hab : Nat.coprime a b
hgcd : Nat.gcd a b = 1
⊢ ↑1 ≡ 1 [ZMOD ↑b]
[PROOFSTEP]
rfl
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
⊢ a % b < b
[PROOFSTEP]
have : a % b < |b| := emod_lt _ (ne_of_gt hb)
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
this : a % b < |b|
⊢ a % b < b
[PROOFSTEP]
rwa [abs_of_pos hb] at this
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
⊢ a % b ≡ a [ZMOD b]
[PROOFSTEP]
simp [ModEq]
[GOAL]
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑(natAbs z) < b ∧ ↑(natAbs z) ≡ a [ZMOD b]
[PROOFSTEP]
constructor
[GOAL]
case left
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑(natAbs z) < b
[PROOFSTEP]
rw [ofNat_natAbs_eq_of_nonneg z hz1]
[GOAL]
case right
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑(natAbs z) ≡ a [ZMOD b]
[PROOFSTEP]
rw [ofNat_natAbs_eq_of_nonneg z hz1]
[GOAL]
case left
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z < b
[PROOFSTEP]
assumption
[GOAL]
case right
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z ≡ a [ZMOD b]
[PROOFSTEP]
assumption


[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
[PROOFSTEP]
let ⟨b, Hb⟩ := Hbdd
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
[PROOFSTEP]
let ⟨lb, H⟩ := leastOfBdd b Hb Hinh
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → b ≤ z
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
⊢ ∃ lb, P lb ∧ ∀ (z : ℤ), P z → lb ≤ z
[PROOFSTEP]
exact ⟨lb, H⟩
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
⊢ ↑(leastOfBdd b Hb Hinh) = ↑(leastOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases leastOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
[GOAL]
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → n ≤ z) } = ↑(leastOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases leastOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
[GOAL]
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → n ≤ z
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → n' ≤ z
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → n ≤ z) } =
    ↑{ val := n', property := (_ : P n' ∧ ∀ (z : ℤ), P z → n' ≤ z) }
[PROOFSTEP]
exact le_antisymm (h2n _ hn') (h2n' _ hn)
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P (- -elt)
[PROOFSTEP]
rw [neg_neg]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
elt : ℤ
Helt : P elt
⊢ P elt
[PROOFSTEP]
exact Helt
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
Hinh' : ∃ z, P (-z)
lb : ℤ
Plb : P (-lb)
al : ∀ (z : ℤ), P (-z) → lb ≤ z
z : ℤ
h : P z
⊢ P (- -z)
[PROOFSTEP]
rwa [neg_neg]
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
[PROOFSTEP]
let ⟨b, Hb⟩ := Hbdd
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
[PROOFSTEP]
let ⟨lb, H⟩ := greatestOfBdd b Hb Hinh
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
Hbdd : ∃ b, ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
lb : ℤ
H : P lb ∧ ∀ (z : ℤ), P z → z ≤ lb
⊢ ∃ ub, P ub ∧ ∀ (z : ℤ), P z → z ≤ ub
[PROOFSTEP]
exact ⟨lb, H⟩
[GOAL]
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
⊢ ↑(greatestOfBdd b Hb Hinh) = ↑(greatestOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases greatestOfBdd b Hb Hinh with ⟨n, hn, h2n⟩
[GOAL]
case mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → z ≤ n) } = ↑(greatestOfBdd b' Hb' Hinh)
[PROOFSTEP]
rcases greatestOfBdd b' Hb' Hinh with ⟨n', hn', h2n'⟩
[GOAL]
case mk.intro.mk.intro
P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
n : ℤ
hn : P n
h2n : ∀ (z : ℤ), P z → z ≤ n
n' : ℤ
hn' : P n'
h2n' : ∀ (z : ℤ), P z → z ≤ n'
⊢ ↑{ val := n, property := (_ : P n ∧ ∀ (z : ℤ), P z → z ≤ n) } =
    ↑{ val := n', property := (_ : P n' ∧ ∀ (z : ℤ), P z → z ≤ n') }
[PROOFSTEP]
exact le_antisymm (h2n' _ hn) (h2n _ hn')


[GOAL]
a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d
[PROOFSTEP]
cases' hbc with k hk
[GOAL]
case intro
a b c d : ℤ
hb : b ≠ 0
h : b * a = c * d
k : ℤ
hk : c = b * k
⊢ a = c / b * d
[PROOFSTEP]
subst hk
[GOAL]
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d
[PROOFSTEP]
rw [Int.mul_ediv_cancel_left _ hb]
[GOAL]
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
[PROOFSTEP]
rw [mul_assoc] at h
[GOAL]
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * (k * d)
⊢ a = k * d
[PROOFSTEP]
apply mul_left_cancel₀ hb h
[GOAL]
a b : ℤ
w : a ∣ b
h : natAbs b < natAbs a
⊢ b = 0
[PROOFSTEP]
rw [← natAbs_dvd, ← dvd_natAbs, coe_nat_dvd] at w
[GOAL]
a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ b = 0
[PROOFSTEP]
rw [← natAbs_eq_zero]
[GOAL]
a b : ℤ
w : natAbs a ∣ natAbs b
h : natAbs b < natAbs a
⊢ natAbs b = 0
[PROOFSTEP]
exact eq_zero_of_dvd_of_lt w h
[GOAL]
m n : ℕ
h : Nat.succ n ≤ m
⊢ ofNat m + -[n+1] = ofNat (m - Nat.succ n)
[PROOFSTEP]
rw [negSucc_eq, ofNat_eq_cast, ofNat_eq_cast, ← Nat.cast_one, ← Nat.cast_add, ← sub_eq_add_neg, ← Nat.cast_sub h]


[GOAL]
n : ℤ
⊢ sqrt (n * n) = ↑(natAbs n)
[PROOFSTEP]
rw [sqrt, ← natAbs_mul_self, toNat_coe_nat, Nat.sqrt_eq]
[GOAL]
x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [← hn, sqrt_eq, ← Int.ofNat_mul, natAbs_mul_self]


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
⊢ DecidablePred fun x => x ∈ s ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
⊢ DecidablePred fun x => x ∈ s ^ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, mem_one]
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
⊢ DecidablePred fun x => x = 1
[PROOFSTEP]
infer_instance
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : DecidablePred fun x => x ∈ s ^ n
⊢ DecidablePred fun x => x ∈ s ^ Nat.succ n
[PROOFSTEP]
letI := ih
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : DecidablePred fun x => x ∈ s ^ n
this : DecidablePred fun x => x ∈ s ^ n := ih
⊢ DecidablePred fun x => x ∈ s ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x => x ∈ s
n : ℕ
ih : DecidablePred fun x => x ∈ s ^ n
this : DecidablePred fun x => x ∈ s ^ n := ih
⊢ DecidablePred fun x => x ∈ s * s ^ n
[PROOFSTEP]
infer_instance
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
have hG : 0 < Fintype.card G := Fintype.card_pos_iff.mpr ⟨1⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
by_cases hS : S = ∅
[GOAL]
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : S = ∅
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
refine' fun k hk ↦ Fintype.card_congr _
[GOAL]
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : S = ∅
k : ℕ
hk : Fintype.card G ≤ k
⊢ ↑(S ^ k) ≃ ↑(S ^ Fintype.card G)
[PROOFSTEP]
rw [hS, empty_pow (ne_of_gt (lt_of_lt_of_le hG hk)), empty_pow (ne_of_gt hG)]
[GOAL]
case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 hS
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
have key :
  ∀ (a) (s t : Set G) [Fintype s] [Fintype t], (∀ b : G, b ∈ s → a * b ∈ t) → Fintype.card s ≤ Fintype.card t :=
  by
  refine' fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨a * b, h b hb⟩) _
  rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
  exact Subtype.ext (mul_left_cancel (Subtype.ext_iff.mp hbc))
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
⊢ ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
[PROOFSTEP]
refine' fun a s t _ _ h ↦ Fintype.card_le_of_injective (fun ⟨b, hb⟩ ↦ ⟨a * b, h b hb⟩) _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a✝ : G
ha : a✝ ∈ S
a : G
s t : Set G
x✝¹ : Fintype ↑s
x✝ : Fintype ↑t
h : ∀ (b : G), b ∈ s → a * b ∈ t
⊢ Function.Injective fun x =>
    match x with
    | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) }
[PROOFSTEP]
rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a✝ : G
ha : a✝ ∈ S
a : G
s t : Set G
x✝¹ : Fintype ↑s
x✝ : Fintype ↑t
h : ∀ (b : G), b ∈ s → a * b ∈ t
b : G
hb : b ∈ s
c : G
hc : c ∈ s
hbc :
  (fun x =>
        match x with
        | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
      { val := b, property := hb } =
    (fun x =>
        match x with
        | { val := b, property := hb } => { val := a * b, property := (_ : a * b ∈ t) })
      { val := c, property := hc }
⊢ { val := b, property := hb } = { val := c, property := hc }
[PROOFSTEP]
exact Subtype.ext (mul_left_cancel (Subtype.ext_iff.mp hbc))
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
have mono : Monotone (fun n ↦ Fintype.card (↥(S ^ n)) : ℕ → ℕ) :=
  monotone_nat_of_le_succ fun n ↦ key a _ _ fun b hb ↦ Set.mul_mem_mul ha hb
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)
[PROOFSTEP]
refine'
  card_pow_eq_card_pow_card_univ_aux mono (fun n ↦ set_fintype_card_le_univ (S ^ n)) fun n h ↦
    le_antisymm (mono (n + 1).le_succ) (key a⁻¹ (S ^ (n + 2)) (S ^ (n + 1)) _)
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ ∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)
[PROOFSTEP]
replace h₂ : { a } * S ^ n = S ^ (n + 1)
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ {a} * S ^ n = S ^ (n + 1)
[PROOFSTEP]
have : Fintype (Set.singleton a * S ^ n) := by
  classical!
  apply fintypeMul
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ Fintype ↑(Set.singleton a * S ^ n)
[PROOFSTEP]
classical!
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
em✝ : (a : Prop) → Decidable a
⊢ Fintype ↑(Set.singleton a * S ^ n)
[PROOFSTEP]
apply fintypeMul
[GOAL]
case h₂
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(Set.singleton a * S ^ n)
⊢ {a} * S ^ n = S ^ (n + 1)
[PROOFSTEP]
refine' Set.eq_of_subset_of_card_le _ (le_trans (ge_of_eq h) _)
[GOAL]
case h₂.refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(Set.singleton a * S ^ n)
⊢ {a} * S ^ n ⊆ S ^ (n + 1)
[PROOFSTEP]
exact mul_subset_mul (Set.singleton_subset_iff.mpr ha) Set.Subset.rfl
[GOAL]
case h₂.refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
this : Fintype ↑(Set.singleton a * S ^ n)
⊢ Fintype.card ↑(S ^ n) ≤ Fintype.card ↑({a} * S ^ n)
[PROOFSTEP]
convert key a (S ^ n) ({ a } * S ^ n) fun b hb ↦ Set.mul_mem_mul (Set.mem_singleton a) hb
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : {a} * S ^ n = S ^ (n + 1)
⊢ ∀ (b : G), b ∈ S ^ (n + 2) → a⁻¹ * b ∈ S ^ (n + 1)
[PROOFSTEP]
rw [pow_succ', ← h₂, mul_assoc, ← pow_succ', h₂]
[GOAL]
case neg.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : {a} * S ^ n = S ^ (n + 1)
⊢ ∀ (b : G), b ∈ {a} * S ^ (n + 1) → a⁻¹ * b ∈ S ^ (n + 1)
[PROOFSTEP]
rintro _ ⟨b, c, hb, hc, rfl⟩
[GOAL]
case neg.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x => x ∈ S ^ k
hG : 0 < Fintype.card G
hS : ¬S = ∅
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ (b : G), b ∈ s → a * b ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n => Fintype.card ↑(S ^ n)
n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : {a} * S ^ n = S ^ (n + 1)
b c : G
hb : b ∈ {a}
hc : c ∈ S ^ (n + 1)
⊢ a⁻¹ * (fun x x_1 => x * x_1) b c ∈ S ^ (n + 1)
[PROOFSTEP]
rwa [Set.mem_singleton_iff.mp hb, inv_mul_cancel_left]


[GOAL]
a b : ℤ
⊢ natAbs a = natAbs b ↔ Associated a b
[PROOFSTEP]
refine' Int.natAbs_eq_natAbs_iff.trans _
[GOAL]
a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b
[PROOFSTEP]
constructor
[GOAL]
case mp
a b : ℤ
⊢ a = b ∨ a = -b → Associated a b
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case mp.inl
a : ℤ
⊢ Associated a a
[PROOFSTEP]
rfl
[GOAL]
case mp.inr
b : ℤ
⊢ Associated (-b) b
[PROOFSTEP]
exact ⟨-1, by simp⟩
[GOAL]
b : ℤ
⊢ -b * ↑(-1) = b
[PROOFSTEP]
simp
[GOAL]
case mpr
a b : ℤ
⊢ Associated a b → a = b ∨ a = -b
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case mpr.intro
a : ℤ
u : ℤˣ
⊢ a = a * ↑u ∨ a = -(a * ↑u)
[PROOFSTEP]
obtain rfl | rfl := Int.units_eq_one_or u
[GOAL]
case mpr.intro.inl
a : ℤ
⊢ a = a * ↑1 ∨ a = -(a * ↑1)
[PROOFSTEP]
exact Or.inl (by simp)
[GOAL]
a : ℤ
⊢ a = a * ↑1
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.inr
a : ℤ
⊢ a = a * ↑(-1) ∨ a = -(a * ↑(-1))
[PROOFSTEP]
exact Or.inr (by simp)
[GOAL]
a : ℤ
⊢ a = -(a * ↑(-1))
[PROOFSTEP]
simp