internlm/Lean-Github huggingface dataset:
Theorem: MulAction.orbit.isPretransitive_iff
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ orbit G a = ⊤ ↔ IsPretransitive G X
Tactic:
rw [IsPretransitive.mk_base_iff a]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ orbit G a = ⊤ ↔ ∀ (x : X), ∃ g, g • a = x
Theorem: MulAction.orbit.isPretransitive_iff
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ orbit G a = ⊤ ↔ ∀ (x : X), ∃ g, g • a = x
Tactic:
rw [Set.ext_iff]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∀ (x : X), ∃ g, g • a = x
Theorem: MulAction.orbit.isPretransitive_iff
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ (∀ (x : X), x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∀ (x : X), ∃ g, g • a = x
Tactic:
apply forall_congr'
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (a_1 : X), (a_1 ∈ orbit G a ↔ a_1 ∈ ⊤) ↔ ∃ g, g • a = a_1
Theorem: MulAction.orbit.isPretransitive_iff
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a : X
⊢ ∀ (a_1 : X), (a_1 ∈ orbit G a ↔ a_1 ∈ ⊤) ↔ ∃ g, g • a = a_1
Tactic:
intro x
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ (x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∃ g, g • a = x
Theorem: MulAction.orbit.isPretransitive_iff
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ (x ∈ orbit G a ↔ x ∈ ⊤) ↔ ∃ g, g • a = x
Tactic:
simp_rw [Set.top_eq_univ, Set.mem_univ, iff_true_iff]
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ x ∈ orbit G a ↔ ∃ g, g • a = x
Theorem: MulAction.orbit.isPretransitive_iff
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
a x : X
⊢ x ∈ orbit G a ↔ ∃ g, g • a = x
Tactic:
rw [mem_orbit_iff]
Proof state after:
no goals
Theorem: three_cycle_is_commutator
Proof state before:
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ commutatorSet ↥(alternatingGroup α)
Tactic:
apply mem_commutatorSet_of_isConj_sq
Proof state after:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsConj g (g ^ 2)
Theorem: three_cycle_is_commutator
Proof state before:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsConj g (g ^ 2)
Tactic:
apply alternatingGroup.isThreeCycle_isConj h5 hg
Proof state after:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsThreeCycle ↑(g ^ 2)
Theorem: three_cycle_is_commutator
Proof state before:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsThreeCycle ↑(g ^ 2)
Tactic:
exact hg.isThreeCycle_sq
Proof state after:
no goals
Theorem: three_cycle_is_commutator'
Proof state before:
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg : IsThreeCycle g
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
rw [← Subgroup.coe_mk (alternatingGroup α) g (Equiv.Perm.IsThreeCycle.sign hg)] at hg
Proof state after:
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Theorem: three_cycle_is_commutator'
Proof state before:
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
obtain ⟨p, q, h⟩ := three_cycle_is_commutator h5 hg
Proof state after:
case intro.intro
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Theorem: three_cycle_is_commutator'
Proof state before:
case intro.intro
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ p q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
use p
Proof state after:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Theorem: three_cycle_is_commutator'
Proof state before:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ ∃ q, g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
use q
Proof state after:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Theorem: three_cycle_is_commutator'
Proof state before:
case h
β : Type ?u.1022
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : Perm α
hg✝ : IsThreeCycle g
hg : IsThreeCycle ↑{ val := g, property := ⋯ }
p q : ↥(alternatingGroup α)
h : ⁅p, q⁆ = { val := g, property := ⋯ }
⊢ g = ↑p * ↑q * ↑p⁻¹ * ↑q⁻¹
Tactic:
simp only [← Subgroup.coe_mul, ← Subgroup.coe_inv, ← commutatorElement_def, h, coe_mk]
Proof state after:
no goals
Theorem: three_cycle_mem_commutator
Proof state before:
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ _root_.commutator ↥(alternatingGroup α)
Tactic:
rw [commutator_eq_closure]
Proof state after:
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ closure (commutatorSet ↥(alternatingGroup α))
Theorem: three_cycle_mem_commutator
Proof state before:
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ closure (commutatorSet ↥(alternatingGroup α))
Tactic:
apply Subgroup.subset_closure
Proof state after:
case a
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ commutatorSet ↥(alternatingGroup α)
Theorem: three_cycle_mem_commutator
Proof state before:
case a
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ commutatorSet ↥(alternatingGroup α)
Tactic:
exact three_cycle_is_commutator h5 hg
Proof state after:
no goals
Theorem: alternatingGroup_is_perfect
Proof state before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ _root_.commutator ↥(alternatingGroup α) = ⊤
Tactic:
suffices closure {b : alternatingGroup α | (b : Perm α).IsThreeCycle} = ⊤ by
  rw [eq_top_iff, ← this, Subgroup.closure_le]
  intro b hb
  exact three_cycle_mem_commutator h5 hb
Proof state after:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ closure {b | IsThreeCycle ↑b} = ⊤
Theorem: alternatingGroup_is_perfect
Proof state before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ closure {b | IsThreeCycle ↑b} = ⊤
Tactic:
apply Subgroup.closure_closure_coe_preimage
Proof state after:
no goals
Theorem: alternatingGroup_is_perfect
Proof state before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
⊢ _root_.commutator ↥(alternatingGroup α) = ⊤
Tactic:
rw [eq_top_iff, ← this, Subgroup.closure_le]
Proof state after:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
⊢ {b | IsThreeCycle ↑b} ⊆ ↑(_root_.commutator ↥(alternatingGroup α))
Theorem: alternatingGroup_is_perfect
Proof state before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
⊢ {b | IsThreeCycle ↑b} ⊆ ↑(_root_.commutator ↥(alternatingGroup α))
Tactic:
intro b hb
Proof state after:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
b : ↥(alternatingGroup α)
hb : b ∈ {b | IsThreeCycle ↑b}
⊢ b ∈ ↑(_root_.commutator ↥(alternatingGroup α))
Theorem: alternatingGroup_is_perfect
Proof state before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
b : ↥(alternatingGroup α)
hb : b ∈ {b | IsThreeCycle ↑b}
⊢ b ∈ ↑(_root_.commutator ↥(alternatingGroup α))
Tactic:
exact three_cycle_mem_commutator h5 hb
Proof state after:
no goals
Theorem: alternatingGroup_is_perfect'
Proof state before:
β : Type ?u.7470
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α
Tactic:
rw [← Subgroup.commutator_eq', alternatingGroup_is_perfect h5, Subgroup.map_top_eq_range,
  Subgroup.subtype_range]
Proof state after:
no goals
Theorem: alternatingGroup.commutator_group_le
Proof state before:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ _root_.commutator (Perm α) ≤ alternatingGroup α
Tactic:
rw [commutator_eq_closure, Subgroup.closure_le]
Proof state after:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ commutatorSet (Perm α) ⊆ ↑(alternatingGroup α)
Theorem: alternatingGroup.commutator_group_le
Proof state before:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ commutatorSet (Perm α) ⊆ ↑(alternatingGroup α)
Tactic:
intro x
Proof state after:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : Perm α
⊢ x ∈ commutatorSet (Perm α) → x ∈ ↑(alternatingGroup α)
Theorem: alternatingGroup.commutator_group_le
Proof state before:
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : Perm α
⊢ x ∈ commutatorSet (Perm α) → x ∈ ↑(alternatingGroup α)
Tactic:
rintro ⟨p, q, rfl⟩
Proof state after:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ ⁅p, q⁆ ∈ ↑(alternatingGroup α)
Theorem: alternatingGroup.commutator_group_le
Proof state before:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ ⁅p, q⁆ ∈ ↑(alternatingGroup α)
Tactic:
simp only [SetLike.mem_coe, mem_alternatingGroup, map_commutatorElement,
  commutatorElement_eq_one_iff_commute]
Proof state after:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ Commute (sign p) (sign q)
Theorem: alternatingGroup.commutator_group_le
Proof state before:
case intro.intro
β : Type ?u.8051
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p q : Perm α
⊢ Commute (sign p) (sign q)
Tactic:
apply Commute.all
Proof state after:
no goals
Theorem: alternatingGroup.commutator_group_eq
Proof state before:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ _root_.commutator (Perm α) = alternatingGroup α
Tactic:
apply le_antisymm alternatingGroup.commutator_group_le
Proof state after:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ alternatingGroup α ≤ _root_.commutator (Perm α)
Theorem: alternatingGroup.commutator_group_eq
Proof state before:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ alternatingGroup α ≤ _root_.commutator (Perm α)
Tactic:
rw [← alternatingGroup_is_perfect' h5]
Proof state after:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)
Theorem: alternatingGroup.commutator_group_eq
Proof state before:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)
Tactic:
exact commutator_mono le_top le_top
Proof state after:
no goals
Theorem: exercise2_1
Proof state before:
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) → (∃ x, p x) ∨ ∃ x, q x

