awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H : Set G) T
g : G
⊢ (g * (↑(hT.toRightFun (T := T) g) : G)⁻¹)⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹
have rw : (↑(hT.toRightFun (T := T) g) : G)⁻¹⁻¹ * g⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹
Tactic: rw [mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hT : IsComplement (↑H : Set G) T
g : G
rw : (↑(hT.toRightFun (T := T) g) : G)⁻¹⁻¹ * g⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹
⊢ (g * (↑(hT.toRightFun (T := T) g) : G)⁻¹)⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹
have rw₁ : (↑(hT.toRightFun (T := T) g) : G) * g⁻¹ = (↑(hT.toRightFun (T := T) g) : G) * g⁻¹
Tactic: rw [mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
inst_1 : H.FiniteIndex
h : IsComplement S (↑H : Set G)
⊢ S.encard = (↑H.index : ℕ∞)
have rw : Eq (α := ℕ∞) (↑S.ncard : ℕ∞) (↑H.index : ℕ∞)
Tactic: rw [← h.finite_left.cast_ncard_eq, h.ncard_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
S : Set G
inst_1 : H.FiniteIndex
h : IsComplement S (↑H : Set G)
rw : Eq (α := ℕ∞) (↑S.ncard : ℕ∞) (↑H.index : ℕ∞)
⊢ S.encard = (↑H.index : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑H.index : ℕ∞) (↑H.index : ℕ∞)
Tactic: rw [← h.finite_left.cast_ncard_eq, h.ncard_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
inst_1 : H.FiniteIndex
h : IsComplement (↑H : Set G) T
⊢ T.encard = (↑H.index : ℕ∞)
have rw : Eq (α := ℕ∞) (↑T.ncard : ℕ∞) (↑H.index : ℕ∞)
Tactic: rw [← h.finite_right.cast_ncard_eq, h.ncard_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
inst_1 : H.FiniteIndex
h : IsComplement (↑H : Set G) T
rw : Eq (α := ℕ∞) (↑T.ncard : ℕ∞) (↑H.index : ℕ∞)
⊢ T.encard = (↑H.index : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑H.index : ℕ∞) (↑H.index : ℕ∞)
Tactic: rw [← h.finite_right.cast_ncard_eq, h.ncard_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
⊢ IsComplement (f • (↑T : Set G)) (↑H : Set G)
have refine : ∀ (g : G), ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)
Tactic: refine isComplement_iff_existsUnique_inv_mul_mem.mpr fun g => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
⊢ ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)
have obtain : ∀ (t : (↑(↑T : Set G) : Type u_1)) (ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G))
  (ht2 :
    ∀ (y : (↑(↑T : Set G) : Type u_1)),
      (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t),
  ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)
Tactic: obtain ⟨t, ht1, ht2⟩ := isComplement_iff_existsUnique_inv_mul_mem.mp T.2 (f⁻¹ • g)
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
⊢ ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)
have refine_1 : (fun (s : (↑(f • (↑T : Set G)) : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ (↑H : Set G))
  (Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) sorry)
Tactic: refine ⟨⟨f • (t : G), Set.smul_mem_smul_set t.2⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
refine_1 :
  (fun (s : (↑(f • (↑T : Set G)) : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ (↑H : Set G))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯)
⊢ ∃! s : (↑(f • (↑T : Set G)) : Type u_1), (↑s : G)⁻¹ * g ∈ (↑H : Set G)
have refine_2 : ∀ (y : (↑(f • (↑T : Set G)) : Type u_1)),
  (fun (s : (↑(f • (↑T : Set G)) : Type u_1)) ↦ (↑s : G)⁻¹ * g ∈ (↑H : Set G)) y →
    y = Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) sorry
Tactic: refine ⟨⟨f • (t : G), Set.smul_mem_smul_set t.2⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
t' : G
ht' : t' ∈ (↑T : Set G)
h : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯) : G)⁻¹ * g ∈ (↑H : Set G)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯ =
    Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯
have h₁ : (f⁻¹ • (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') sorry) : G))⁻¹ * f⁻¹ • g ∈ H
Tactic: replace h := QuotientAction.inv_mul_mem f⁻¹ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
S T_1 : Set G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
T : H.LeftTransversal
g : G
t : (↑(↑T : Set G) : Type u_1)
ht1 : (↑t : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)
ht2 :
  ∀ (y : (↑(↑T : Set G) : Type u_1)),
    (fun (s : (↑(↑T : Set G) : Type u_1)) ↦ (↑s : G)⁻¹ * f⁻¹ • g ∈ (↑H : Set G)) y → y = t
t' : G
ht' : t' ∈ (↑T : Set G)
h : (f⁻¹ • (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯) : G))⁻¹ * f⁻¹ • g ∈ H
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) ((fun (x : G) ↦ f • x) t') ⋯ =
    Subtype.mk (p := fun (x : G) ↦ x ∈ f • (↑T : Set G)) (f • (↑t : G)) ⋯
have refine_2 : ∀ (h : t'⁻¹ * f⁻¹ • g ∈ H), t' = (↑t : G)
Tactic: simp only [Subtype.ext_iff, smul_left_cancel_iff, inv_smul_smul] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G) =
    HSMul.hSMul (β := G) f
      (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) (f⁻¹ • q)) : G)
have rw : Eq.{u_1 + 1} (α := G)
  (↑((sorry.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G)
  (↑((sorry.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) (f • f⁻¹ • q)) :
    G)
Tactic: rw [smul_leftQuotientEquiv, smul_inv_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
F : Type u_2
inst_1 : Group F
inst_2 : MulAction F G
inst_3 : QuotientAction F H
f : F
S : H.LeftTransversal
q : G ⧸ H
rw :
  Eq.{u_1 + 1} (α := G)
    (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G)
    (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) (f • f⁻¹ • q)) :
      G)
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G) =
    HSMul.hSMul (β := G) f
      (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) (f⁻¹ • q)) : G)
