awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
hg : Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer s) g
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) g
have this : (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
          AddAut G) :
      (a : G) → G) ''
    (↑(AddSubgroup.closure s) : Set G) =
  (↑(AddSubgroup.closure
        ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
                AddAut G) :
            (a : G) → G) ''
          s)) :
    Set G)
Tactic: have : AddAut.conj g '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj g '' s) :=
    congr($(AddAut.conj g |>.toAddMonoidHom.map_closure s))
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_5
inst : AddGroup G
s : Set G
g : G
hg : Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer s) g
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) g
have this₁ : (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g) :
          AddAut G) :
      (a : G) → G) ''
    (↑(AddSubgroup.closure s) : Set G) =
  (↑(AddSubgroup.closure s) : Set G)
Tactic: rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq.mp hg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s
have refine : ∀ (hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s) (h : G) (hh : h ∈ H) (k : G) (hk : h * k * h⁻¹ ∈ s), k ∈ s
Tactic: refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ H ≤ normalizer (↑K : Set G) ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
have refine : ∀ (hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K) (h : G) (hh : h ∈ H) (k : G) (hk : h * k * h⁻¹ ∈ (↑K : Set G)),
  k ∈ (↑K : Set G)
Tactic: refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
⊢ H ≤ normalizer (↑(closure s) : Set G) ↔ ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
have refine : ∀ (hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)) (h : G) (hh : h ∈ H),
  Membership.mem (γ := Subgroup G) (normalizer (↑(closure s) : Set G)) h
Tactic: refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(closure s) : Set G)) h
have this : (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
  (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
Tactic: have : MulAut.conj h '' (closure s) = closure (MulAut.conj h '' s) :=
    congr($(MulAut.conj h |>.toMonoidHom.map_closure s))
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ Membership.mem (γ := Subgroup G) (normalizer (↑(closure s) : Set G)) h
have rw : (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G) = (↑(closure s) : Set G)
Tactic: rw [mem_normalizer_iff_conj_image_eq, this]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G) =
    (↑(closure s) : Set G)
have apply : (↑(closure s) : Set G) ⊆ (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
Tactic: apply subset_antisymm <| by simpa using hH h hh
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := Subgroup G) (closure s) (h * g * h⁻¹)
h : G
hh : h ∈ H
this :
  (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G) =
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
⊢ (↑(closure s) : Set G) ⊆
    (↑(closure ((⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' s)) : Set G)
have rw : s ⊆ (⇑((MulAut.conj : (a : G) → MulAut G) h : MulAut G) : (a : G) → G) '' (↑(closure s) : Set G)
Tactic: rw [SetLike.coe_subset_coe, closure_le, ← this]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
⊢ H ≤ AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G) ↔
    ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
have refine : ∀ (hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)) (h : G)
  (hh : h ∈ H), Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) h
Tactic: refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| AddSubgroup.mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) h
have this : (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
          AddAut G) :
      (a : G) → G) ''
    (↑(AddSubgroup.closure s) : Set G) =
  (↑(AddSubgroup.closure
        ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                AddAut G) :
            (a : G) → G) ''
          s)) :
    Set G)
Tactic: have : AddAut.conj h '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj h '' s) :=
    congr($(AddAut.conj h |>.toAddMonoidHom.map_closure s))
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ Membership.mem (γ := AddSubgroup G) (AddSubgroup.normalizer (↑(AddSubgroup.closure s) : Set G)) h
have rw : (↑(AddSubgroup.closure
        ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                AddAut G) :
            (a : G) → G) ''
          s)) :
    Set G) =
  (↑(AddSubgroup.closure s) : Set G)
Tactic: rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq, this]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G) =
    (↑(AddSubgroup.closure s) : Set G)
have apply : (↑(AddSubgroup.closure s) : Set G) ⊆
  (↑(AddSubgroup.closure
        ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                AddAut G) :
            (a : G) → G) ''
          s)) :
    Set G)