case mpr
α : Type u_1
p q : α → Prop
⊢ ((∃ x, p x) ∨ ∃ x, q x) → ∃ x, p x ∨ q x
Theorem: exercise2_1
Proof state before:
case mp
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) → (∃ x, p x) ∨ ∃ x, q x
Tactic:
rintro ⟨x, hpx|hqx⟩
Proof state after:
case mp.intro.inl
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ (∃ x, p x) ∨ ∃ x, q x

case mp.intro.inr
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ (∃ x, p x) ∨ ∃ x, q x
Theorem: exercise2_1
Proof state before:
case mp.intro.inl
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ (∃ x, p x) ∨ ∃ x, q x
Tactic:
left
Proof state after:
case mp.intro.inl.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x
Theorem: exercise2_1
Proof state before:
case mp.intro.inl.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x
Tactic:
use x
Proof state after:
no goals
Theorem: exercise2_1
Proof state before:
case mp.intro.inr
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ (∃ x, p x) ∨ ∃ x, q x
Tactic:
right
Proof state after:
case mp.intro.inr.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, q x
Theorem: exercise2_1
Proof state before:
case mp.intro.inr.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, q x
Tactic:
use x
Proof state after:
no goals
Theorem: exercise2_1
Proof state before:
case mpr
α : Type u_1
p q : α → Prop
⊢ ((∃ x, p x) ∨ ∃ x, q x) → ∃ x, p x ∨ q x
Tactic:
rintro (⟨x, hpx⟩|⟨x, hqx⟩)
Proof state after:
case mpr.inl.intro
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x ∨ q x

