awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOpposite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
rw :
  Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))))
    (Subgroup.op (normalizer (↑H.unop : Set G)))
⊢ Eq (α := Subgroup G) (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))) (normalizer (↑H.unop : Set G))
have rw₁ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (Subgroup.op (normalizer (↑H.unop : Set G)))
Tactic: rw [← op_inj, op_unop, op_normalizer, op_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOpposite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
rw :
  Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))))
    (Subgroup.op (normalizer (↑H.unop : Set G)))
rw₁ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (Subgroup.op (normalizer (↑H.unop : Set G)))
⊢ Eq (α := Subgroup G) (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))) (normalizer (↑H.unop : Set G))
have rw₂ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (normalizer (↑H.unop.op : Set Gᵐᵒᵖ))
Tactic: rw [← op_inj, op_unop, op_normalizer, op_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOpposite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
rw :
  Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))))
    (Subgroup.op (normalizer (↑H.unop : Set G)))
rw₁ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (Subgroup.op (normalizer (↑H.unop : Set G)))
rw₂ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (normalizer (↑H.unop.op : Set Gᵐᵒᵖ))
⊢ Eq (α := Subgroup G) (Subgroup.unop (normalizer (↑H : Set Gᵐᵒᵖ))) (normalizer (↑H.unop : Set G))
have rw₃ : Eq (α := Subgroup Gᵐᵒᵖ) (normalizer (↑H : Set Gᵐᵒᵖ)) (normalizer (↑H : Set Gᵐᵒᵖ))
Tactic: rw [← op_inj, op_unop, op_normalizer, op_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ Eq (α := Subgroup Gᵐᵒᵖ) (Subgroup.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))
have simp_rw : Eq.{u_2 + 1} (α := Subgroup Gᵐᵒᵖ) (sInf {a : Subgroup Gᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ)})
  (sInf {K : Subgroup Gᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑K : Set Gᵐᵒᵖ)})
Tactic: simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subgroup.coe_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ Eq.{u_2 + 1} (α := Subgroup Gᵐᵒᵖ) (sInf {a : Subgroup Gᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ)})
    (sInf {K : Subgroup Gᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑K : Set Gᵐᵒᵖ)})