have rw₁ : Eq.{u_1 + 1} (α := G)
  (↑((sorry.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G)
  (↑((sorry.leftQuotientEquiv (S := (↑(f • S) : Set G)) : (a : G ⧸ H) → (↑(↑(f • S) : Set G) : Type u_1)) q) : G)
Tactic: rw [smul_leftQuotientEquiv, smul_inv_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ IsCompl H K
have fun : ∀ (g : G), Membership.mem (γ := Subgroup G) ⊤ g → g ∈ H ⊔ K
Tactic: refine
    ⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
        let x : H × K := ⟨⟨g, p⟩, 1⟩
        let y : H × K := ⟨1, g, q⟩
        Subtype.ext_iff.mp
          (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
      codisjoint_iff_le_sup.mpr fun g _ => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H.IsComplement' K
g : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ g
⊢ g ∈ H ⊔ K
have obtain : ∀ (h : (↑(↑H : Set G) : Type u_1)) (k : (↑(↑K : Set G) : Type u_1)),
  Membership.mem (γ := Subgroup G) ⊤
      ((fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k)) →
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) (h, k) ∈ H ⊔ K
Tactic: obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g
Cleared hypotheses: g, h_1
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : (↑H : Set G) * (↑K : Set G) = univ
⊢ H.IsComplement' K
have refine : ∀ (g : G),
  ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g
Tactic: refine ⟨mul_injective_of_disjoint h1, fun g => ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : (↑H : Set G) * (↑K : Set G) = univ
g : G
⊢ ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g
have obtain : ∀ (h : G) (hh : h ∈ (↑H : Set G)) (k : G) (hk : k ∈ (↑K : Set G)) (hg : (fun (x1 x2 : G) ↦ x1 * x2) h k = g),
  ∃ (a : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)),
    (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑K : Set G) : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G)) a = g
Tactic: obtain ⟨h, hh, k, hk, hg⟩ := Set.eq_univ_iff_forall.mp h2 g
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
⊢ H.IsComplement' (MulAction.stabilizer G a)
have refine : ∀ (g : G),
  ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
Tactic: refine isComplement_iff_existsUnique.mpr fun g => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
⊢ ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
have obtain : ∀ (h : ↥H) (hh : h • g • a = a),
  ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
Tactic: obtain ⟨h, hh⟩ := h2 g
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
⊢ ((↑h : G) * g) • a = a
have rwa : (↑h : G) • g • a = a
Tactic: rwa [mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
⊢ ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
have hh' : ((↑h : G) * g) • a = a
Tactic: have hh' : (↑h * g) • a = a := by rwa [mul_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
g : G
h : ↥H
hh : h • g • a = a
hh' : ((↑h : G) * g) • a = a
⊢ ∃! x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1), (↑x.1 : G) * (↑x.2 : G) = g
have refine : ∀ (y : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1)),
  (fun (x : (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1)) ↦
        (↑x.1 : G) * (↑x.2 : G) = g)
      y →
    y = (h⁻¹, Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) ((↑h : G) * g) hh')
Tactic: refine ⟨⟨h⁻¹, h * g, hh'⟩, inv_mul_cancel_left ↑h g, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
⊢ (h * h') • a = a
have rwa : h • h' • a = a
Tactic: rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
rwa : h • h' • a = a
⊢ (h * h') • a = a
have rwa₁ : h • (↑h' : G) • a = a
Tactic: rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
rwa : h • h' • a = a
rwa₁ : h • (↑h' : G) • a = a
⊢ (h * h') • a = a
have rwa₂ : h • (↑h' : G) • g • a = g • a
Tactic: rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
rwa : h • h' • a = a
rwa₁ : h • (↑h' : G) • a = a
rwa₂ : h • (↑h' : G) • g • a = g • a
⊢ (h * h') • a = a
have rwa₃ : h • ((↑h' : G) * g) • a = g • a
Tactic: rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
rwa : h • h' • a = a
rwa₁ : h • (↑h' : G) • a = a
rwa₂ : h • (↑h' : G) • g • a = g • a
rwa₃ : h • ((↑h' : G) * g) • a = g • a
⊢ (h * h') • a = a
have rwa₄ : h • ((↑h' : G) * g) • a = a
Tactic: rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h1 : ∀ (h : ↥H), h • a = a → h = 1
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
⊢ Eq (α := (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1))
    (h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg)
    (h⁻¹,
      Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
        ((↑h : G) *
          ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
            (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
        hh')
have h1₁ : h * h' = 1
Tactic: specialize h1 (h * h') (by rwa [mul_smul, smul_def h', ← hg, ← mul_smul, hg])
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
h1 : h * h' = 1
⊢ Eq (α := (↑(↑H : Set G) : Type u_1) × (↑(↑(MulAction.stabilizer G a) : Set G) : Type u_1))
    (h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg)
    (h⁻¹,
      Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
        ((↑h : G) *
          ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
            (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
        hh')
have refine : (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
  (↑(h⁻¹,
          Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
            ((↑h : G) *
              ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
            hh').2 :
    G)
Tactic: refine Prod.ext (eq_inv_of_mul_eq_one_right h1) (Subtype.ext ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
h1 : h * h' = 1
⊢ (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
have rwa : ∀ (h1 : (↑(h * h') : G) = (↑1 : G)),
  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
Tactic: rwa [Subtype.ext_iff, coe_one, coe_mul, ← right_eq_mul, mul_assoc (↑h) (↑h') g] at h1
Cleared hypotheses: h1