awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.IsSubnormal
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
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
⊢ 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⟩

Premises used: Subgroup.IsSubnormal.step, eq_or_ne, Subgroup.IsSubnormal.top, Top.top, Or.inr, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
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) ⊤
inr : ∀ (K : Subgroup G) (HK : H < K) (Ksn : K.IsSubnormal) (h : (H.subgroupOf K).Normal), H.IsSubnormal
⊢ H.IsSubnormal

Tactic:
obtain rfl | ⟨K, HK, Ksn, h⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
⊢ IsSubnormal.{u_1} (G := G) ⊤

Tactic:
top

Premises used: Subgroup.IsSubnormal.top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
⊢ IsSubnormal.{u_1} (G := G) ⊤

Tactic:
exact top

Premises used: Subgroup.IsSubnormal.top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal

Tactic:
step _ _ HK.le Ksn h

Premises used: LT.lt.le, Subgroup.IsSubnormal.step
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
HK : H < K
Ksn : K.IsSubnormal
h : (H.subgroupOf K).Normal
⊢ H.IsSubnormal

Tactic:
exact step _ _ HK.le Ksn h

Premises used: LT.lt.le, Subgroup.IsSubnormal.step
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
ne_top : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.IsSubnormal
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 < ⊤
step₁ : ∀ (K_ne : K ≠ ⊤), ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
obtain rfl | K_ne := eq_or_ne K ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
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 < ⊤
⊢ H.Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le, top_le_iff, normalizer_eq_top_iff] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer, Subgroup.normalizer_eq_top_iff, top_le_iff
-- Module: Mathlib.GroupTheory.IsSubnormal
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 < ⊤
hN₁ : H.Normal
⊢ ∀ (ne_top : Ne.{u_1 + 1} (α := Subgroup G) ⊤ ⊤), ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le, top_le_iff, normalizer_eq_top_iff] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer, Subgroup.normalizer_eq_top_iff, top_le_iff
-- Module: Mathlib.GroupTheory.IsSubnormal
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 : H.Normal
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:
⟨H, hN, le_rfl, ne_top.lt_top⟩

Premises used: le_rfl, Ne.lt_top, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.IsSubnormal
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 : H.Normal
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:
exact ⟨H, hN, le_rfl, ne_top.lt_top⟩
-- Module: Mathlib.GroupTheory.IsSubnormal
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_ne : K ≠ ⊤
⊢ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
grind
-- Module: Mathlib.GroupTheory.IsSubnormal
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 < ⊤
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 < ⊤
⊢ ∃ (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

Premises used: Subgroup.IsSubnormal.step, Subgroup.normalizer_eq_top_iff, top_le_iff, Subgroup.IsSubnormal.top, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
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 < ⊤
inr : ∀ (H_ne : H ≠ ⊤), H = ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
obtain rfl | H_ne := eq_or_ne H ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
hN : IsSubnormal.{u_1} (G := G) ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

Tactic:
simp
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
grind only [iff_eq_top_or_exists, exists_normal_and_le_and_lt_top_of_ne]

Premises used: Subgroup.IsSubnormal.iff_eq_top_or_exists, Subgroup.IsSubnormal.exists_normal_and_le_and_lt_top_of_ne
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ ∀ (i : ℕ), Normal.{u_1} (G := ↥⊤) (subgroupOf ⊤ ⊤)

Tactic:
simp
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
left : Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦ ⊤
⊢ ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = ⊤ ∧ f n = ⊤

Tactic:
use 0, fun _ ↦ ⊤, ?_, (by simp)

Premises used: Top.top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦ ⊤

Tactic:
monotone_nat_of_le_succ fun _ ↦ le_top

Premises used: le_top, monotone_nat_of_le_succ
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦ ⊤

Tactic:
exact monotone_nat_of_le_succ fun _ ↦ le_top

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.GroupTheory.IsSubnormal
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 = ⊤
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 = ⊤
⊢ ∃ (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
-- Module: Mathlib.GroupTheory.IsSubnormal
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
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))
⊢ ∃ (n : ℕ) (f : ℕ → Subgroup G),
    Monotone f ∧ (∀ (i : ℕ), Normal (G := ↥(f (i + 1))) ((f i).subgroupOf (f (i + 1)))) ∧ f 0 = H ∧ f n = ⊤

Tactic:
use n + 1, fun | 0 => H | n + 1 => f n, ?_, ?_
-- Module: Mathlib.GroupTheory.IsSubnormal
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 = ⊤
⊢ (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:
grind
-- Module: Mathlib.GroupTheory.IsSubnormal
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

Tactic:
monotone_nat_of_le_succ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.GroupTheory.IsSubnormal
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 = ⊤
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)
⊢ Monotone.{0, u_1} (β := Subgroup G) fun (x : ℕ) ↦
    match (motive := ℕ → Subgroup G) x with
    | 0 => H
    | n.succ => f n

