awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = H → H = ⊤
h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₆ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₇ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₀ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₁ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₁₃ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = H → H = ⊤
h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₆ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₇ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₀ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₁ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₃ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₁₄ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = H → H = ⊤
h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₆ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₇ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₀ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₁ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₃ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₄ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₁₅ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = H → H = ⊤
h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₆ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₇ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₀ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₁ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₃ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₄ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₅ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₆ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₇ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₈ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₉ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₂₀ h₂₁ h₂₂ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₂₃ : ¬normalizer (↑H : Set G) = H → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = H → H = ⊤
h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₆ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₇ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₀ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₁ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₃ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₄ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₅ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₆ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₇ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₈ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₉ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₂₀ h₂₁ h₂₂ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₂₃ h₂₄ h₂₅ : ¬normalizer (↑H : Set G) = H → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₂₆ : H = ⊤ → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = H → H = ⊤
h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₄ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₅ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₆ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = H → H = ⊤
h₇ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₀ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₁ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)
h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₃ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
h₁₄ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₅ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₆ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₇ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₁₈ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
h₁₉ : normalizer (↑H : Set G) = H → ¬¬H = ⊤ → H = ⊤
h₂₀ h₂₁ h₂₂ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = H → H = ⊤
h₂₃ h₂₄ h₂₅ : ¬normalizer (↑H : Set G) = H → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
h₂₆ : H = ⊤ → H = normalizer (↑H : Set G) → H ≤ ⊤ → ¬H = ⊤ → False
h₂₇ h₂₈ h₂₉ : normalizer (↑H : Set G) = H → ¬H ≤ ⊤ → H = ⊤
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₃₀ : normalizer (↑H : Set G) = H → H = ⊤ → H = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
x : G
⊢ x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x
have rw : (∃ (i : G) (_ : i ∈ s), x ∈ conjugatesOf i) ↔ ∃ a ∈ s, IsConj a x
Tactic: rw [conjugatesOfSet, Set.mem_iUnion₂]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
tn : N.Normal
a_1 : G
h : a_1 ∈ N
a : G
hc : a ∈ conjugatesOf a_1
⊢ a ∈ (↑N : Set G)
have obtain : ∀ (c : G) (hc : c * a_1 * c⁻¹ ∈ conjugatesOf a_1), c * a_1 * c⁻¹ ∈ (↑N : Set G)
Tactic: obtain ⟨c, rfl⟩ := isConj_iff.1 hc
Cleared hypotheses: a, hc
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s
have rcases : ∀ (a : G) (h₁ : a ∈ s) (h₂ : IsConj a x), c * x * c⁻¹ ∈ conjugatesOfSet s
Tactic: rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g : G
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * n * g⁻¹)
have refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
Tactic: refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g : G
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * n * g⁻¹)
have refine_2 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * 1 * g⁻¹)
Tactic: refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g : G
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
refine_2 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * 1 * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * n * g⁻¹)
have refine_3 : ∀ (x y : G),
  Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
    Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y →
      ∀ (ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹))
        (ihy : Membership.mem (γ := Subgroup G) (normalClosure s) (g * y * g⁻¹)),
        Membership.mem (γ := Subgroup G) (normalClosure s) (g * (x * y) * g⁻¹)
Tactic: refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g : G
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
refine_2 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * 1 * g⁻¹)
refine_3 :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
      Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y →
        ∀ (ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹))
          (ihy : Membership.mem (γ := Subgroup G) (normalClosure s) (g * y * g⁻¹)),
          Membership.mem (γ := Subgroup G) (normalClosure s) (g * (x * y) * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * n * g⁻¹)
have refine_4 : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
    ∀ (ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)),
      Membership.mem (γ := Subgroup G) (normalClosure s) (g * x⁻¹ * g⁻¹)
Tactic: refine Subgroup.closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_)
      (fun x _ ihx => ?_) h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x y : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
h_2 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
ihy : Membership.mem (γ := Subgroup G) (normalClosure s) (g * y * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * (x * y) * g⁻¹)
have refine_3 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹ * (g * y * g⁻¹))
Tactic: rw [← conj_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
n : G
h : Membership.mem (γ := Subgroup G) (normalClosure s) n
g x : G
h_1 : Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x
ihx : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)
⊢ Membership.mem (γ := Subgroup G) (normalClosure s) (g * x⁻¹ * g⁻¹)
have refine_4 : Membership.mem (γ := Subgroup G) (normalClosure s) (g * x * g⁻¹)⁻¹
Tactic: rw [← conj_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
⊢ a ∈ N
have refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), x ∈ N
Tactic: refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), x ∈ N
⊢ a ∈ N
have refine_2 : 1 ∈ N
Tactic: refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), x ∈ N
refine_2 : 1 ∈ N
⊢ a ∈ N
have refine_3 : ∀ (x y : G),
  Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
    Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y → ∀ (ihx : x ∈ N) (ihy : y ∈ N), x * y ∈ N
Tactic: refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
N : Subgroup G
inst_1 : N.Normal
h : s ⊆ (↑N : Set G)
a : G
w : Membership.mem (γ := Subgroup G) (normalClosure s) a
refine_1 : ∀ (x : G) (hx : x ∈ conjugatesOfSet s), x ∈ N
refine_2 : 1 ∈ N
refine_3 :
  ∀ (x y : G),
    Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x →
      Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) y → ∀ (ihx : x ∈ N) (ihy : y ∈ N), x * y ∈ N