Tactic: apply subset_antisymm <| by simpa using hH h hh
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_5
inst : AddGroup G
H : AddSubgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, Membership.mem (γ := AddSubgroup G) (AddSubgroup.closure s) (h + g + -h)
h : G
hh : h ∈ H
this :
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
            AddAut G) :
        (a : G) → G) ''
      (↑(AddSubgroup.closure s) : Set G) =
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
⊢ (↑(AddSubgroup.closure s) : Set G) ⊆
    (↑(AddSubgroup.closure
          ((⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G)
                    ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
                  AddAut G) :
              (a : G) → G) ''
            s)) :
      Set G)
have rw : s ⊆
  (⇑((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) h) :
          AddAut G) :
      (a : G) → G) ''
    (↑(AddSubgroup.closure s) : Set G)
Tactic: rw [SetLike.coe_subset_coe, AddSubgroup.closure_le, ← this]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
x : N
⊢ x ∈ comap f (normalizer (↑H : Set G)) → Membership.mem (γ := Subgroup N) (normalizer (↑(comap f H) : Set N)) x
have simp : (∀ (h : G),
    h ∈ H ↔ HMul.hMul (β := G) (HMul.hMul (α := G) ((f : (a : N) → G) x : G) h) (((f : (a : N) → G) x)⁻¹ : G) ∈ H) →
  ∀ (h : N),
    Membership.mem (α := G) H ((f : (a : N) → G) h : G) ↔
      Membership.mem (α := G) H ((f : (a : N) → G) (x * h * x⁻¹) : G)
Tactic: simp only [mem_normalizer_iff, mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : N
⊢ x ∈ map f (normalizer (↑H : Set G)) → Membership.mem (γ := Subgroup N) (normalizer (↑(map f H) : Set N)) x
have simp : ∀ (x_1 : G),
  (∀ (h : G), h ∈ H ↔ x_1 * h * x_1⁻¹ ∈ H) →
    (f : (a : G) → N) x_1 = x →
      ∀ (h : N), (∃ x ∈ H, (f : (a : G) → N) x = h) ↔ ∃ x_2 ∈ H, (f : (a : G) → N) x_2 = x * h * x⁻¹
Tactic: simp only [and_imp, mem_map, exists_imp, mem_normalizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x ∈ H, (f : (a : G) → N) x = n) ↔
    ∃ x_1 ∈ H,
      (f : (a : G) → N) x_1 =
        HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
have mp : (∃ x ∈ H, (f : (a : G) → N) x = n) →
  ∃ x_1 ∈ H,
    (f : (a : G) → N) x_1 =
      HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
mp :
  (∃ x ∈ H, (f : (a : G) → N) x = n) →
    ∃ x_1 ∈ H,
      (f : (a : G) → N) x_1 =
        HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
⊢ (∃ x ∈ H, (f : (a : G) → N) x = n) ↔
    ∃ x_1 ∈ H,
      (f : (a : G) → N) x_1 =
        HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
have mpr : (∃ x_1 ∈ H,
    (f : (a : G) → N) x_1 =
      HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)) →
  ∃ x ∈ H, (f : (a : G) → N) x = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ ∃ x_1 ∈ H,
    (f : (a : G) → N) x_1 =
      HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : G) → N) x : N) ((f : (a : G) → N) y : N))
        (((f : (a : G) → N) x)⁻¹ : N)
have right : (f : (a : G) → N) (x * y * x⁻¹) =
  HMul.hMul (β := N) (HMul.hMul (α := N) (β := N) ((f : (a : G) → N) x : N) ((f : (a : G) → N) y : N))
    (((f : (a : G) → N) x)⁻¹ : N)
Tactic: use x * y * x⁻¹, (hx y).1 hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy :
  (f : (a : G) → N) y =
    HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
⊢ ∃ x ∈ H, (f : (a : G) → N) x = n
have h : x⁻¹ * y * x ∈ H ∧ (f : (a : G) → N) (x⁻¹ * y * x) = n
Tactic: use x⁻¹ * y * x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy :
  (f : (a : G) → N) y =
    HMul.hMul (β := N) (HMul.hMul (α := N) ((f : (a : G) → N) x : N) n) (((f : (a : G) → N) x)⁻¹ : N)
