internlm/Lean-Github huggingface dataset:
Theorem: conjugate_top
Proof state before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ x⁻¹ * a * x ∈ ⊤ ∧ a = x * (x⁻¹ * a * x) * x⁻¹
Tactic:
constructor
Proof state after:
case h.left
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ x⁻¹ * a * x ∈ ⊤

case h.right
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ a = x * (x⁻¹ * a * x) * x⁻¹
Theorem: conjugate_top
Proof state before:
case h.left
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ x⁻¹ * a * x ∈ ⊤
Tactic:
apply Subgroup.mem_top
Proof state after:
no goals
Theorem: conjugate_top
Proof state before:
case h.right
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ a = x * (x⁻¹ * a * x) * x⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: conjugate_eq_of_abelian
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
⊢ conjugate H x = H
Tactic:
ext a
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ a ∈ conjugate H x ↔ a ∈ H
Theorem: conjugate_eq_of_abelian
Proof state before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ a ∈ conjugate H x ↔ a ∈ H
Tactic:
rw [mem_conjugate_iff]
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ (∃ h ∈ H, a = x * h * x⁻¹) ↔ a ∈ H
Theorem: conjugate_eq_of_abelian
Proof state before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ (∃ h ∈ H, a = x * h * x⁻¹) ↔ a ∈ H
Tactic:
constructor
Proof state after:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ (∃ h ∈ H, a = x * h * x⁻¹) → a ∈ H