case mpr.inr.intro
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, p x ∨ q x
Theorem: exercise2_1
Proof state before:
case mpr.inl.intro
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x ∨ q x
Tactic:
use x
Proof state after:
case h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x ∨ q x
Theorem: exercise2_1
Proof state before:
case h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x ∨ q x
Tactic:
left
Proof state after:
case h.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x
Theorem: exercise2_1
Proof state before:
case h.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x
Tactic:
assumption
Proof state after:
no goals
Theorem: exercise2_1
Proof state before:
case mpr.inr.intro
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, p x ∨ q x
Tactic:
use x
Proof state after:
case h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ p x ∨ q x
Theorem: exercise2_1
Proof state before:
case h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ p x ∨ q x
Tactic:
right
Proof state after:
case h.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ q x
Theorem: exercise2_1
Proof state before:
case h.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ q x
Tactic:
assumption
Proof state after:
no goals
Theorem: exercise2_2
Proof state before:
f g : ℝ → ℝ
x : ℝ
h : SurjectiveFunction (g ∘ f)
⊢ SurjectiveFunction g
Tactic:
intro y
Proof state after:
f g : ℝ → ℝ
x : ℝ
h : SurjectiveFunction (g ∘ f)
y : ℝ
⊢ ∃ x, g x = y
Theorem: exercise2_2
Proof state before:
f g : ℝ → ℝ
x : ℝ
h : SurjectiveFunction (g ∘ f)
y : ℝ
⊢ ∃ x, g x = y
Tactic:
obtain ⟨x, hx⟩ := h y
Proof state after:
case intro
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ ∃ x, g x = y
Theorem: exercise2_2
Proof state before:
case intro
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ ∃ x, g x = y
Tactic:
use f x
Proof state after:
case h
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ g (f x) = y
Theorem: exercise2_2
Proof state before:
case h
f g : ℝ → ℝ
x✝ : ℝ
h : SurjectiveFunction (g ∘ f)
y x : ℝ
hx : (g ∘ f) x = y
⊢ g (f x) = y
Tactic:
exact hx
Proof state after:
no goals
Theorem: exercise2_3
Proof state before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction (g ∘ f) ↔ SurjectiveFunction g
Tactic:
constructor
Proof state after:
case mp
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction (g ∘ f) → SurjectiveFunction g