⊢ x⁻¹ * y * x ∈ H ∧ (f : (a : G) → N) (x⁻¹ * y * x) = n
have h : x * (x⁻¹ * y * x) * x⁻¹ ∈ H ∧ (f : (a : G) → N) (x⁻¹ * y * x) = n
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
h : H ≤ f.range
⊢ comap f (normalizer (↑H : Set G)) = normalizer (↑(comap f H) : Set N)
have apply : normalizer (↑(comap f H) : Set N) ≤ comap f (normalizer (↑H : Set G))
Tactic: apply le_antisymm (le_normalizer_comap f)
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
h : H ≤ f.range
⊢ normalizer (↑(comap f H) : Set N) ≤ comap f (normalizer (↑H : Set G))
have rw : map f (normalizer (↑(comap f H) : Set N)) ≤ normalizer (↑H : Set G)
Tactic: rw [← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
h : H ≤ f.range
⊢ map f (normalizer (↑(comap f H) : Set N)) ≤ normalizer (↑H : Set G)
have apply : LE.le (α := Subgroup G) (normalizer (↑(map f (comap f H)) : Set G)) (normalizer (↑H : Set G))
Tactic: apply (le_normalizer_map f).trans
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
N : Type u_5
inst_1 : Group N
f : N →* G
h : H ≤ f.range
⊢ LE.le (α := Subgroup G) (normalizer (↑(map f (comap f H)) : Set G)) (normalizer (↑H : Set G))
have rw : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑H : Set G))
Tactic: rw [map_comap_eq_self h]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer (↑H : Set G)
have rw : (H.subgroupOf K).Normal ↔ subgroupOf (normalizer (↑H : Set G)) K = ⊤
Tactic: rw [← subgroupOf_eq_top, subgroupOf_normalizer_eq h, normalizer_eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
rw : (H.subgroupOf K).Normal ↔ subgroupOf (normalizer (↑H : Set G)) K = ⊤
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer (↑H : Set G)
have rw₁ : (H.subgroupOf K).Normal ↔ Eq (α := Subgroup ↥K) (normalizer (↑(H.subgroupOf K) : Set ↥K)) ⊤
Tactic: rw [← subgroupOf_eq_top, subgroupOf_normalizer_eq h, normalizer_eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : H ≤ K
rw : (H.subgroupOf K).Normal ↔ subgroupOf (normalizer (↑H : Set G)) K = ⊤
rw₁ : (H.subgroupOf K).Normal ↔ Eq (α := Subgroup ↥K) (normalizer (↑(H.subgroupOf K) : Set ↥K)) ⊤
⊢ (H.subgroupOf K).Normal ↔ K ≤ normalizer (↑H : Set G)
have rw₂ : (H.subgroupOf K).Normal ↔ (H.subgroupOf K).Normal
Tactic: rw [← subgroupOf_eq_top, subgroupOf_normalizer_eq h, normalizer_eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
⊢ NormalizerCondition G ↔ ∀ (H : Subgroup G), normalizer (↑H : Set G) = H → H = ⊤
have h : ∀ (a : Subgroup G), a < ⊤ → a < normalizer (↑a : Set G) ↔ normalizer (↑a : Set G) = a → a = ⊤
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H < ⊤ → H < normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h : H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
Tactic: simp only [lt_iff_le_and_ne, le_normalizer, Ne]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h : (H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G)) → normalizer (↑H : Set G) = 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 ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₁ : (normalizer (↑H : Set G) = H → H = ⊤) → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬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 = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₂ : ¬(H ≤ ⊤ ∧ ¬H = ⊤) → normalizer (↑H : Set G) = 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 ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₃ : True → ¬H = normalizer (↑H : Set G) → normalizer (↑H : Set G) = 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 ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₈ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬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 = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₉ : H = ⊤ → H ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬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 ≤ ⊤ ∧ ¬H = ⊤ → True ∧ ¬H = normalizer (↑H : Set G) ↔ normalizer (↑H : Set G) = H → H = ⊤
have h₁₂ : ¬normalizer (↑H : Set G) = H → H ≤ ⊤ ∧ ¬H = ⊤ → ¬H = normalizer (↑H : Set G)
Tactic: tauto