case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ a ∈ H → ∃ h ∈ H, a = x * h * x⁻¹
Theorem: conjugate_eq_of_abelian
Proof state before:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ (∃ h ∈ H, a = x * h * x⁻¹) → a ∈ H
Tactic:
rintro ⟨b, hb, rfl⟩
Proof state after:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x * b * x⁻¹ ∈ H
Theorem: conjugate_eq_of_abelian
Proof state before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x * b * x⁻¹ ∈ H
Tactic:
rw [habelian]
Proof state after:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x⁻¹ * (x * b) ∈ H
Theorem: conjugate_eq_of_abelian
Proof state before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x⁻¹ * (x * b) ∈ H
Tactic:
rwa [show x⁻¹ * (x * b) = b by group]
Proof state after:
no goals
Theorem: conjugate_eq_of_abelian
Proof state before:
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
b : G
hb : b ∈ H
⊢ x⁻¹ * (x * b) = b
Tactic:
group
Proof state after:
no goals
Theorem: conjugate_eq_of_abelian
Proof state before:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
⊢ a ∈ H → ∃ h ∈ H, a = x * h * x⁻¹
Tactic:
intro ha
Proof state after:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ ∃ h ∈ H, a = x * h * x⁻¹
Theorem: conjugate_eq_of_abelian
Proof state before:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ ∃ h ∈ H, a = x * h * x⁻¹
Tactic:
use x⁻¹ * a * x
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x⁻¹ * a * x ∈ H ∧ a = x * (x⁻¹ * a * x) * x⁻¹
Theorem: conjugate_eq_of_abelian
Proof state before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x⁻¹ * a * x ∈ H ∧ a = x * (x⁻¹ * a * x) * x⁻¹
Tactic:
refine' ⟨_, by group⟩
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x⁻¹ * a * x ∈ H
Theorem: conjugate_eq_of_abelian
Proof state before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x⁻¹ * a * x ∈ H
Tactic:
rw [habelian]
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x * (x⁻¹ * a) ∈ H
Theorem: conjugate_eq_of_abelian
Proof state before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x * (x⁻¹ * a) ∈ H
Tactic:
rwa [show x * (x⁻¹ * a) = a by group]
Proof state after:
no goals
Theorem: conjugate_eq_of_abelian
Proof state before:
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ a = x * (x⁻¹ * a * x) * x⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: conjugate_eq_of_abelian
Proof state before:
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
a : G
ha : a ∈ H
⊢ x * (x⁻¹ * a) = a
Tactic:
group
Proof state after:
no goals
Theorem: Section3sheet1.injective_def
Proof state before:
X Y Z : Type
f : X → Y
⊢ Injective f ↔ ∀ (a b : X), f a = f b → a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1.surjective_def
Proof state before:
X Y Z : Type
f : X → Y
⊢ Surjective f ↔ ∀ (b : Y), ∃ a, f a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1.id_eval
Proof state before:
X Y Z : Type
x : X
⊢ id x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1.comp_eval
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
x : X
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ b = 1 * b
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ 1 * b = a⁻¹ * a * b
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * a * b = a⁻¹ * (a * b)
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * (a * b) = a⁻¹ * (a * c)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * (a * c) = a⁻¹ * a * c
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ a⁻¹ * a * c = 1 * c
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_left_cancel
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : a * b = a * c
⊢ 1 * c = c
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_eq_of_eq_inv_mul
Proof state before:
G : Type
inst✝ : WeakGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a * b = c
Tactic:
apply mul_left_cancel a⁻¹
Proof state after:
case h
G : Type
inst✝ : WeakGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a⁻¹ * (a * b) = a⁻¹ * c
Theorem: Section5sheet2Solutions.WeakGroup.mul_eq_of_eq_inv_mul
Proof state before:
case h
G : Type
inst✝ : WeakGroup G
a b c : G
h : b = a⁻¹ * c
⊢ a⁻¹ * (a * b) = a⁻¹ * c
Tactic:
rwa [← mul_assoc, inv_mul_self, one_mul]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_one
Proof state before:
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ a * 1 = a
Tactic:
apply mul_eq_of_eq_inv_mul
Proof state after:
case h
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ 1 = a⁻¹ * a
Theorem: Section5sheet2Solutions.WeakGroup.mul_one
Proof state before:
case h
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ 1 = a⁻¹ * a
Tactic:
rw [inv_mul_self]
Proof state after:
no goals
Theorem: Section5sheet2Solutions.WeakGroup.mul_inv_self
Proof state before:
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ a * a⁻¹ = 1
Tactic:
apply mul_eq_of_eq_inv_mul
Proof state after:
case h
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ a⁻¹ = a⁻¹ * 1
Theorem: Section5sheet2Solutions.WeakGroup.mul_inv_self
Proof state before:
case h
G : Type
inst✝ : WeakGroup G
a✝ b c a : G
⊢ a⁻¹ = a⁻¹ * 1
Tactic:
rw [mul_one]
Proof state after:
no goals
Theorem: Section7sheet1.conjugate.one_mem
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
sorry
Proof state after:
no goals
Theorem: Section7sheet1.conjugate.inv_mem
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
hy : y ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
⊢ y⁻¹ ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
sorry
Proof state after:
no goals
Theorem: Section7sheet1.conjugate.mul_mem
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
hy : y ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
hz : z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
⊢ y * z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
sorry
Proof state after:
no goals
Theorem: Section7sheet1.mem_conjugate_iff
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ a ∈ conjugate H x ↔ ∃ h ∈ H, a = x * h * x⁻¹
Tactic:
rfl
Proof state after:
no goals
Theorem: Section7sheet1.conjugate_mono
Proof state before:
G : Type
inst✝ : Group G
a b : G
H✝ K✝ : Subgroup G
x y z : G
H K : Subgroup G
h : H ≤ K
⊢ conjugate H x ≤ conjugate K x
Tactic:
sorry
Proof state after:
no goals
Theorem: Section7sheet1.conjugate_bot
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ conjugate ⊥ x = ⊥
Tactic:
sorry
Proof state after:
no goals
Theorem: Section7sheet1.conjugate_top
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ conjugate ⊤ x = ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: Section7sheet1.conjugate_eq_of_abelian
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
habelian : ∀ (a b : G), a * b = b * a
⊢ conjugate H x = H
Tactic:
sorry
Proof state after:
no goals
Theorem: lemma1
Proof state before:
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a ↔ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
Tactic:
constructor
Proof state after:
case mp
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a → Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))

