awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 = ⊤
have right : (match (motive := ℕ → Subgroup G) 0 with
    | 0 => H
    | n.succ => f n) =
    H ∧
  Eq.{u_1 + 1} (α := Subgroup G)
    (match (motive := ℕ → Subgroup G) n + 1 with
      | 0 => H
      | n.succ => f n :
      Subgroup G)
    (⊤ : Subgroup G)
Tactic: use n + 1, fun | 0 => H | n + 1 => f n, ?_, ?_
-- 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
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 = ⊤
right :
  (match (motive := ℕ → Subgroup G) 0 with
      | 0 => H
      | n.succ => f n) =
      H ∧
    Eq.{u_1 + 1} (α := Subgroup G)
      (match (motive := ℕ → Subgroup G) n + 1 with
        | 0 => H
        | n.succ => f n :
        Subgroup G)
      (⊤ : Subgroup G)
⊢ ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤
have left : Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦
  match (motive := ℕ → Subgroup G) x with
  | 0 => H
  | n.succ => f n
Tactic: use n + 1, fun | 0 => H | n + 1 => f n, ?_, ?_
-- 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
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 = ⊤
right :
  (match (motive := ℕ → Subgroup G) 0 with
      | 0 => H
      | n.succ => f n) =
      H ∧
    Eq.{u_1 + 1} (α := Subgroup G)
      (match (motive := ℕ → Subgroup G) n + 1 with
        | 0 => H
        | n.succ => f n :
        Subgroup G)
      (⊤ : Subgroup G)
left :
  Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦
    match (motive := ℕ → Subgroup G) x with
    | 0 => H
    | n.succ => 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 left₁ : ∀ (i : ℕ),
  Normal.{u_1} (G :=
    ↥(match (motive := ℕ → Subgroup G) i + 1 with
        | 0 => H
        | n.succ => f n :
        Subgroup G))
    (subgroupOf
      (match (motive := ℕ → Subgroup G) i with
      | 0 => H
      | n.succ => f n)
      (match (motive := ℕ → Subgroup G) i + 1 with
      | 0 => H
      | n.succ => f n))
Tactic: use n + 1, fun | 0 => H | n + 1 => f n, ?_, ?_
-- 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
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 = ⊤
⊢ Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦
    match (motive := ℕ → Subgroup G) x with
    | 0 => H
    | n.succ => f n
have left : ∀ (n : ℕ),
  LE.le.{u_1} (α := Subgroup G)
    (match (motive := ℕ → Subgroup G) n with
      | 0 => H
      | n.succ => f n :
      Subgroup G)
    (match (motive := ℕ → Subgroup G) n + 1 with
      | 0 => H
      | n.succ => f n :
      Subgroup G)
Tactic: refine monotone_nat_of_le_succ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : H.IsSubnormal
⊢ ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤
have top : ∃ (n : ℕ) (f : ℕ → Subgroup G),
  Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = ⊤ ∧ f n = ⊤