Tactic:
refine monotone_nat_of_le_succ ?_

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.GroupTheory.IsSubnormal
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 : ℕ),
    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:
grind only [monotone_iff_forall_lt]

Premises used: monotone_iff_forall_lt
-- Module: Mathlib.GroupTheory.IsSubnormal
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 = ⊤
left :
  ∀ (i : ℕ),
    (subgroupOf
        (match (motive := ℕ → Subgroup G) i with
        | 0 => H
        | n.succ => f n)
        (f i)).Normal
⊢ ∀ (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:
simp +instances only
-- Module: Mathlib.GroupTheory.IsSubnormal
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 = ⊤
⊢ ∀ (i : ℕ),
    (subgroupOf
        (match (motive := ℕ → Subgroup G) i with
        | 0 => H
        | n.succ => f n)
        (f i)).Normal

Tactic:
grind
-- Module: Mathlib.GroupTheory.IsSubnormal
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 = ⊤
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 = ⊤
⊢ ∃ (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

Premises used: Subgroup.IsSubnormal.step, monotone_iff_forall_lt, Subgroup.IsSubnormal.top, Top.top, monotone_nat_of_le_succ
-- Module: Mathlib.GroupTheory.IsSubnormal
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 = ⊤
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
⊢ H.IsSubnormal

Tactic:
revert H
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
⊢ ∀ {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:
simp_all
-- Module: Mathlib.GroupTheory.IsSubnormal
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

Tactic:
step _ _ (hF <| Nat.le_add_right 0 1) ?_ (H_le _)

Premises used: Nat.le_add_right, Subgroup.IsSubnormal.step, OfNat.ofNat
-- Module: Mathlib.GroupTheory.IsSubnormal
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) = ⊤
succ : (F (HAdd.hAdd (α := ℕ) 0 1)).IsSubnormal
⊢ (F 0).IsSubnormal

Tactic:
refine step _ _ (hF <| Nat.le_add_right 0 1) ?_ (H_le _)

Premises used: Nat.le_add_right, Subgroup.IsSubnormal.step, OfNat.ofNat
-- Module: Mathlib.GroupTheory.IsSubnormal
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

Tactic:
ih ⟨fun n ↦ F (n + 1), ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.IsSubnormal
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) = ⊤
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) ⊤
⊢ (F (HAdd.hAdd (α := ℕ) 0 1)).IsSubnormal

Tactic:
refine ih ⟨fun n ↦ F (n + 1), ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.IsSubnormal
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) = ⊤
⊢ (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:
grind only [Monotone, monotone_iff_forall_lt]

Premises used: Monotone, monotone_iff_forall_lt
-- Module: Mathlib.GroupTheory.IsSubnormal
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
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
⊢ ∀ {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:
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]

Premises used: Monotone, monotone_iff_forall_lt, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
top : K.subtype.range.IsSubnormal
top₁ top₂ top₃ top₄ : K.IsSubnormal
⊢ (map K.subtype ⊤).IsSubnormal

Tactic:
rwa [← MonoidHom.range_eq_map, range_subtype]

Premises used: MonoidHom.range_eq_map, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.IsSubnormal
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

Tactic:
step (A.map K.subtype) (B.map K.subtype) (map_mono h_le) ih ?_

Premises used: Subgroup.map, Subgroup.subtype, Subgroup.IsSubnormal.step, Subgroup.map_mono
-- Module: Mathlib.GroupTheory.IsSubnormal
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
step : Normal (G := ↥(map K.subtype B)) ((map K.subtype A).subgroupOf (map K.subtype B))
⊢ (map K.subtype A).IsSubnormal

Tactic:
refine step (A.map K.subtype) (B.map K.subtype) (map_mono h_le) ih ?_

Premises used: Subgroup.map, Subgroup.subtype, Subgroup.IsSubnormal.step, Subgroup.map_mono
-- Module: Mathlib.GroupTheory.IsSubnormal
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
⊢ B ≤ normalizer (↑A : Set ↥K)

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.GroupTheory.IsSubnormal
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
hN₁ : B ≤ normalizer (↑A : Set ↥K)
⊢ (map K.subtype B).IsSubnormal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer
-- Module: Mathlib.GroupTheory.IsSubnormal
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
step : map K.subtype B ≤ normalizer (↑(map K.subtype A) : Set G)
⊢ Normal (G := ↥(map K.subtype B)) ((map K.subtype A).subgroupOf (map K.subtype B))

Tactic:
rw [normal_subgroupOf_iff_le_normalizer (map_mono h_le)]

Premises used: Subgroup.normal_subgroupOf_iff_le_normalizer, Subgroup.map_mono
-- Module: Mathlib.GroupTheory.IsSubnormal
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
⊢ map K.subtype B ≤ normalizer (↑(map K.subtype A) : Set G)

Tactic:
le_trans (map_mono hN) (le_normalizer_map _)

Premises used: Subgroup.map_mono, Subgroup.le_normalizer_map, le_trans