case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction g → SurjectiveFunction (g ∘ f)
Theorem: exercise2_3
Proof state before:
case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction g → SurjectiveFunction (g ∘ f)
Tactic:
intro hg z
Proof state after:
case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z : ℝ
⊢ ∃ x, (g ∘ f) x = z
Theorem: exercise2_3
Proof state before:
case mpr
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z : ℝ
⊢ ∃ x, (g ∘ f) x = z
Tactic:
obtain ⟨y, hy⟩ := hg z
Proof state after:
case mpr.intro
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z
Theorem: exercise2_3
Proof state before:
case mpr.intro
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
⊢ ∃ x, (g ∘ f) x = z
Tactic:
obtain ⟨x, hx⟩ := hf y
Proof state after:
case mpr.intro.intro
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ ∃ x, (g ∘ f) x = z
Theorem: exercise2_3
Proof state before:
case mpr.intro.intro
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ ∃ x, (g ∘ f) x = z
Tactic:
use x
Proof state after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ (g ∘ f) x = z
Theorem: exercise2_3
Proof state before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ (g ∘ f) x = z
Tactic:
rw [← hy, ← hx]
Proof state after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ (g ∘ f) x = g (f x)
Theorem: exercise2_3
Proof state before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
hg : SurjectiveFunction g
z y : ℝ
hy : g y = z
x : ℝ
hx : f x = y
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
Proof state after:
no goals
Theorem: exercise2_3
Proof state before:
case mp
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction (g ∘ f) → SurjectiveFunction g
Tactic:
exact exercise2_2
Proof state after:
no goals
Theorem: exercise2_4
Proof state before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
⊢ SurjectiveFunction fun x => 2 * f (3 * (x + 4)) + 1
Tactic:
intro y
Proof state after:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
y : ℝ
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y
Theorem: exercise2_4
Proof state before:
f g : ℝ → ℝ
x : ℝ
hf : SurjectiveFunction f
y : ℝ
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y
Tactic:
obtain ⟨x, hx⟩ := hf ((y - 1) / 2)
Proof state after:
case intro
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y
Theorem: exercise2_4
Proof state before:
case intro
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ ∃ x, (fun x => 2 * f (3 * (x + 4)) + 1) x = y
Tactic:
use x / 3 - 4
Proof state after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ (fun x => 2 * f (3 * (x + 4)) + 1) (x / 3 - 4) = y
Theorem: exercise2_4
Proof state before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ (fun x => 2 * f (3 * (x + 4)) + 1) (x / 3 - 4) = y
Tactic:
ring
Proof state after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + f x * 2 = y
Theorem: exercise2_4
Proof state before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + f x * 2 = y
Tactic:
rw [hx]
Proof state after:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + (y - 1) / 2 * 2 = y
Theorem: exercise2_4
Proof state before:
case h
f g : ℝ → ℝ
x✝ : ℝ
hf : SurjectiveFunction f
y x : ℝ
hx : f x = (y - 1) / 2
⊢ 1 + (y - 1) / 2 * 2 = y
Tactic:
ring
Proof state after:
no goals
Theorem: exercise2_5
Proof state before:
s t : ℕ → ℕ
k : ℕ
⊢ EventuallyGrowsFaster (fun n => n * s n) s
Tactic:
intro k
Proof state after:
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * s n ≤ (fun n => n * s n) n
Theorem: exercise2_5
Proof state before:
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * s n ≤ (fun n => n * s n) n
Tactic:
use k
Proof state after:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * s n ≤ (fun n => n * s n) n
Theorem: exercise2_5
Proof state before:
case h
s t : ℕ → ℕ
k✝ k : ℕ
⊢ ∀ n ≥ k, k * s n ≤ (fun n => n * s n) n
Tactic:
intro n hnk
Proof state after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ (fun n => n * s n) n
Theorem: exercise2_5
Proof state before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ (fun n => n * s n) n
Tactic:
simp
Proof state after:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ n * s n
Theorem: exercise2_5
Proof state before:
case h
s t : ℕ → ℕ
k✝ k n : ℕ
hnk : n ≥ k
⊢ k * s n ≤ n * s n
Tactic:
gcongr
Proof state after:
no goals
Theorem: useful_fact
Proof state before:
s t : ℕ → ℕ
k a b c : ℕ
⊢ c ≥ max a b ↔ c ≥ a ∧ c ≥ b
Tactic:
simp
Proof state after:
no goals
Theorem: exercise2_6
Proof state before:
s t : ℕ → ℕ
k : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
⊢ EventuallyGrowsFaster (s₁ + s₂) (t₁ + t₂)
Tactic:
intro k
Proof state after:
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Theorem: exercise2_6
Proof state before:
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k : ℕ
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
obtain ⟨N₁, hN₁⟩ := h₁ k
Proof state after:
case intro
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Theorem: exercise2_6
Proof state before:
case intro
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
obtain ⟨N₂, hN₂⟩ := h₂ k
Proof state after:
case intro.intro
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Theorem: exercise2_6
Proof state before:
case intro.intro
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
⊢ ∃ N, ∀ n ≥ N, k * (t₁ + t₂) n ≤ (s₁ + s₂) n
Tactic:
use max N₁ N₂
Proof state after:
case h
s t : ℕ → ℕ
k✝ : ℕ
s₁ s₂ t₁ t₂ : ℕ → ℕ
h₁ : EventuallyGrowsFaster s₁ t₁
h₂ : EventuallyGrowsFaster s₂ t₂
k N₁ : ℕ
hN₁ : ∀ n ≥ N₁, k * t₁ n ≤ s₁ n
N₂ : ℕ
hN₂ : ∀ n ≥ N₂, k * t₂ n ≤ s₂ n
⊢ ∀ n ≥ max N₁ N₂, k * (t₁ + t₂) n ≤ (s₁ + s₂) n