have e_a : ∀ (a : Subgroup Gᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Gᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Gᵐᵒᵖ)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (goal)
Goal:
G : Type u_2
inst : Group G
s : Set Gᵐᵒᵖ
⊢ Eq (α := Subgroup G) (Subgroup.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))
have rw : Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
Tactic: rw [← op_inj, op_unop, op_closure]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (goal)
Goal:
G : Type u_2
inst : Group G
s : Set Gᵐᵒᵖ
⊢ Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw : Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure ((fun (x : Gᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (goal)
Goal:
G : Type u_2
inst : Group G
s : Set Gᵐᵒᵖ
simp_rw : Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure ((fun (x : Gᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
⊢ Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw₁ : Eq (α := Subgroup Gᵐᵒᵖ) (closure s) (closure ((fun (x : Gᵐᵒᵖ) ↦ x) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.Normal ↔ H.Normal
have rw : H.unop.op.Normal ↔ H.Normal
Tactic: rw [← normal_op, op_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gᵐᵒᵖ
rw : H.unop.op.Normal ↔ H.Normal
⊢ H.unop.Normal ↔ H.Normal
have rw₁ : H.Normal ↔ H.Normal
Tactic: rw [← normal_op, op_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
S : Type u_1
G : Type u_2
inst : Group G
inst_1 : LinearOrder G
x_1 : SetLike S G
inst_2 : InvMemClass S G
H : S
x : G
⊢ |x|ₘ ∈ H ↔ x ∈ H
have inl : |x|ₘ = x → (|x|ₘ ∈ H ↔ x ∈ H)
Tactic: cases mabs_choice x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
S : Type u_1
G : Type u_2
inst : Group G
inst_1 : LinearOrder G
x_1 : SetLike S G
inst_2 : InvMemClass S G
H : S
x : G
inl : |x|ₘ = x → (|x|ₘ ∈ H ↔ x ∈ H)
⊢ |x|ₘ ∈ H ↔ x ∈ H
have inr : |x|ₘ = x⁻¹ → (|x|ₘ ∈ H ↔ x ∈ H)
Tactic: cases mabs_choice x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (hypothesis)
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : a ∈ (x ⊔ y) ⊓ z
⊢ a ∈ x ⊔ y ⊓ z
have ha₁ : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
Tactic: rw [mem_inf, mem_sup] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
a : C
ha : (∃ y_1 ∈ x, ∃ z ∈ y, y_1 * z = a) ∧ a ∈ z
⊢ a ∈ x ⊔ y ⊓ z
have rcases : ∀ (b : C) (hb : b ∈ x) (c : C) (hc : c ∈ y) (haz : b * c ∈ z), b * c ∈ x ⊔ y ⊓ z
Tactic: rcases ha with ⟨⟨b, hb, c, hc, rfl⟩, haz⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
C : Type u_1
inst : CommGroup C
x y z : Subgroup C
xz : x ≤ z
b : C
hb : b ∈ x
c : C
hc : c ∈ y
haz : b * c ∈ z
⊢ b * c ∈ x ⊔ y ⊓ z
have rw : ∃ y_1 ∈ x, ∃ z_1 ∈ y ⊓ z, y_1 * z_1 = b * c
Tactic: rw [mem_sup]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : IsCoatom M
⊢ IsCoatom (comap φ M)
have refine_1 : ∀ (hM : M ≠ ⊤), comap φ M ≠ ⊤
Tactic: refine And.imp (fun hM ↦ ?_) (fun hM ↦ ?_) hM
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM : IsCoatom M
refine_1 : ∀ (hM : M ≠ ⊤), comap φ M ≠ ⊤
⊢ IsCoatom (comap φ M)
have refine_2 : ∀ (hM : ∀ (b : Subgroup H), M < b → b = ⊤) (b : Subgroup G), comap φ M < b → b = ⊤
Tactic: refine And.imp (fun hM ↦ ?_) (fun hM ↦ ?_) hM
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
hM : M ≠ ⊤
⊢ comap φ M ≠ ⊤
have refine_1 : ∀ (hM : comap φ M ≠ comap φ ⊤), comap φ M ≠ ⊤
Tactic: rwa [← (comap_injective hφ).ne_iff, comap_top] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
hM : M ≠ ⊤
refine_1 : ∀ (hM : comap φ M ≠ comap φ ⊤), comap φ M ≠ ⊤
⊢ comap φ M ≠ ⊤
have refine_1₁ : ∀ (hM : comap φ M ≠ ⊤), comap φ M ≠ ⊤
Tactic: rwa [← (comap_injective hφ).ne_iff, comap_top] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
K : Subgroup G
hK : comap φ M < K
⊢ K = ⊤
have hM₁ : M < map φ K → map φ K = ⊤
Tactic: specialize hM (K.map φ)
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : M < map φ K → map φ K = ⊤
⊢ K = ⊤
have hM₁ : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
Tactic: rw [← comap_lt_comap_of_surjective hφ, ← (comap_injective hφ).eq_iff] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Order (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Type u_2
inst_1 : Group H
φ : G →* H
hφ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
M : Subgroup H
hM_1 : IsCoatom M
K : Subgroup G
hK : comap φ M < K
hM : comap φ M < comap φ (map φ K) → comap φ (map φ K) = comap φ ⊤
⊢ K = ⊤
have hM₁ : comap φ M < K → K = ⊤
Tactic: rw [comap_map_eq_self ((M.ker_le_comap φ).trans hK.le), comap_top] at hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
S : Type u_4
inst : Group G
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ a • (↑s : Set G) = (↑s : Set G)
have h : ∀ (x : G), x ∈ a • (↑s : Set G) ↔ x ∈ (↑s : Set G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
S : Type u_4
inst : Group G
inst_1 : SetLike S G
inst_2 : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ MulOpposite.op a • (↑s : Set G) = (↑s : Set G)
have h : ∀ (x : G), x ∈ MulOpposite.op a • (↑s : Set G) ↔ x ∈ (↑s : Set G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ s * (↑(closure s) : Set G) = (↑(closure s) : Set G)
have rw : ⋃ a ∈ s, a • (↑(closure s) : Set G) = (↑(closure s) : Set G)
Tactic: rw [← smul_eq_mul, ← Set.iUnion_smul_set]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (hypothesis)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, a • (↑(closure s) : Set G) = (↑(closure s) : Set G)
have h : ∀ (a : G) (ha : a ∈ s), a • (↑(closure s) : Set G) = (↑(closure s) : Set G)
Tactic: have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
    smul_coe_set <| subset_closure ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ (↑(closure s) : Set G) * s = (↑(closure s) : Set G)
have rw : ⋃ a ∈ s, (↑(closure s) : Set G) <• a = (↑(closure s) : Set G)
Tactic: rw [← Set.iUnion_op_smul_set]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (hypothesis)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, (↑(closure s) : Set G) <• a = (↑(closure s) : Set G)
have h : ∀ (a : G) (ha : a ∈ s), (↑(closure s) : Set G) <• a = (↑(closure s) : Set G)
Tactic: have h a (ha : a ∈ s) : (closure s : Set G) <• a = closure s :=
    op_smul_coe_set <| subset_closure ha
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ (n + 1) * (↑(closure s) : Set G) = (↑(closure s) : Set G)
have rw : s ^ n * s * (↑(closure s) : Set G) = (↑(closure s) : Set G)
Tactic: rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : s ^ n * s * (↑(closure s) : Set G) = (↑(closure s) : Set G)
⊢ s ^ (n + 1) * (↑(closure s) : Set G) = (↑(closure s) : Set G)
have rw₁ : s ^ n * (s * (↑(closure s) : Set G)) = (↑(closure s) : Set G)
Tactic: rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : s ^ n * s * (↑(closure s) : Set G) = (↑(closure s) : Set G)
rw₁ : s ^ n * (s * (↑(closure s) : Set G)) = (↑(closure s) : Set G)
⊢ s ^ (n + 1) * (↑(closure s) : Set G) = (↑(closure s) : Set G)
have rw₂ : s ^ n * (↑(closure s) : Set G) = (↑(closure s) : Set G)
Tactic: rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : s ^ n * s * (↑(closure s) : Set G) = (↑(closure s) : Set G)
rw₁ : s ^ n * (s * (↑(closure s) : Set G)) = (↑(closure s) : Set G)
rw₂ : s ^ n * (↑(closure s) : Set G) = (↑(closure s) : Set G)
⊢ s ^ (n + 1) * (↑(closure s) : Set G) = (↑(closure s) : Set G)
have rw₃ : (↑(closure s) : Set G) = (↑(closure s) : Set G)
Tactic: rw [pow_succ, mul_assoc, mul_subgroupClosure hs, pow_mul_subgroupClosure hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ (↑(closure s) : Set G) * s ^ (n + 1) = (↑(closure s) : Set G)
have rw : (↑(closure s) : Set G) * (s * s ^ n) = (↑(closure s) : Set G)
Tactic: rw [pow_succ', ← mul_assoc, subgroupClosure_mul hs, subgroupClosure_mul_pow hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : (↑(closure s) : Set G) * (s * s ^ n) = (↑(closure s) : Set G)
⊢ (↑(closure s) : Set G) * s ^ (n + 1) = (↑(closure s) : Set G)
have rw₁ : (↑(closure s) : Set G) * s * s ^ n = (↑(closure s) : Set G)
Tactic: rw [pow_succ', ← mul_assoc, subgroupClosure_mul hs, subgroupClosure_mul_pow hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : (↑(closure s) : Set G) * (s * s ^ n) = (↑(closure s) : Set G)
rw₁ : (↑(closure s) : Set G) * s * s ^ n = (↑(closure s) : Set G)
⊢ (↑(closure s) : Set G) * s ^ (n + 1) = (↑(closure s) : Set G)
have rw₂ : (↑(closure s) : Set G) * s ^ n = (↑(closure s) : Set G)
Tactic: rw [pow_succ', ← mul_assoc, subgroupClosure_mul hs, subgroupClosure_mul_pow hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
hs : s.Nonempty
n : ℕ
rw : (↑(closure s) : Set G) * (s * s ^ n) = (↑(closure s) : Set G)
rw₁ : (↑(closure s) : Set G) * s * s ^ n = (↑(closure s) : Set G)
rw₂ : (↑(closure s) : Set G) * s ^ n = (↑(closure s) : Set G)
⊢ (↑(closure s) : Set G) * s ^ (n + 1) = (↑(closure s) : Set G)
have rw₃ : (↑(closure s) : Set G) = (↑(closure s) : Set G)
Tactic: rw [pow_succ', ← mul_assoc, subgroupClosure_mul hs, subgroupClosure_mul_pow hs]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
s : G
hs : s ∈ S⁻¹
⊢ s ∈ (↑(closure S) : Set G)
have rw : Membership.mem (γ := Subgroup G) (closure S) s⁻¹
Tactic: rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
⊢ Eq (α := Submonoid G) (toSubmonoid (closure S)) (Submonoid.closure (S ∪ S⁻¹))
have refine_1 : ∀ (x : G) (hx : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x),
  Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
Tactic: refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
refine_1 :
  ∀ (x : G) (hx : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x),
    Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
⊢ Eq (α := Submonoid G) (toSubmonoid (closure S)) (Submonoid.closure (S ∪ S⁻¹))
have refine_2 : S ∪ S⁻¹ ⊆ (↑(toSubmonoid (closure S)) : Set G)
Tactic: refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
x : G
hx : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
have refine_1 : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (closure S) x →
    ∀ (hx : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x),
      Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x⁻¹
Tactic: refine
      closure_induction
        (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
        (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
x_1 : G
hx_1 : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x_1
x : G
h : Membership.mem (γ := Subgroup G) (closure S) x
hx : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x⁻¹
have refine_1 : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)⁻¹) x
Tactic: rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
x_1 : G
hx_1 : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x_1
x : G
h : Membership.mem (γ := Subgroup G) (closure S) x
hx : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
refine_1 : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)⁻¹) x
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x⁻¹
have refine_1₁ : Membership.mem (γ := Submonoid G) (Submonoid.closure (S⁻¹ ∪ S⁻¹⁻¹)) x
Tactic: rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
x_1 : G
hx_1 : Membership.mem (γ := Submonoid G) (toSubmonoid (closure S)) x_1
x : G
h : Membership.mem (γ := Subgroup G) (closure S) x
hx : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x
refine_1 : Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)⁻¹) x
refine_1₁ : Membership.mem (γ := Submonoid G) (Submonoid.closure (S⁻¹ ∪ S⁻¹⁻¹)) x
⊢ Membership.mem (γ := Submonoid G) (Submonoid.closure (S ∪ S⁻¹)) x⁻¹
have refine_1₂ : Membership.mem (γ := Submonoid G) (Submonoid.closure (S⁻¹ ∪ S)) x
Tactic: rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
g : G
⊢ Eq (α := Submonoid G) (toSubmonoid (zpowers g)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
have rw : Eq (α := Submonoid G) (toSubmonoid (closure {g})) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
Tactic: rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
g : G
rw : Eq (α := Submonoid G) (toSubmonoid (closure {g})) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
⊢ Eq (α := Submonoid G) (toSubmonoid (zpowers g)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
have rw₁ : Eq (α := Submonoid G) (Submonoid.closure ({g} ∪ {g}⁻¹)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
Tactic: rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
g : G
rw : Eq (α := Submonoid G) (toSubmonoid (closure {g})) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₁ : Eq (α := Submonoid G) (Submonoid.closure ({g} ∪ {g}⁻¹)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
⊢ Eq (α := Submonoid G) (toSubmonoid (zpowers g)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
have rw₂ : Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
Tactic: rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
g : G
rw : Eq (α := Submonoid G) (toSubmonoid (closure {g})) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₁ : Eq (α := Submonoid G) (Submonoid.closure ({g} ∪ {g}⁻¹)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₂ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
⊢ Eq (α := Submonoid G) (toSubmonoid (zpowers g)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
have rw₃ : Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.closure {g} ⊔ Submonoid.powers g⁻¹)
Tactic: rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
g : G
rw : Eq (α := Submonoid G) (toSubmonoid (closure {g})) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₁ : Eq (α := Submonoid G) (Submonoid.closure ({g} ∪ {g}⁻¹)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₂ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₃ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.closure {g} ⊔ Submonoid.powers g⁻¹)
⊢ Eq (α := Submonoid G) (toSubmonoid (zpowers g)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
have rw₄ : Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹)
  (Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹})
Tactic: rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
g : G
rw : Eq (α := Submonoid G) (toSubmonoid (closure {g})) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₁ : Eq (α := Submonoid G) (Submonoid.closure ({g} ∪ {g}⁻¹)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₂ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
rw₃ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹) (Submonoid.closure {g} ⊔ Submonoid.powers g⁻¹)
rw₄ :
  Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g}⁻¹)
    (Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹})
⊢ Eq (α := Submonoid G) (toSubmonoid (zpowers g)) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
have rw₅ : Eq (α := Submonoid G) (Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹})
  (Submonoid.closure {g} ⊔ Submonoid.closure {g⁻¹})
Tactic: rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
g : G
⊢ LE.le (α := Submonoid G) (Submonoid.powers g) (toSubmonoid (zpowers g))
have rw : LE.le (α := Submonoid G) (Submonoid.powers g) (Submonoid.powers g ⊔ Submonoid.powers g⁻¹)
Tactic: rw [toSubmonoid_zpowers]