awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : Eq.{u_1 + 1} (α := Subgroup ↥H) (_root_.commutator ↥H) ⊤ ↔ ⁅H, H⁆ = H
⊢ IsPerfect.{u_1} ↥H ↔ ⁅H, H⁆ = H
have rw₁ : map H.subtype (_root_.commutator ↥H) = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
Tactic: rw [Group.isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : Eq.{u_1 + 1} (α := Subgroup ↥H) (_root_.commutator ↥H) ⊤ ↔ ⁅H, H⁆ = H
rw₁ : map H.subtype (_root_.commutator ↥H) = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
⊢ IsPerfect.{u_1} ↥H ↔ ⁅H, H⁆ = H
have rw₂ : ⁅H, H⁆ = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
Tactic: rw [Group.isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : Eq.{u_1 + 1} (α := Subgroup ↥H) (_root_.commutator ↥H) ⊤ ↔ ⁅H, H⁆ = H
rw₁ : map H.subtype (_root_.commutator ↥H) = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
rw₂ : ⁅H, H⁆ = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
⊢ IsPerfect.{u_1} ↥H ↔ ⁅H, H⁆ = H
have rw₃ : ⁅H, H⁆ = H.subtype.range ↔ ⁅H, H⁆ = H
Tactic: rw [Group.isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : Eq.{u_1 + 1} (α := Subgroup ↥H) (_root_.commutator ↥H) ⊤ ↔ ⁅H, H⁆ = H
rw₁ : map H.subtype (_root_.commutator ↥H) = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
rw₂ : ⁅H, H⁆ = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
rw₃ : ⁅H, H⁆ = H.subtype.range ↔ ⁅H, H⁆ = H
⊢ IsPerfect.{u_1} ↥H ↔ ⁅H, H⁆ = H
have rw₄ : ⁅H, H⁆ = H ↔ ⁅H, H⁆ = H
Tactic: rw [Group.isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G
have rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
Tactic: rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G
have rw₁ : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
Tactic: rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
rw₁ : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G
have rw₂ : Eq.{u_1 + 1} (α := Subgroup G) (map (G := ↥⊤) (Subgroup.subtype ⊤) (_root_.commutator ↥⊤))
    (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
  Eq (α := Subgroup G) (_root_.commutator G) ⊤
Tactic: rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
rw₁ : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₂ :
  Eq.{u_1 + 1} (α := Subgroup G) (map (G := ↥⊤) (Subgroup.subtype ⊤) (_root_.commutator ↥⊤))
      (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G
have rw₃ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
  Eq (α := Subgroup G) (_root_.commutator G) ⊤
Tactic: rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
rw₁ : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₂ :
  Eq.{u_1 + 1} (α := Subgroup G) (map (G := ↥⊤) (Subgroup.subtype ⊤) (_root_.commutator ↥⊤))
      (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₃ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G
have rw₄ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
    (MonoidHom.range (G := ↥⊤) (Subgroup.subtype ⊤)) ↔
  Eq (α := Subgroup G) (_root_.commutator G) ⊤
Tactic: rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
rw₁ : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₂ :
  Eq.{u_1 + 1} (α := Subgroup G) (map (G := ↥⊤) (Subgroup.subtype ⊤) (_root_.commutator ↥⊤))
      (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₃ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₄ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
      (MonoidHom.range (G := ↥⊤) (Subgroup.subtype ⊤)) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G
have rw₅ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
Tactic: rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
rw₁ : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₂ :
  Eq.{u_1 + 1} (α := Subgroup G) (map (G := ↥⊤) (Subgroup.subtype ⊤) (_root_.commutator ↥⊤))
      (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₃ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₄ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
      (MonoidHom.range (G := ↥⊤) (Subgroup.subtype ⊤)) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₅ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤ ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G
have rw₆ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤ ↔
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤
Tactic: rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
f : G →* G'
hG : IsPerfect G
h_comm : IsMulCommutative G
⊢ Subsingleton G
have by_contra! : ∀ (h_not_subsingleton : Nontrivial G), False
Tactic: by_contra! h_not_subsingleton
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
inst_2 : IsPerfect.{u_1} ↥H
⊢ IsPerfect.{u_2} ↥(map f H)
have rw : ⁅map f H, map f H⁆ = map f H
Tactic: rw [isPerfect_iff, ← map_commutator, commutator_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
inst_2 : IsPerfect.{u_1} ↥H
rw : ⁅map f H, map f H⁆ = map f H
⊢ IsPerfect.{u_2} ↥(map f H)
have rw₁ : map f ⁅H, H⁆ = map f H
Tactic: rw [isPerfect_iff, ← map_commutator, commutator_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
inst_2 : IsPerfect.{u_1} ↥H
rw : ⁅map f H, map f H⁆ = map f H
rw₁ : map f ⁅H, H⁆ = map f H
⊢ IsPerfect.{u_2} ↥(map f H)
have rw₂ : map f H = map f H
Tactic: rw [isPerfect_iff, ← map_commutator, commutator_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : IsPerfect G
⊢ IsPerfect.{u_2} ↥f.range
have rw : IsPerfect.{u_2} ↥(map f ⊤)
Tactic: rw [MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.IsPerfect (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : IsPerfect G
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ IsPerfect G'
have rw : IsPerfect.{u_2} ↥f.range
Tactic: rw [← top_iff, ← MonoidHom.range_eq_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
hG : IsSimpleGroup G
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
Knorm : K.Normal
⊢ H.Normal
have step : ∀ (h_le : H ≤ ⊥) (hSubn : IsSubnormal.{u_1} (G := G) ⊥) (hN : Normal (G := ↥⊥) (H.subgroupOf ⊥))
  (Knorm : Normal.{u_1} (G := G) ⊥), H.Normal
Tactic: obtain rfl | rfl := Knorm.eq_bot_or_eq_top
Cleared hypotheses: K, h_le, hSubn, hN, Knorm
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
hG : IsSimpleGroup G
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
Knorm : K.Normal
step :
  ∀ (h_le : H ≤ ⊥) (hSubn : IsSubnormal.{u_1} (G := G) ⊥) (hN : Normal (G := ↥⊥) (H.subgroupOf ⊥))
    (Knorm : Normal.{u_1} (G := G) ⊥), H.Normal
⊢ H.Normal
have step₁ : ∀ (h_le : H ≤ ⊤) (hSubn : IsSubnormal.{u_1} (G := G) ⊤) (hN : Normal (G := ↥⊤) (H.subgroupOf ⊤))
  (Knorm : Normal.{u_1} (G := G) ⊤), H.Normal
Tactic: obtain rfl | rfl := Knorm.eq_bot_or_eq_top
Cleared hypotheses: K, h_le, hSubn, hN, Knorm
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : IsSimpleGroup G
hN : H.IsSubnormal
⊢ H.Normal
have top : Normal.{u_1} (G := G) ⊤
Tactic: induction hN with
  | top => simp
  | step H K h_le hSubn hN Knorm =>
    obtain rfl | rfl := Knorm.eq_bot_or_eq_top
    · grind
    · grind [!normal_subgroupOf_iff_le_normalizer_inf, inf_of_le_left, normalizer_eq_top_iff]
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : IsSimpleGroup G
hN : H.IsSubnormal
top : Normal.{u_1} (G := G) ⊤
⊢ H.Normal
have step : ∀ (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal) (Knorm : K.Normal), H.Normal
Tactic: induction hN with
  | top => simp
  | step H K h_le hSubn hN Knorm =>
    obtain rfl | rfl := Knorm.eq_bot_or_eq_top
    · grind
    · grind [!normal_subgroupOf_iff_le_normalizer_inf, inf_of_le_left, normalizer_eq_top_iff]
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K = ⊤ ∨ ∃ (K_1 : Subgroup G), K < K_1 ∧ K_1.IsSubnormal ∧ (K.subgroupOf K_1).Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step : ∀ (HK : H ≤ ⊤) (hS : IsSubnormal.{u_1} (G := G) ⊤) (hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)),
  H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Tactic: obtain rfl | ⟨K', HK', hS', hN'⟩ := ih
Cleared hypotheses: K, HK, hS, hN, ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K = ⊤ ∨ ∃ (K_1 : Subgroup G), K < K_1 ∧ K_1.IsSubnormal ∧ (K.subgroupOf K_1).Normal
step :
  ∀ (HK : H ≤ ⊤) (hS : IsSubnormal.{u_1} (G := G) ⊤) (hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)),
    H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step₁ : ∀ (K' : Subgroup G) (HK' : K < K') (hS' : K'.IsSubnormal) (hN' : (K.subgroupOf K').Normal),
  H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Tactic: obtain rfl | ⟨K', HK', hS', hN'⟩ := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H : Subgroup G
HK : H ≤ ⊤
hS : IsSubnormal.{u_1} (G := G) ⊤
hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step : ∀ (HK : LE.le.{u_1} (α := Subgroup G) ⊤ ⊤) (hN : Normal.{u_1} (G := ↥⊤) (subgroupOf ⊤ ⊤)),
  Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), ⊤ < K ∧ K.IsSubnormal ∧ (subgroupOf ⊤ K).Normal
Tactic: obtain rfl | hH := eq_or_ne H ⊤
Cleared hypotheses: H, HK, hN
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H : Subgroup G
HK : H ≤ ⊤
hS : IsSubnormal.{u_1} (G := G) ⊤
hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)
step :
  ∀ (HK : LE.le.{u_1} (α := Subgroup G) ⊤ ⊤) (hN : Normal.{u_1} (G := ↥⊤) (subgroupOf ⊤ ⊤)),
    Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), ⊤ < K ∧ K.IsSubnormal ∧ (subgroupOf ⊤ K).Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step₁ : ∀ (hH : H ≠ ⊤), H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Tactic: obtain rfl | hH := eq_or_ne H ⊤
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step : ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Tactic: right
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
⊢ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step : ∀ (HK : H ≤ H) (hS : H.IsSubnormal) (hN : (H.subgroupOf H).Normal) (HK' : H < K') (hN' : (H.subgroupOf K').Normal),
  ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Tactic: obtain rfl | hH := eq_or_ne H K
Cleared hypotheses: K, HK, hS, hN, HK', hN'
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
step :
  ∀ (HK : H ≤ H) (hS : H.IsSubnormal) (hN : (H.subgroupOf H).Normal) (HK' : H < K') (hN' : (H.subgroupOf K').Normal),
    ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step₁ : ∀ (hH : H ≠ K), ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Tactic: obtain rfl | hH := eq_or_ne H K
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K' : Subgroup G
hS' : K'.IsSubnormal
HK : H ≤ H
hS : H.IsSubnormal
hN : (H.subgroupOf H).Normal
HK' : H < K'
hN' : (H.subgroupOf K').Normal
w : Subgroup G
⊢ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have h : H < K' ∧ K'.IsSubnormal ∧ (H.subgroupOf K').Normal
Tactic: use K'
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.IsSubnormal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have top : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), ⊤ < K ∧ K.IsSubnormal ∧ (subgroupOf ⊤ K).Normal
Tactic: induction h with
    | top => simp
    | step H K HK hS hN ih =>
      obtain rfl | ⟨K', HK', hS', hN'⟩ := ih
      · obtain rfl | hH := eq_or_ne H ⊤
        · simp
        · exact Or.inr ⟨⊤, by simp [hH.lt_top , *]⟩
      right
      obtain rfl | hH := eq_or_ne H K
      · use K'
      · exact ⟨K, by simpa [*] using HK.lt_of_ne hH⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.IsSubnormal
top : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), ⊤ < K ∧ K.IsSubnormal ∧ (subgroupOf ⊤ K).Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
have step : ∀ (H K : Subgroup G) (HK : H ≤ K) (hS : K.IsSubnormal) (hN : (H.subgroupOf K).Normal)
  (ih : K = ⊤ ∨ ∃ (K_1 : Subgroup G), K < K_1 ∧ K_1.IsSubnormal ∧ (K.subgroupOf K_1).Normal),
  H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Tactic: induction h with
    | top => simp
    | step H K HK hS hN ih =>
      obtain rfl | ⟨K', HK', hS', hN'⟩ := ih
      · obtain rfl | hH := eq_or_ne H ⊤
        · simp
        · exact Or.inr ⟨⊤, by simp [hH.lt_top , *]⟩
      right
      obtain rfl | hH := eq_or_ne H K
      · use K'
      · exact ⟨K, by simpa [*] using HK.lt_of_ne hH⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ H.IsSubnormal
have inl : IsSubnormal.{u_1} (G := G) ⊤
Tactic: obtain rfl | ⟨K, HK, Ksn, h⟩ := h
Cleared hypotheses: H, h
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
inl : IsSubnormal.{u_1} (G := G) ⊤
⊢ H.IsSubnormal
have inr : ∀ (K : Subgroup G) (HK : H < K) (Ksn : K.IsSubnormal) (h : (H.subgroupOf K).Normal), H.IsSubnormal
Tactic: obtain rfl | ⟨K, HK, Ksn, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : ∀ (ne_top : K ≠ ⊤), ∃ (K_1 : Subgroup G), K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
have step : ∀ (h_le : H ≤ ⊤) (hSubn : IsSubnormal.{u_1} (G := G) ⊤) (hN : Normal (G := ↥⊤) (H.subgroupOf ⊤))
  (ih : ∀ (ne_top : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊤), ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤),
  ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
Tactic: obtain rfl | K_ne := eq_or_ne K ⊤
Cleared hypotheses: K, h_le, hSubn, hN, ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : ∀ (ne_top : K ≠ ⊤), ∃ (K_1 : Subgroup G), K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤
ne_top : H ≠ ⊤
step :
  ∀ (h_le : H ≤ ⊤) (hSubn : IsSubnormal.{u_1} (G := G) ⊤) (hN : Normal (G := ↥⊤) (H.subgroupOf ⊤))
    (ih : ∀ (ne_top : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊤), ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤),
    ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
have step₁ : ∀ (K_ne : K ≠ ⊤), ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
Tactic: obtain rfl | K_ne := eq_or_ne K ⊤
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H_1 H : Subgroup G
ne_top : H ≠ ⊤
h_le : H ≤ ⊤
hSubn : IsSubnormal.{u_1} (G := G) ⊤
hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)
ih : ∀ (ne_top : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊤), ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
have hN₁ : H.Normal
Tactic: rw [normal_subgroupOf_iff_le_normalizer h_le, top_le_iff, normalizer_eq_top_iff] at hN
Cleared hypotheses: hN, ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hN : H.IsSubnormal
ne_top : H ≠ ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
have top : ∀ (ne_top : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊤), ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
Tactic: induction hN with
  | top => contradiction
  | step H K h_le hSubn hN ih =>
    obtain rfl | K_ne := eq_or_ne K ⊤
    · rw [normal_subgroupOf_iff_le_normalizer h_le, top_le_iff, normalizer_eq_top_iff] at hN
      exact ⟨H, hN, le_rfl, ne_top.lt_top⟩
    · grind
Cleared hypotheses: hN, ne_top
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hN : H.IsSubnormal
ne_top : H ≠ ⊤
top : ∀ (ne_top : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊤), ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
have step : ∀ (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal)
  (ih : ∀ (ne_top : K ≠ ⊤), ∃ (K_1 : Subgroup G), K_1.Normal ∧ K ≤ K_1 ∧ K_1 < ⊤) (ne_top : H ≠ ⊤),
  ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
Tactic: induction hN with
  | top => contradiction
  | step H K h_le hSubn hN ih =>
    obtain rfl | K_ne := eq_or_ne K ⊤
    · rw [normal_subgroupOf_iff_le_normalizer h_le, top_le_iff, normalizer_eq_top_iff] at hN
      exact ⟨H, hN, le_rfl, ne_top.lt_top⟩
    · grind
Cleared hypotheses: hN, ne_top
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hN : H.IsSubnormal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
have inl : ∀ (hN : IsSubnormal.{u_1} (G := G) ⊤), Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
Tactic: obtain rfl | H_ne := eq_or_ne H ⊤
Cleared hypotheses: H, hN
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hN : H.IsSubnormal
inl :
  ∀ (hN : IsSubnormal.{u_1} (G := G) ⊤),
    Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
have inr : ∀ (H_ne : H ≠ ⊤), H = ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
Tactic: obtain rfl | H_ne := eq_or_ne H ⊤
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = ⊤ ∧ f n = ⊤
have left : Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦ ⊤
Tactic: use 0, fun _ ↦ ⊤, ?_, (by simp)
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih :
  ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = K ∧ f n = ⊤
⊢ ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤
have step : ∀ (n : ℕ) (f : ℕ → Subgroup G) (hf : Monotone f)
  (f0 : ∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) (fn : f 0 = K ∧ f n = ⊤),
  ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤
Tactic: obtain ⟨n, f, hf, f0, fn⟩ := ih
Cleared hypotheses: ih