internlm/Lean-Github huggingface dataset:
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ ∀ ε > 0, |t - s| < ε
Tactic:
intro ε hε
Proof state after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
⊢ |t - s| < ε
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
⊢ |t - s| < ε
Tactic:
obtain ⟨X, hX⟩ := h ε hε
Proof state after:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |(fun n => a n - a n) n - (s - t)| < ε
⊢ |t - s| < ε
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |(fun n => a n - a n) n - (s - t)| < ε
⊢ |t - s| < ε
Tactic:
specialize hX X (by rfl)
Proof state after:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : |(fun n => a n - a n) X - (s - t)| < ε
⊢ |t - s| < ε
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : |(fun n => a n - a n) X - (s - t)| < ε
⊢ |t - s| < ε
Tactic:
simpa using hX
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
this : ∀ ε > 0, |t - s| < ε
⊢ s = t
Tactic:
linarith [eq_zero_of_abs_lt_eps this]
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |(fun n => a n - a n) n - (s - t)| < ε
⊢ X ≤ X
Tactic:
rfl
Proof state after:
no goals
Theorem: Secion7Sheet2.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:
sorry
Proof state after:
no goals
Theorem: Secion7Sheet2.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:
sorry
Proof state after:
no goals
Theorem: Secion7Sheet2.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:
sorry
Proof state after:
no goals
Theorem: Section4sheet4.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: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
⊢ Set.Nonempty (↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)))
Tactic:
rw [Set.nonempty_iff_ne_empty]
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
⊢ ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) ≠ ∅
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
⊢ ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) ≠ ∅
Tactic:
intro h
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) = ∅
⊢ False
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)) = ∅
⊢ False
Tactic:
rw [Set.diff_eq_empty] at h
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ False
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ False
Tactic:
apply hInonfg
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.FG I
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.FG I
Tactic:
refine' ⟨Finset.image (fun m : Fin n => (g m.1 m.2).1) Finset.univ, _⟩
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) = I
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) = I
Tactic:
refine' le_antisymm _ h
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ≤ I
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ≤ I
Tactic:
rw [Ideal.span_le]
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ⊆ ↑I
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
⊢ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ) ⊆ ↑I
Tactic:
intro a ha
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : a ∈ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)
⊢ a ∈ ↑I
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : a ∈ ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)
⊢ a ∈ ↑I
Tactic:
simp only [Finset.coe_image, Finset.coe_univ, Set.image_univ,
  Set.mem_range] at ha
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : ∃ y, ↑(g ↑y (_ : ↑y < n)) = a
⊢ a ∈ ↑I
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
a : A
ha : ∃ y, ↑(g ↑y (_ : ↑y < n)) = a
⊢ a ∈ ↑I
Tactic:
rcases ha with ⟨y, rfl⟩
Proof state after:
case intro
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
y : Fin n
⊢ ↑(g ↑y (_ : ↑y < n)) ∈ ↑I
Theorem: Section16Sheet2solutions.lemma1
Proof state before:
case intro
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
h : ↑I ⊆ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
y : Fin n
⊢ ↑(g ↑y (_ : ↑y < n)) ∈ ↑I
Tactic:
exact (g y.1 y.2).2
Proof state after:
no goals
Theorem: Section16Sheet2solutions.lemma1'
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
set S : Set A := _
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ?m.3713
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Theorem: Section16Sheet2solutions.lemma1'
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ?m.3713
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
have ne1 : Set.Nonempty S := lemma1 hInonfg n g
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
ne1 : Set.Nonempty S
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Theorem: Section16Sheet2solutions.lemma1'
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
ne1 : Set.Nonempty S
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
choose x hx using ne1
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Theorem: Section16Sheet2solutions.lemma1'
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ Set.Nonempty {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
refine ⟨⟨x, hx.1⟩, ?_⟩
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ { val := x, property := (_ : x ∈ ↑I) } ∈
    {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Theorem: Section16Sheet2solutions.lemma1'
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ S
⊢ { val := x, property := (_ : x ∈ ↑I) } ∈
    {x | ↑x ∉ Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ)}
Tactic:
simp only [Finset.coe_image, Finset.coe_univ, Set.image_univ, Set.mem_diff,
  SetLike.mem_coe, Set.mem_setOf_eq] at hx ⊢
Proof state after:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ I ∧ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))
⊢ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))
Theorem: Section16Sheet2solutions.lemma1'
Proof state before:
A : Type
inst✝¹ : CommRing A
inst✝ : DecidableEq A
I : Ideal A
hInonfg : ¬Ideal.FG I
n : ℕ
g : (m : ℕ) → m < n → ↥I
S : Set A := ↑I \ ↑(Ideal.span ↑(Finset.image (fun m => ↑(g ↑m (_ : ↑m < n))) Finset.univ))
x : A
hx : x ∈ I ∧ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))
⊢ x ∉ Ideal.span (Set.range fun m => ↑(g ↑m (_ : ↑m < n)))
Tactic:
exact hx.2
Proof state after:
no goals
Theorem: 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:
use 1
Proof state after:
case h
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H ∧ 1 = x * 1 * x⁻¹
Theorem: conjugate.one_mem
Proof state before:
case h
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H ∧ 1 = x * 1 * x⁻¹
Tactic:
constructor
Proof state after:
case h.left
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H