case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a})) → IsIntegral R a
Theorem: lemma1
Proof state before:
case mp
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a → Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
Tactic:
exact IsIntegral.fg_adjoin_singleton
Proof state after:
no goals
Theorem: lemma1
Proof state before:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a})) → IsIntegral R a
Tactic:
intro h
Proof state after:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
h : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
⊢ IsIntegral R a
Theorem: lemma1
Proof state before:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
h : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
⊢ IsIntegral R a
Tactic:
exact IsIntegral.of_mem_of_fg _ h _ (Algebra.self_mem_adjoin_singleton R a)
Proof state after:
no goals
Theorem: comp_id
Proof state before:
G H : Type
inst✝² : Group G
inst✝¹ : Group H
φ : G →* H
a : G
K : Type
inst✝ : Group K
ψ : H →* K
⊢ MonoidHom.comp φ (MonoidHom.id G) = φ
Tactic:
ext x
Proof state after:
case h
G H : Type
inst✝² : Group G
inst✝¹ : Group H
φ : G →* H
a : G
K : Type
inst✝ : Group K
ψ : H →* K
x : G
⊢ (MonoidHom.comp φ (MonoidHom.id G)) x = φ x
Theorem: comp_id
Proof state before:
case h
G H : Type
inst✝² : Group G
inst✝¹ : Group H
φ : G →* H
a : G
K : Type
inst✝ : Group K
ψ : H →* K
x : G
⊢ (MonoidHom.comp φ (MonoidHom.id G)) x = φ x
Tactic:
rfl
Proof state after:
no goals
Theorem: id_comp
Proof state before:
G H : Type
inst✝² : Group G
inst✝¹ : Group H
φ : G →* H
a : G
K : Type
inst✝ : Group K
ψ : H →* K
⊢ MonoidHom.comp (MonoidHom.id H) φ = φ
Tactic:
ext x
Proof state after:
case h
G H : Type
inst✝² : Group G
inst✝¹ : Group H
φ : G →* H
a : G
K : Type
inst✝ : Group K
ψ : H →* K
x : G
⊢ (MonoidHom.comp (MonoidHom.id H) φ) x = φ x
Theorem: id_comp
Proof state before:
case h
G H : Type
inst✝² : Group G
inst✝¹ : Group H
φ : G →* H
a : G
K : Type
inst✝ : Group K
ψ : H →* K
x : G
⊢ (MonoidHom.comp (MonoidHom.id H) φ) x = φ x
Tactic:
rfl
Proof state after:
no goals
Theorem: comp_assoc
Proof state before:
G H : Type
inst✝³ : Group G
inst✝² : Group H
φ : G →* H
a : G
K : Type
inst✝¹ : Group K
ψ : H →* K
L : Type
inst✝ : Group L
ρ : K →* L
⊢ MonoidHom.comp (MonoidHom.comp ρ ψ) φ = MonoidHom.comp ρ (MonoidHom.comp ψ φ)
Tactic:
rfl
Proof state after:
no goals
Theorem: Section10sheet1.Real.isOpen_univ
Proof state before:
X : Type
⊢ IsOpen Set.univ
Tactic:
sorry
Proof state after:
no goals
Theorem: Section10sheet1.Real.isOpen_inter
Proof state before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
⊢ IsOpen (s ∩ t)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section10sheet1.Real.isOpen_sUnion
Proof state before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
⊢ IsOpen (⋃₀ F)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
x : ℤ
⊢ x - 3 ∣ x ^ 3 - 3 ↔ x - 3 ∣ 24
Tactic:
have h : x - 3 ∣ x ^ 3 - 27
Proof state after:
case h
x : ℤ
⊢ x - 3 ∣ x ^ 3 - 27

x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 ↔ x - 3 ∣ 24
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 ↔ x - 3 ∣ 24
Tactic:
constructor
Proof state after:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 → x - 3 ∣ 24