⊢ a ∈ N
have refine_4 : ∀ (x : G), Membership.mem (γ := Subgroup G) (closure (conjugatesOfSet s)) x → ∀ (ihx : x ∈ N), x⁻¹ ∈ N
Tactic: refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
⊢ Eq (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}
have rw : LE.le (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}
Tactic: rw [eq_bot_iff, ← normalClosure_subset_iff, coe_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
rw : LE.le (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}
⊢ Eq (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}
have rw₁ : s ⊆ (↑⊥ : Set G) ↔ s ⊆ {1}
Tactic: rw [eq_bot_iff, ← normalClosure_subset_iff, coe_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
s : Set G
rw : LE.le (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}
rw₁ : s ⊆ (↑⊥ : Set G) ↔ s ⊆ {1}
⊢ Eq (α := Subgroup G) (normalClosure s) ⊥ ↔ s ⊆ {1}
have rw₂ : s ⊆ {1} ↔ s ⊆ {1}
Tactic: rw [eq_bot_iff, ← normalClosure_subset_iff, coe_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Eq.{u_1 + 1} (α := Subgroup G) (normalClosure ∅) ⊥
have rw : Eq (α := Subgroup G) (normalClosure (↑(closure ∅) : Set G)) ⊥
Tactic: rw [← normalClosure_closure_eq_normalClosure, closure_empty, normalClosure_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq (α := Subgroup G) (normalClosure (↑(closure ∅) : Set G)) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup G) (normalClosure ∅) ⊥
have rw₁ : Eq (α := Subgroup G) (normalClosure (↑⊥ : Set G)) ⊥
Tactic: rw [← normalClosure_closure_eq_normalClosure, closure_empty, normalClosure_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq (α := Subgroup G) (normalClosure (↑(closure ∅) : Set G)) ⊥
rw₁ : Eq (α := Subgroup G) (normalClosure (↑⊥ : Set G)) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup G) (normalClosure ∅) ⊥
have rw₂ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊥
Tactic: rw [← normalClosure_closure_eq_normalClosure, closure_empty, normalClosure_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
⊢ a * 1 * a⁻¹ ∈ H
have rw : 1 ∈ H
Tactic: rw [mul_one, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a ∈ H
have rw : 1 * a * 1⁻¹ ∈ H
Tactic: rw [← mul_one a, ← inv_one, ← one_mul a]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a * b⁻¹) * c⁻¹ ∈ H
have rw : c * b * a * (c * b)⁻¹ ∈ H
Tactic: rw [mul_assoc, mul_assoc, ← mul_inv_rev, ← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
G' : Type u_8
N' : Type u_9
inst_2 : Group G'
inst_3 : Group N'
f : G →* N
g : G' →* N'
⊢ (f.prodMap g).ker = f.ker.prod g.ker
have rw : comap (N := N × N') (f.prodMap g) ⊥ = f.ker.prod g.ker
Tactic: rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
G' : Type u_8
N' : Type u_9
inst_2 : Group G'
inst_3 : Group N'
f : G →* N
g : G' →* N'
rw : comap (N := N × N') (f.prodMap g) ⊥ = f.ker.prod g.ker
⊢ (f.prodMap g).ker = f.ker.prod g.ker
have rw₁ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod g.ker
Tactic: rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
G' : Type u_8
N' : Type u_9
inst_2 : Group G'
inst_3 : Group N'
f : G →* N
g : G' →* N'
rw : comap (N := N × N') (f.prodMap g) ⊥ = f.ker.prod g.ker
rw₁ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod g.ker
⊢ (f.prodMap g).ker = f.ker.prod g.ker
have rw₂ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod (comap g ⊥)
Tactic: rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
G' : Type u_8
N' : Type u_9
inst_2 : Group G'
inst_3 : Group N'
f : G →* N
g : G' →* N'
rw : comap (N := N × N') (f.prodMap g) ⊥ = f.ker.prod g.ker
rw₁ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod g.ker
rw₂ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod (comap g ⊥)
⊢ (f.prodMap g).ker = f.ker.prod g.ker
have rw₃ : Eq (α := Subgroup (G × G')) (comap (N := N × N') (f.prodMap g) ⊥) (comap (N := N × N') (f.prodMap g) (prod ⊥ ⊥))
Tactic: rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
G' : Type u_8
N' : Type u_9
inst_2 : Group G'
inst_3 : Group N'
f : G →* N
g : G' →* N'
rw : comap (N := N × N') (f.prodMap g) ⊥ = f.ker.prod g.ker
rw₁ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod g.ker
rw₂ : comap (N := N × N') (f.prodMap g) ⊥ = (comap f ⊥).prod (comap g ⊥)
rw₃ : Eq (α := Subgroup (G × G')) (comap (N := N × N') (f.prodMap g) ⊥) (comap (N := N × N') (f.prodMap g) (prod ⊥ ⊥))
⊢ (f.prodMap g).ker = f.ker.prod g.ker
have rw₄ : Eq (α := Subgroup (G × G')) (comap (N := N × N') (f.prodMap g) ⊥) (comap (N := N × N') (f.prodMap g) ⊥)
Tactic: rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ (Subgroup.map f H).Normal
have rw : Subgroup.map f (normalizer (↑H : Set G)) ≤ normalizer (↑(Subgroup.map f H) : Set N)
Tactic: rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map,
    ← H.normalizer_eq_top]