case h.right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 = x * 1 * x⁻¹
Theorem: conjugate.one_mem
Proof state before:
case h.left
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ H
Tactic:
exact H.one_mem
Proof state after:
no goals
Theorem: conjugate.one_mem
Proof state before:
case h.right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 = x * 1 * x⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: 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:
rcases hy with ⟨g, hg, rfl⟩
Proof state after:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Theorem: conjugate.inv_mem
Proof state before:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
use g⁻¹, inv_mem hg
Proof state after:
case right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ = x * g⁻¹ * x⁻¹
Theorem: conjugate.inv_mem
Proof state before:
case right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z g : G
hg : g ∈ H
⊢ (x * g * x⁻¹)⁻¹ = x * g⁻¹ * x⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: 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:
rcases hy with ⟨g, hg, rfl⟩
Proof state after:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z : G
hz : z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
g : G
hg : g ∈ H
⊢ x * g * x⁻¹ * z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Theorem: conjugate.mul_mem
Proof state before:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x z : G
hz : z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
g : G
hg : g ∈ H
⊢ x * g * x⁻¹ * z ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
rcases hz with ⟨k, hk, rfl⟩
Proof state after:
case intro.intro.intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x g : G
hg : g ∈ H
k : G
hk : k ∈ H
⊢ x * g * x⁻¹ * (x * k * x⁻¹) ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Theorem: conjugate.mul_mem
Proof state before:
case intro.intro.intro.intro
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x g : G
hg : g ∈ H
k : G
hk : k ∈ H
⊢ x * g * x⁻¹ * (x * k * x⁻¹) ∈ {a | ∃ h ∈ H, a = x * h * x⁻¹}
Tactic:
use g * k, mul_mem hg hk
Proof state after:
case right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x g : G
hg : g ∈ H
k : G
hk : k ∈ H
⊢ x * g * x⁻¹ * (x * k * x⁻¹) = x * (g * k) * x⁻¹
Theorem: conjugate.mul_mem
Proof state before:
case right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x g : G
hg : g ∈ H
k : G
hk : k ∈ H
⊢ x * g * x⁻¹ * (x * k * x⁻¹) = x * (g * k) * x⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: 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: 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:
intro g
Proof state after:
G : Type
inst✝ : Group G
a b : G
H✝ K✝ : Subgroup G
x y z : G
H K : Subgroup G
h : H ≤ K
g : G
⊢ g ∈ conjugate H x → g ∈ conjugate K x
Theorem: 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
g : G
⊢ g ∈ conjugate H x → g ∈ conjugate K x
Tactic:
rintro ⟨t, ht, rfl⟩
Proof state after:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H✝ K✝ : Subgroup G
x y z : G
H K : Subgroup G
h : H ≤ K
t : G
ht : t ∈ H
⊢ x * t * x⁻¹ ∈ conjugate K x
Theorem: conjugate_mono
Proof state before:
case intro.intro
G : Type
inst✝ : Group G
a b : G
H✝ K✝ : Subgroup G
x y z : G
H K : Subgroup G
h : H ≤ K
t : G
ht : t ∈ H
⊢ x * t * x⁻¹ ∈ conjugate K x
Tactic:
exact ⟨t, h ht, rfl⟩
Proof state after:
no goals
Theorem: conjugate_bot
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ conjugate ⊥ x = ⊥
Tactic:
ext a
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ conjugate ⊥ x ↔ a ∈ ⊥
Theorem: conjugate_bot
Proof state before:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ conjugate ⊥ x ↔ a ∈ ⊥
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 a : G
⊢ (∃ h ∈ ⊥, a = x * h * x⁻¹) ↔ a ∈ ⊥
Theorem: conjugate_bot
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 * h * x⁻¹) ↔ a ∈ ⊥
Tactic:
rw [Subgroup.mem_bot]
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊥, a = x * h * x⁻¹) ↔ a = 1
Theorem: conjugate_bot
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 * h * x⁻¹) ↔ a = 1
Tactic:
constructor
Proof state after:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊥, a = x * h * x⁻¹) → a = 1