case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ 24 → x - 3 ∣ x ^ 3 - 3
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case h
x : ℤ
⊢ x - 3 ∣ x ^ 3 - 27
Tactic:
use x ^ 2 + 3 * x + 9
Proof state after:
case h
x : ℤ
⊢ x ^ 3 - 27 = (x - 3) * (x ^ 2 + 3 * x + 9)
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case h
x : ℤ
⊢ x ^ 3 - 27 = (x - 3) * (x ^ 2 + 3 * x + 9)
Tactic:
ring
Proof state after:
no goals
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ x ^ 3 - 3 → x - 3 ∣ 24
Tactic:
intro h1
Proof state after:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
⊢ x - 3 ∣ 24
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
⊢ x - 3 ∣ 24
Tactic:
have h2 := dvd_sub h1 h
Proof state after:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ x - 3 ∣ 24
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case mp
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ x - 3 ∣ 24
Tactic:
convert h2
Proof state after:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ 24 = x ^ 3 - 3 - (x ^ 3 - 27)
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ x ^ 3 - 3
h2 : x - 3 ∣ x ^ 3 - 3 - (x ^ 3 - 27)
⊢ 24 = x ^ 3 - 3 - (x ^ 3 - 27)
Tactic:
ring
Proof state after:
no goals
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
⊢ x - 3 ∣ 24 → x - 3 ∣ x ^ 3 - 3
Tactic:
intro h1
Proof state after:
case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x - 3 ∣ x ^ 3 - 3
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case mpr
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x - 3 ∣ x ^ 3 - 3
Tactic:
convert dvd_add h h1 using 1
Proof state after:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x ^ 3 - 3 = x ^ 3 - 27 + 24
Theorem: Section15sheet2Solutions.lemma1
Proof state before:
case h.e'_4
x : ℤ
h : x - 3 ∣ x ^ 3 - 27
h1 : x - 3 ∣ 24
⊢ x ^ 3 - 3 = x ^ 3 - 27 + 24
Tactic:
ring
Proof state after:
no goals
Theorem: Section15sheet2Solutions.int_dvd_iff
Proof state before:
x n : ℤ
hn : n ≠ 0
⊢ x ∣ n ↔ Int.natAbs x ∈ Nat.divisors (Int.natAbs n)
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: Section15sheet2Solutions.lemma2
Proof state before:
x : ℤ
⊢ x ∣ 24 ↔ x ∈ {-24, -12, -8, -6, -4, -3, -2, -1, 1, 2, 3, 4, 6, 8, 12, 24}
Tactic:
suffices : x ∣ 24 ↔ x.natAbs ∈ ({1, 2, 3, 4, 6, 8, 12, 24} : Finset ℕ)
Proof state after:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔ x ∈ {-24, -12, -8, -6, -4, -3, -2, -1, 1, 2, 3, 4, 6, 8, 12, 24}

case this
x : ℤ
⊢ x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
Theorem: Section15sheet2Solutions.lemma2
Proof state before:
case this
x : ℤ
⊢ x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
Tactic:
exact int_dvd_iff _ 24 (by norm_num)
Proof state after:
no goals
Theorem: Section15sheet2Solutions.lemma2
Proof state before:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔ x ∈ {-24, -12, -8, -6, -4, -3, -2, -1, 1, 2, 3, 4, 6, 8, 12, 24}
Tactic:
simp only [Set.mem_insert_iff, Set.mem_singleton_iff]
Proof state after:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24
Theorem: Section15sheet2Solutions.lemma2
Proof state before:
x : ℤ
this : x ∣ 24 ↔ Int.natAbs x ∈ {1, 2, 3, 4, 6, 8, 12, 24}
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24
Tactic:
simp only [Finset.mem_insert, Int.natAbs_eq_iff, Nat.cast_one,
  Nat.cast_ofNat, Finset.mem_singleton] at this
Proof state after:
x : ℤ
this :
  x ∣ 24 ↔
    (x = 1 ∨ x = -1) ∨
      (x = 2 ∨ x = -2) ∨
        (x = 3 ∨ x = -3) ∨
          (x = 4 ∨ x = -4) ∨ (x = 6 ∨ x = -6) ∨ (x = 8 ∨ x = -8) ∨ (x = 12 ∨ x = -12) ∨ x = 24 ∨ x = -24
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24
Theorem: Section15sheet2Solutions.lemma2
Proof state before:
x : ℤ
this :
  x ∣ 24 ↔
    (x = 1 ∨ x = -1) ∨
      (x = 2 ∨ x = -2) ∨
        (x = 3 ∨ x = -3) ∨
          (x = 4 ∨ x = -4) ∨ (x = 6 ∨ x = -6) ∨ (x = 8 ∨ x = -8) ∨ (x = 12 ∨ x = -12) ∨ x = 24 ∨ x = -24