Tactic: induction h with
    | top =>
      use 0, fun _ ↦ ⊤, ?_, (by simp)
      exact monotone_nat_of_le_succ fun _ ↦ le_top
    | step H K h_le hSubn hN ih =>
      obtain ⟨n, f, hf, f0, fn⟩ := ih
      use n + 1, fun | 0 => H | n + 1 => f n, ?_, ?_
      · grind
      · refine monotone_nat_of_le_succ ?_
        grind only [monotone_iff_forall_lt]
      · simp +instances only
        grind
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 :
  ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = ⊤ ∧ 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 : ∀ (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 = ⊤
Tactic: induction h with
    | top =>
      use 0, fun _ ↦ ⊤, ?_, (by simp)
      exact monotone_nat_of_le_succ fun _ ↦ le_top
    | step H K h_le hSubn hN ih =>
      obtain ⟨n, f, hf, f0, fn⟩ := ih
      use n + 1, fun | 0 => H | n + 1 => f n, ?_, ?_
      · grind
      · refine monotone_nat_of_le_succ ?_
        grind only [monotone_iff_forall_lt]
      · simp +instances only
        grind
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
n : ℕ
hyps :
  ∃ (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤
⊢ H.IsSubnormal
have revert : ∀ {H : Subgroup G}
  (hyps :
    ∃ (f : ℕ → Subgroup G),
      Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤),
  H.IsSubnormal
Tactic: revert H
Cleared hypotheses: H, hyps
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  ∀ {H : Subgroup G}
    (hyps :
      ∃ (f : ℕ → Subgroup G),
        Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤),
    H.IsSubnormal
F : ℕ → Subgroup G
hF : Monotone F
H_le : ∀ (i : ℕ), Normal (G := ↥(F (i + 1))) ((F i).subgroupOf (F (i + 1)))
ih1 : F (n + 1) = ⊤
⊢ (F 0).IsSubnormal
have succ : (F (HAdd.hAdd (α := ℕ) 0 1)).IsSubnormal
Tactic: refine step _ _ (hF <| Nat.le_add_right 0 1) ?_ (H_le _)
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih :
  ∀ {H : Subgroup G}
    (hyps :
      ∃ (f : ℕ → Subgroup G),
        Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤),
    H.IsSubnormal
F : ℕ → Subgroup G
hF : Monotone F
H_le : ∀ (i : ℕ), Normal (G := ↥(F (i + 1))) ((F i).subgroupOf (F (i + 1)))
ih1 : F (n + 1) = ⊤
⊢ (F (HAdd.hAdd (α := ℕ) 0 1)).IsSubnormal
have succ : (Monotone.{0, u_1} (β := Subgroup G) fun (n : ℕ) ↦ F (n + 1)) ∧
  (∀ (i : ℕ),
      Normal.{u_1} (G := ↥((fun (n : ℕ) ↦ F (n + 1)) (i + 1)))
        (subgroupOf ((fun (n : ℕ) ↦ F (n + 1)) i) ((fun (n : ℕ) ↦ F (n + 1)) (i + 1)))) ∧
    (fun (n : ℕ) ↦ F (n + 1)) 0 = F (HAdd.hAdd (α := ℕ) 0 1) ∧
      Eq.{u_1 + 1} (α := Subgroup G) ((fun (n : ℕ) ↦ F (n + 1)) n) ⊤
Tactic: refine ih ⟨fun n ↦ F (n + 1), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
⊢ ∀ {H : Subgroup G}
    (hyps :
      ∃ (f : ℕ → Subgroup G),
        Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤),
    H.IsSubnormal
have zero : ∀ {H : Subgroup G}
  (hyps :
    ∃ (f : ℕ → Subgroup G),
      Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f 0 = ⊤),
  H.IsSubnormal
Tactic: induction n with
    | zero => simp_all
    | succ n ih =>
      rintro J ⟨F, hF, H_le, rfl, ih1⟩
      refine step _ _ (hF <| Nat.le_add_right 0 1) ?_ (H_le _)
      refine ih ⟨fun n ↦ F (n + 1), ?_⟩
      grind only [Monotone, monotone_iff_forall_lt]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
zero :
  ∀ {H : Subgroup G}
    (hyps :
      ∃ (f : ℕ → Subgroup G),
        Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f 0 = ⊤),
    H.IsSubnormal
⊢ ∀ {H : Subgroup G}
    (hyps :
      ∃ (f : ℕ → Subgroup G),
        Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤),
    H.IsSubnormal
have succ : ∀ (n : ℕ)
  (ih :
    ∀ {H : Subgroup G}
      (hyps :
        ∃ (f : ℕ → Subgroup G),
          Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤),
      H.IsSubnormal)
  {H : Subgroup G}
  (hyps :
    ∃ (f : ℕ → Subgroup G),
      Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f (n + 1) = ⊤),
  H.IsSubnormal
Tactic: induction n with
    | zero => simp_all
    | succ n ih =>
      rintro J ⟨F, hF, H_le, rfl, ih1⟩
      refine step _ _ (hF <| Nat.le_add_right 0 1) ?_ (H_le _)
      refine ih ⟨fun n ↦ F (n + 1), ?_⟩
      grind only [Monotone, monotone_iff_forall_lt]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
⊢ (map K.subtype ⊤).IsSubnormal
have top : K.subtype.range.IsSubnormal
Tactic: rwa [← MonoidHom.range_eq_map, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : (A.subgroupOf B).Normal
ih : (map K.subtype B).IsSubnormal
⊢ (map K.subtype A).IsSubnormal
have step : Normal (G := ↥(map K.subtype B)) ((map K.subtype A).subgroupOf (map K.subtype B))
Tactic: refine step (A.map K.subtype) (B.map K.subtype) (map_mono h_le) ih ?_
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : (A.subgroupOf B).Normal
ih : (map K.subtype B).IsSubnormal
⊢ Normal (G := ↥(map K.subtype B)) ((map K.subtype A).subgroupOf (map K.subtype B))
have hN₁ : B ≤ normalizer (↑A : Set ↥K)
Tactic: rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
Cleared hypotheses: hN, ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : B ≤ normalizer (↑A : Set ↥K)
ih : (map K.subtype B).IsSubnormal
⊢ Normal (G := ↥(map K.subtype B)) ((map K.subtype A).subgroupOf (map K.subtype B))
have step : map K.subtype B ≤ normalizer (↑(map K.subtype A) : Set G)
Tactic: rw [normal_subgroupOf_iff_le_normalizer (map_mono h_le)]
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Hsn : H.IsSubnormal
Ksn : K.IsSubnormal
⊢ (map K.subtype H).IsSubnormal
have top : (map K.subtype ⊤).IsSubnormal
Tactic: induction Hsn with
  | top =>
    rwa [← MonoidHom.range_eq_map, range_subtype]
  | step A B h_le hSubn hN ih =>
    refine step (A.map K.subtype) (B.map K.subtype) (map_mono h_le) ih ?_
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (map_mono h_le)]
    exact le_trans (map_mono hN) (le_normalizer_map _)
Cleared hypotheses: Hsn
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Hsn : H.IsSubnormal
Ksn : K.IsSubnormal
top : (map K.subtype ⊤).IsSubnormal
⊢ (map K.subtype H).IsSubnormal
have step : ∀ (A B : Subgroup ↥K) (h_le : A ≤ B) (hSubn : B.IsSubnormal) (hN : (A.subgroupOf B).Normal)
  (ih : (map K.subtype B).IsSubnormal), (map K.subtype A).IsSubnormal
Tactic: induction Hsn with
  | top =>
    rwa [← MonoidHom.range_eq_map, range_subtype]
  | step A B h_le hSubn hN ih =>
    refine step (A.map K.subtype) (B.map K.subtype) (map_mono h_le) ih ?_
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (map_mono h_le)]
    exact le_trans (map_mono hN) (le_normalizer_map _)
Cleared hypotheses: Hsn
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
HK : H ≤ K
Hsn : (H.subgroupOf K).IsSubnormal
Ksn : K.IsSubnormal
⊢ H.IsSubnormal
have key : (map K.subtype (H.subgroupOf K)).IsSubnormal
Tactic: have key := Hsn.trans' Ksn
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
HK : H ≤ K
Hsn : (H.subgroupOf K).IsSubnormal
Ksn : K.IsSubnormal
key : (map K.subtype (H.subgroupOf K)).IsSubnormal
⊢ H.IsSubnormal
have rwa : ∀ (key : H.IsSubnormal), H.IsSubnormal
Tactic: rwa [map_subgroupOf_eq_of_le HK] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ (map f ⊤).IsSubnormal
have top : IsSubnormal.{u_2} (G := G') ⊤
Tactic: rw [map_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
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (map f K).IsSubnormal
⊢ (map f H).IsSubnormal
have step : Normal (G := ↥(map f K)) ((map f H).subgroupOf (map f K))
Tactic: apply step _ (map f K) (map_mono h_le) ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (map f K).IsSubnormal
⊢ Normal (G := ↥(map f K)) ((map f H).subgroupOf (map f K))
have hN₁ : K ≤ normalizer (↑H : Set G)
Tactic: rw [normal_subgroupOf_iff_le_normalizer h_le] 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
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
hS : H.IsSubnormal
⊢ (map f H).IsSubnormal
have top : (map f ⊤).IsSubnormal
Tactic: induction hS with
  | top =>
    rw [map_top_of_surjective f hf]
    apply top
  | step H K h_le hSubn hN ih =>
    apply step _ (map f K) (map_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    exact normal_subgroupOf_of_le_normalizer ((map_mono hN).trans (H.le_normalizer_map f))
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
G' : Type u_2
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
hS : H.IsSubnormal
top : (map f ⊤).IsSubnormal
⊢ (map f H).IsSubnormal
have step : ∀ (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal) (ih : (map f K).IsSubnormal),
  (map f H).IsSubnormal
Tactic: induction hS with
  | top =>
    rw [map_top_of_surjective f hf]
    apply top
  | step H K h_le hSubn hN ih =>
    apply step _ (map f K) (map_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    exact normal_subgroupOf_of_le_normalizer ((map_mono hN).trans (H.le_normalizer_map f))
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (comap f K).IsSubnormal
⊢ (comap f H).IsSubnormal
have step : Normal (G := ↥(comap f K)) ((comap f H).subgroupOf (comap f K))
Tactic: apply step _ (comap f K) (comap_mono h_le) ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (hypothesis)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (comap f K).IsSubnormal
⊢ Normal (G := ↥(comap f K)) ((comap f H).subgroupOf (comap f K))
have hN₁ : K ≤ normalizer (↑H : Set G')
Tactic: rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
Cleared hypotheses: hN, ih
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer (↑H : Set G')
ih : (comap f K).IsSubnormal
⊢ Normal (G := ↥(comap f K)) ((comap f H).subgroupOf (comap f K))
have step : comap f K ≤ normalizer (↑(comap f H) : Set G)
Tactic: rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
h : H'.IsSubnormal
⊢ (comap f H').IsSubnormal
have top : (comap f ⊤).IsSubnormal
Tactic: induction h with
  | top => simp
  | step H K h_le hSubn hN ih =>
    apply step _ (comap f K) (comap_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]
    exact (comap_mono hN).trans (le_normalizer_comap f)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.IsSubnormal (goal)
Goal:
G : Type u_1
inst : Group G
G' : Type u_2
inst_1 : Group G'
H' : Subgroup G'
f : G →* G'
h : H'.IsSubnormal
top : (comap f ⊤).IsSubnormal
⊢ (comap f H').IsSubnormal
have step : ∀ (H K : Subgroup G') (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal)
  (ih : (comap f K).IsSubnormal), (comap f H).IsSubnormal
Tactic: induction h with
  | top => simp
  | step H K h_le hSubn hN ih =>
    apply step _ (comap f K) (comap_mono h_le) ih
    rw [normal_subgroupOf_iff_le_normalizer h_le] at hN
    rw [normal_subgroupOf_iff_le_normalizer (comap_mono h_le)]
    exact (comap_mono hN).trans (le_normalizer_comap f)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg_1 : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
y : ↥(powers x)
⊢ IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
have obtain : ∀ (n : ℕ) (hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : M)), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
Tactic: obtain ⟨n, hn⟩ := y.2
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg_1 : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
hg : IsUnit.{u_3} (M := P) ((g : (a : M) → P) x : P)
y : ↥(powers x)
n : ℕ
hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : M)
⊢ IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
have rw : IsUnit (HPow.hPow (α := P) ((g : (a : M) → P) x : P) n)
Tactic: rw [← hn, g.map_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
y : M
G : AwayMap (x * y) P
⊢ HMul.hMul (α := P) ((G : (a : M) → P) x : P)
      (mk' G y (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers (x * y)) x_1) (x * y) ⋯)) =
    1
have rw : mk' G (x * y) (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers (x * y)) x_1) (x * y) sorry) = 1
Tactic: rw [mul_mk'_eq_mk'_of_mul, mk'_self]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
g : M →* P
hg : ∀ (y : ↥S), IsUnit.{u_3} (M := P) ((g : (a : M) → P) (↑y : M) : P)
x : M
F : AwayMap x N
y : M
G : AwayMap (x * y) P
rw :
  mk' G (x * y) (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers (x * y)) x_1) (x * y) ⋯) = 1
⊢ HMul.hMul (α := P) ((G : (a : M) → P) x : P)
      (mk' G y (Subtype.mk (p := fun (x_1 : M) ↦ Membership.mem (γ := Submonoid M) (powers (x * y)) x_1) (x * y) ⋯)) =
    1
have rw₁ : Eq.{u_3 + 1} (α := P) 1 1
Tactic: rw [mul_mk'_eq_mk'_of_mul, mk'_self]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
⊢ IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (↑y : A) : C)
have obtain : ∀ (n : ℕ) (hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)), IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (↑y : A) : C)
Tactic: obtain ⟨n, hn⟩ := y.2
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
n : ℕ
hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)
⊢ IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (↑y : A) : C)
have rw : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) ((fun (i : ℕ) ↦ i • x) n) : C)
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
hg : IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) x : C)
y : ↥(multiples x)
n : ℕ
hn : (fun (i : ℕ) ↦ i • x) n = (↑y : A)
⊢ IsAddUnit.{u_6} (M := C) ((g : (a : A) → C) (n • x) : C)
have rw : IsAddUnit (HSMul.hSMul (β := C) n ((g : (a : A) → C) x : C))
Tactic: rw [g.map_nsmul]
-- Lean 4 proof step from Mathlib.GroupTheory.MonoidLocalization.Away (goal)
Goal:
M : Type u_1
inst : CommMonoid M
S : Submonoid M
N : Type u_2
inst_1 : CommMonoid N
P : Type u_3
inst_2 : CommMonoid P
A : Type u_4
inst_3 : AddCommMonoid A
x : A
B : Type u_5
inst_4 : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst_5 : AddCommMonoid C
g : A →+ C
y : A
G : AwayMap (x + y) C
⊢ HAdd.hAdd (α := C) ((G : (a : A) → C) x : C)
      (mk' G y
        (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := AddSubmonoid A) (multiples (x + y)) x_1) (x + y) ⋯)) =
    0
have rw : mk' G (x + y)
    (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := AddSubmonoid A) (multiples (x + y)) x_1) (x + y) sorry) =
  0
Tactic: rw [add_mk'_eq_mk'_of_add, mk'_self]