case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a = 1 → ∃ h ∈ ⊥, a = x * h * x⁻¹
Theorem: conjugate_bot
Proof state before:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊥, a = x * h * x⁻¹) → a = 1
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 b : G
hb : b ∈ ⊥
⊢ x * b * x⁻¹ = 1
Theorem: conjugate_bot
Proof state before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b ∈ ⊥
⊢ x * b * x⁻¹ = 1
Tactic:
rw [Subgroup.mem_bot] at hb
Proof state after:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * b * x⁻¹ = 1
Theorem: conjugate_bot
Proof state before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * b * x⁻¹ = 1
Tactic:
rw [hb]
Proof state after:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * 1 * x⁻¹ = 1
Theorem: conjugate_bot
Proof state before:
case h.mp.intro.intro
G : Type
inst✝ : Group G
a b✝ : G
H K : Subgroup G
x y z b : G
hb : b = 1
⊢ x * 1 * x⁻¹ = 1
Tactic:
group
Proof state after:
no goals
Theorem: conjugate_bot
Proof state before:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a = 1 → ∃ h ∈ ⊥, a = x * h * x⁻¹
Tactic:
rintro rfl
Proof state after:
case h.mpr
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ ∃ h ∈ ⊥, 1 = x * h * x⁻¹
Theorem: conjugate_bot
Proof state before:
case h.mpr
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ ∃ h ∈ ⊥, 1 = x * h * x⁻¹
Tactic:
use 1
Proof state after:
case h
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ ⊥ ∧ 1 = x * 1 * x⁻¹
Theorem: conjugate_bot
Proof state before:
case h
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ ⊥ ∧ 1 = x * 1 * x⁻¹
Tactic:
constructor
Proof state after:
case h.left
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ ⊥

case h.right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 = x * 1 * x⁻¹
Theorem: conjugate_bot
Proof state before:
case h.left
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 ∈ ⊥
Tactic:
rw [Subgroup.mem_bot]
Proof state after:
no goals
Theorem: conjugate_bot
Proof state before:
case h.right
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ 1 = x * 1 * x⁻¹
Tactic:
group
Proof state after:
no goals
Theorem: conjugate_top
Proof state before:
G : Type
inst✝ : Group G
a b : G
H K : Subgroup G
x y z : G
⊢ conjugate ⊤ x = ⊤
Tactic:
ext a
Proof state after:
case h
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ conjugate ⊤ x ↔ a ∈ ⊤
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
⊢ a ∈ conjugate ⊤ x ↔ a ∈ ⊤
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 a : G
⊢ (∃ h ∈ ⊤, a = x * h * x⁻¹) ↔ a ∈ ⊤
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 * h * x⁻¹) ↔ a ∈ ⊤
Tactic:
constructor
Proof state after:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊤, a = x * h * x⁻¹) → a ∈ ⊤

case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ ⊤ → ∃ h ∈ ⊤, a = x * h * x⁻¹
Theorem: conjugate_top
Proof state before:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ (∃ h ∈ ⊤, a = x * h * x⁻¹) → a ∈ ⊤
Tactic:
intro h
Proof state after:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : ∃ h ∈ ⊤, a = x * h * x⁻¹
⊢ a ∈ ⊤
Theorem: conjugate_top
Proof state before:
case h.mp
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : ∃ h ∈ ⊤, a = x * h * x⁻¹
⊢ a ∈ ⊤
Tactic:
exact Subgroup.mem_top a
Proof state after:
no goals
Theorem: conjugate_top
Proof state before:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
⊢ a ∈ ⊤ → ∃ h ∈ ⊤, a = x * h * x⁻¹
Tactic:
intro h
Proof state after:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ ∃ h ∈ ⊤, a = x * h * x⁻¹
Theorem: conjugate_top
Proof state before:
case h.mpr
G : Type
inst✝ : Group G
a✝ b : G
H K : Subgroup G
x y z a : G
h : a ∈ ⊤
⊢ ∃ 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 a : G
h : a ∈ ⊤
⊢ x⁻¹ * a * x ∈ ⊤ ∧ a = x * (x⁻¹ * a * x) * x⁻¹