⊢ x ∣ 24 ↔
    x = -24 ∨
      x = -12 ∨
        x = -8 ∨
          x = -6 ∨ x = -4 ∨ x = -3 ∨ x = -2 ∨ x = -1 ∨ x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 6 ∨ x = 8 ∨ x = 12 ∨ x = 24
Tactic:
tauto
Proof state after:
no goals
Theorem: Section15sheet2Solutions.lemma2
Proof state before:
x : ℤ
⊢ 24 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Section4sheet4Solutions.mem_def
Proof state before:
X : Type
P : X → Prop
a : X
⊢ a ∈ {x | P x} ↔ P a
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1solutions.injective_def
Proof state before:
X Y Z : Type
f : X → Y
⊢ Injective f ↔ ∀ (a b : X), f a = f b → a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1solutions.surjective_def
Proof state before:
X Y Z : Type
f : X → Y
⊢ Surjective f ↔ ∀ (b : Y), ∃ a, f a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1solutions.id_eval
Proof state before:
X Y Z : Type
x : X
⊢ id x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1solutions.comp_eval
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
x : X
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Section17sheet2solutions.Complex.differentiableAt_coe
Proof state before:
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (fun y => ↑(f y)) x
Tactic:
apply Complex.ofRealClm.differentiableAt.comp _ hf
Proof state after:
no goals
Theorem: e10
Proof state before:
V : Type
G : SimpleGraph V
v w x : V
a : Walk G v w
⊢ Adj g5 1 0
Tactic:
decide
Proof state after:
no goals
Theorem: e21
Proof state before:
V : Type
G : SimpleGraph V
v w x : V
a : Walk G v w
⊢ Adj g5 2 1
Tactic:
decide
Proof state after:
no goals
Theorem: e02
Proof state before:
V : Type
G : SimpleGraph V
v w x : V
a : Walk G v w
⊢ Adj g5 0 2
Tactic:
decide
Proof state after:
no goals
Theorem: e30
Proof state before:
V : Type
G : SimpleGraph V
v w x : V
a : Walk G v w
⊢ Adj g5 3 0
Tactic:
decide
Proof state after:
no goals
Theorem: e43
Proof state before:
V : Type
G : SimpleGraph V
v w x : V
a : Walk G v w
⊢ Adj g5 4 3
Tactic:
decide
Proof state after:
no goals
Theorem: e04
Proof state before:
V : Type
G : SimpleGraph V
v w x : V
a : Walk G v w
⊢ Adj g5 0 4
Tactic:
decide
Proof state after:
no goals
Theorem: Section17sheet2.Complex.differentiableAt_coe
Proof state before:
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (fun y => ↑(f y)) x
Tactic:
apply Complex.ofRealClm.differentiableAt.comp _ hf
Proof state after:
no goals
Theorem: Section4sheet1Solutions.subset_def
Proof state before:
X : Type
A B C D : Set X
x : X
⊢ A ⊆ B ↔ ∀ x ∈ A, x ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: Section4sheet1Solutions.mem_union_iff
Proof state before:
X : Type
A B C D : Set X
x : X
⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
Tactic:
rfl
Proof state after:
no goals
Theorem: Section3sheet1.Yb_ne_Yc
Proof state before:
⊢ Y.b ≠ Y.c
Tactic:
intro h
Proof state after:
h : Y.b = Y.c
⊢ False
Theorem: Section3sheet1.Yb_ne_Yc
Proof state before:
h : Y.b = Y.c
⊢ False
Tactic:
cases h
Proof state after:
no goals
Theorem: Section3sheet1.gYb_eq_gYc
Proof state before:
⊢ g Y.b = g Y.c
Tactic:
sorry
Proof state after:
no goals
Theorem: Section3sheet1.gf_injective
Proof state before:
⊢ Injective (g ∘ f)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section3sheet1.gf_surjective
Proof state before:
⊢ Surjective (g ∘ f)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section19sheet2.lemma1
Proof state before:
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a ↔ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
Tactic:
constructor
Proof state after:
case mp
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a → Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))

case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a})) → IsIntegral R a
Theorem: Section19sheet2.lemma1
Proof state before:
case mp
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a → Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
Tactic:
exact IsIntegral.fg_adjoin_singleton
Proof state after:
no goals