awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Group R
inst_1 : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Eq (α := Subgroup R) (MulAction.stabilizer R m) (MulAction.stabilizer R (↑m : M))
have rw : Eq (α := Submonoid R) (Subgroup.toSubmonoid (MulAction.stabilizer R m))
  (Subgroup.toSubmonoid (MulAction.stabilizer R (↑m : M)))
Tactic: rw [← Subgroup.toSubmonoid_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
hx : x ∈ p
⊢ -x ∈ p
have rw : HSMul.hSMul.{u, v, v} (α := R) (-1) x ∈ p
Tactic: rw [← neg_one_smul R]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : SubMulAction R M
x : M
h : -x ∈ p
⊢ x ∈ p
have rw : - -x ∈ p
Tactic: rw [← neg_neg x]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Monoid M
inst_1 : MulAction M α
s : SubMulAction M α
⊢ Set.range (ι := ↥s) (⇑s.inclusion : (a : ↥s) → α) = s.carrier
have rw : Set.range (ι := ↥s) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) = s.carrier
Tactic: rw [inclusion.coe_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Monoid R
inst_1 : AddCommMonoid M
inst_2 : DistribMulAction R M
x y : { v : M // v ≠ 0 }
a : Rˣ
ha : (fun (m : Rˣ) ↦ m • (↑y : M)) a = (↑x : M)
⊢ (fun (m : Rˣ) ↦ m • y) a = x
have a₁ : (↑((fun (m : Rˣ) ↦ m • y) a) : M) = (↑x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
H : Subgroup G
hH : H.Normal
g : G
a : α
ha : a ∈ MulAction.fixedPoints.{u_1, u_2} (↥H) α
h : ↥H
⊢ h • g • a = g • a
have rw : (g⁻¹ * (↑h : G) * g) • a = a
Tactic: rw [Subgroup.smul_def, ← inv_smul_eq_iff, smul_smul, smul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Support (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group H
inst_1 : SMul G α
inst_2 : SMul G β
inst_3 : MulAction H α
inst_4 : SMul H β
inst_5 : SMulCommClass G H β
inst_6 : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
⊢ g' • g • b = g • b
have a : ∀ ⦃a : α⦄, a ∈ s → g' • a = a
Tactic: rw [smul_comm, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Support (hypothesis)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group H
inst_1 : SMul G α
inst_2 : SMul G β
inst_3 : MulAction H α
inst_4 : SMul H β
inst_5 : SMulCommClass G H β
inst_6 : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
⊢ g' • a = a
have this : g' • g • a = g • a
Tactic: have := Set.forall_mem_image.1 hg' ha
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Support (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group H
inst_1 : SMul G α
inst_2 : SMul G β
inst_3 : MulAction H α
inst_4 : SMul H β
inst_5 : SMulCommClass G H β
inst_6 : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
this : g' • g • a = g • a
⊢ g' • a = a
have a₁ : ∀ (this : g • g' • a = g • a), g' • a = a
Tactic: rwa [smul_comm, smul_left_cancel_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Support (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group H
inst_1 : SMul G α
inst_2 : SMul G β
inst_3 : MulAction H α
inst_4 : SMul H β
inst_5 : SMulCommClass G H β
inst_6 : SMulCommClass G H α
s : Set α
b : β
g : H
h : Supports G s b
g' : G
hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a
a : α
ha : a ∈ s
this : g' • g • a = g • a
a₁ : ∀ (this : g • g' • a = g • a), g' • a = a
⊢ g' • a = a
have a₂ : ∀ (this : g' • a = a), g' • a = a
Tactic: rwa [smul_comm, smul_left_cancel_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
⊢ ∃ (g : G), g • x = y
have obtain : ∀ (g : G) (hx : g • a = x), ∃ (g : G), g • x = y
Tactic: obtain ⟨g, hx⟩ := hG x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
g : G
hx : g • a = x
⊢ ∃ (g : G), g • x = y
have obtain : ∀ (h : G) (hy : h • a = y), ∃ (g : G), g • x = y
Tactic: obtain ⟨h, hy⟩ := hG y
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ (h * g⁻¹) • x = y
have rw : (h * g⁻¹) • g • a = y
Tactic: rw [← hx, smul_smul, inv_mul_cancel_right, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
rw : (h * g⁻¹) • g • a = y
⊢ (h * g⁻¹) • x = y
have rw₁ : (h * g⁻¹ * g) • a = y
Tactic: rw [← hx, smul_smul, inv_mul_cancel_right, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
hG : ∀ (x : X), ∃ (g : G), g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
rw : (h * g⁻¹) • g • a = y
rw₁ : (h * g⁻¹ * g) • a = y
rw₂ : h • a = y
⊢ (h * g⁻¹) • x = y
have rw₃ : y = y
Tactic: rw [← hx, smul_smul, inv_mul_cancel_right, hy]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
⊢ IsPretransitive G X ↔ orbit G a = Set.univ
have rw : (∀ (x : X), ∃ (g : G), g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ x
Tactic: rw [isPretransitive_iff_base a, Set.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
⊢ (∀ (x : X), ∃ (g : G), g • a = x) ↔ ∀ (x : X), x ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ x
have h : ∀ (a_1 : X), (∃ (g : G), g • a = a_1) ↔ (a_1 ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ a_1)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a x : X
⊢ (∃ (g : G), g • a = x) ↔ (x ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ x)
have h : (∃ (g : G), g • a = x) ↔ (x ∈ orbit G a ↔ True)
Tactic: simp_rw [Set.mem_univ, iff_true, mem_orbit_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a x : X
h : (∃ (g : G), g • a = x) ↔ (x ∈ orbit G a ↔ True)
⊢ (∃ (g : G), g • a = x) ↔ (x ∈ orbit G a ↔ Membership.mem (γ := Set X) Set.univ x)
have h₁ : (∃ (g : G), g • a = x) ↔ x ∈ orbit G a
Tactic: simp_rw [Set.mem_univ, iff_true, mem_orbit_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
⊢ IsPretransitive N β
have exists_smul_eq : ∀ (x y : β), ∃ (g : N), g • x = y
Tactic: apply MulAction.IsPretransitive.mk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
x y : β
⊢ ∃ (g : N), g • x = y
have exists_smul_eq : ∀ (x' : α), ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = y
Tactic: obtain ⟨x', rfl⟩ := hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
y : β
x' : α
⊢ ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = y
have exists_smul_eq : ∀ (y' : α), ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = (f : (a : α) → β) y'
Tactic: obtain ⟨y', rfl⟩ := hf y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPretransitive M α
x' y' : α
⊢ ∃ (g : N), HSMul.hSMul (β := β) g ((f : (a : α) → β) x' : β) = (f : (a : α) → β) y'
have exists_smul_eq : ∀ (g : M), ∃ (g_1 : N), HSMul.hSMul (β := β) g_1 ((f : (a : α) → β) x' : β) = (f : (a : α) → β) (g • x')
Tactic: obtain ⟨g, rfl⟩ := h.exists_smul_eq x' y'
Cleared hypotheses: y'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ IsPretransitive M α ↔ IsPretransitive N β
have mp : IsPretransitive M α → IsPretransitive N β
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
mp : IsPretransitive M α → IsPretransitive N β
⊢ IsPretransitive M α ↔ IsPretransitive N β
have mpr : IsPretransitive N β → IsPretransitive M α
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
⊢ IsPretransitive M α
have mpr : ∀ (x y : α), ∃ (g : M), g • x = y
Tactic: apply IsPretransitive.mk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
⊢ ∃ (g : M), g • x = y
have mpr : ∀ (k : N) (hk : HSMul.hSMul (β := β) k ((f : (a : α) → β) x : β) = (f : (a : α) → β) y), ∃ (g : M), g • x = y
Tactic: obtain ⟨k, hk⟩ := hN.exists_smul_eq (f x) (f y)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
k : N
hk : HSMul.hSMul (β := β) k ((f : (a : α) → β) x : β) = (f : (a : α) → β) y
⊢ ∃ (g : M), g • x = y
have mpr : ∀ (g : M) (hk : HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) y), ∃ (g : M), g • x = y
Tactic: obtain ⟨g, rfl⟩ := hφ k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
g : M
hk : HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) y
⊢ ∃ (g : M), g • x = y
have h : g • x = y
Tactic: use g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Transitive (goal)
Goal:
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction M α
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_5 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
hN : IsPretransitive N β
x y : α
g : M
hk : HSMul.hSMul (β := β) (φ g) ((f : (a : α) → β) x : β) = (f : (a : α) → β) y
⊢ g • x = y
have h : Eq.{u_6 + 1} (α := β) ((f : (a : α) → β) (g • x) : β) ((f : (a : α) → β) y : β)
Tactic: apply hf.injective
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)
have obtain : ∀ (n : N)
  (hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E)),
  ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)
Tactic: obtain ⟨n, hn⟩ := mul_inv_mem_range_inl σ σ' g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E)
⊢ (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)
have rw : (σ : (a : G) → E) g =
  HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E))
    ((σ' : (a : G) → E) g : E)
Tactic: rw [hn, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E)
rw :
  (σ : (a : G) → E) g =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g : E) (((σ' : (a : G) → E) g)⁻¹ : E))
      ((σ' : (a : G) → E) g : E)
⊢ (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ' : (a : G) → E) g : E)
have rw₁ : Eq.{u_3 + 1} (α := E) ((σ : (a : G) → E) g : E) ((σ : (a : G) → E) g : E)
Tactic: rw [hn, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
⊢ ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)
have obtain : ∀ (n : N)
  (hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E)),
  ∃ (n : N), (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)
Tactic: obtain ⟨n, hn⟩ := inv_mul_mem_range_inl σ' σ g
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E)
⊢ (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)
have rw : (σ : (a : G) → E) g =
  HMul.hMul (α := E) ((σ' : (a : G) → E) g : E)
    (HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E))
Tactic: rw [hn, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : (S.inl : (a : N) → E) n = HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E)
rw :
  (σ : (a : G) → E) g =
    HMul.hMul (α := E) ((σ' : (a : G) → E) g : E)
      (HMul.hMul (α := E) (β := E) (((σ' : (a : G) → E) g)⁻¹ : E) ((σ : (a : G) → E) g : E))
⊢ (σ : (a : G) → E) g = HMul.hMul (α := E) (β := E) ((σ' : (a : G) → E) g : E) ((S.inl : (a : N) → E) n : E)
have rw₁ : Eq.{u_3 + 1} (α := E) ((σ : (a : G) → E) g : E) ((σ : (a : G) → E) g : E)
Tactic: rw [hn, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
⊢ ∃ (n : N),
    (σ : (a : G) → E) (g₁ * g₂) =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) g₁ : E))
        ((σ : (a : G) → E) g₂ : E)
have obtain : ∀ (n : N)
  (hn :
    (S.inl : (a : N) → E) n =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
        (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)),
  ∃ (n : N),
    (σ : (a : G) → E) (g₁ * g₂) =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) g₁ : E))
        ((σ : (a : G) → E) g₂ : E)
Tactic: obtain ⟨n, hn⟩ := mul_mul_mul_inv_mem_range_inl σ g₁ g₂
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
⊢ ∃ (n : N),
    (σ : (a : G) → E) (g₁ * g₂) =
      HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) g₁ : E))
        ((σ : (a : G) → E) g₂ : E)
have h : (σ : (a : G) → E) (g₁ * g₂) =
  HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
    ((σ : (a : G) → E) g₂ : E)
Tactic: use n⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
⊢ (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
have h : (σ : (a : G) → E) (g₁ * g₂) =
  HMul.hMul (α := E) ((S.inl : (a : N) → E) n⁻¹ : E)
    (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
Tactic: rw [mul_assoc, map_inv, eq_inv_mul_iff_mul_eq, ← eq_mul_inv_iff_mul_eq, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
h :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (α := E) ((S.inl : (a : N) → E) n⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
⊢ (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
have h₁ : (σ : (a : G) → E) (g₁ * g₂) =
  HMul.hMul (α := E) (((S.inl : (a : N) → E) n)⁻¹ : E)
    (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
Tactic: rw [mul_assoc, map_inv, eq_inv_mul_iff_mul_eq, ← eq_mul_inv_iff_mul_eq, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
h :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (α := E) ((S.inl : (a : N) → E) n⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
h₁ :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (α := E) (((S.inl : (a : N) → E) n)⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
⊢ (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
have h₂ : HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) (g₁ * g₂) : E) =
  HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E)
Tactic: rw [mul_assoc, map_inv, eq_inv_mul_iff_mul_eq, ← eq_mul_inv_iff_mul_eq, hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupExtension.Basic (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
E : Type u_3
inst_2 : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
h :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (α := E) ((S.inl : (a : N) → E) n⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
h₁ :
  (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (α := E) (((S.inl : (a : N) → E) n)⁻¹ : E)
      (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
h₂ :
  HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n : E) ((σ : (a : G) → E) (g₁ * g₂) : E) =
    HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E)
h₃ :
  (S.inl : (a : N) → E) n =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
      (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
⊢ (σ : (a : G) → E) (g₁ * g₂) =
    HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((S.inl : (a : N) → E) n⁻¹ : E) ((σ : (a : G) → E) g₁ : E))
      ((σ : (a : G) → E) g₂ : E)
have h₄ : HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
    (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E) =
  HMul.hMul (β := E) (HMul.hMul (α := E) (β := E) ((σ : (a : G) → E) g₁ : E) ((σ : (a : G) → E) g₂ : E))
    (((σ : (a : G) → E) (g₁ * g₂))⁻¹ : E)
Tactic: rw [mul_assoc, map_inv, eq_inv_mul_iff_mul_eq, ← eq_mul_inv_iff_mul_eq, hn]