awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
rwa : ∀ (hf : H ⊔ f.ker = comap f (map f K)), H = K
rwa₁ : ∀ (hf : H ⊔ f.ker = K ⊔ f.ker), H = K
⊢ H = K
have rwa₂ : ∀ (hf : H = K ⊔ f.ker), H = K
Tactic: rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup G
hH : f.ker ≤ H
hK : f.ker ≤ K
hf : comap f (map f H) = comap f (map f K)
rwa : ∀ (hf : H ⊔ f.ker = comap f (map f K)), H = K
rwa₁ : ∀ (hf : H ⊔ f.ker = K ⊔ f.ker), H = K
rwa₂ : ∀ (hf : H = K ⊔ f.ker), H = K
⊢ H = K
have rwa₃ : ∀ (hf : H = K), H = K
Tactic: rwa [comap_map_eq, comap_map_eq, sup_of_le_left hH, sup_of_le_left hK] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
have rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
Tactic: rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
have rw₁ : map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
Tactic: rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
rw₁ : map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
have rw₂ : f.range ⊓ H ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
Tactic: rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
rw₁ : map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₂ : f.range ⊓ H ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
have rw₃ : f.range ⊓ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
Tactic: rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
rw₁ : map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₂ : f.range ⊓ H ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₃ : f.range ⊓ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
have rw₄ : H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
Tactic: rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
rw₁ : map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₂ : f.range ⊓ H ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₃ : f.range ⊓ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
rw₄ : H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
have rw₅ : H ⊔ K = f.range ⊓ (H ⊔ K)
Tactic: rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
f : G →* N
H K : Subgroup N
hH : H ≤ f.range
hK : K ≤ f.range
rw : map f (comap f H ⊔ comap f K) = f.range ⊓ (H ⊔ K)
rw₁ : map f (comap f H) ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₂ : f.range ⊓ H ⊔ map f (comap f K) = f.range ⊓ (H ⊔ K)
rw₃ : f.range ⊓ H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
rw₄ : H ⊔ f.range ⊓ K = f.range ⊓ (H ⊔ K)
rw₅ : H ⊔ K = f.range ⊓ (H ⊔ K)
⊢ map f (comap f H ⊔ comap f K) = map f (comap f (H ⊔ K))
have rw₆ : H ⊔ K = H ⊔ K
Tactic: rw [map_comap_eq, map_sup, map_comap_eq, map_comap_eq, inf_eq_right.mpr hH,
        inf_eq_right.mpr hK, inf_eq_right.mpr (sup_le hH hK)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B
have map_injective_of_ker_le : map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)
Tactic: refine
    map_injective_of_ker_le B.subtype (ker_le_comap _ _)
      (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)
have simp : B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
Tactic: simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
have rw : A ⊔ A' = B ⊓ A ⊔ B ⊓ A'
Tactic: rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
rw : A ⊔ A' = B ⊓ A ⊔ B ⊓ A'
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
have rw₁ : A ⊔ A' = B ⊓ A ⊔ A'
Tactic: rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
rw : A ⊔ A' = B ⊓ A ⊔ B ⊓ A'
rw₁ : A ⊔ A' = B ⊓ A ⊔ A'
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
have rw₂ : A ⊔ A' = A ⊔ A'
Tactic: rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ Codisjoint (α := Subgroup ↥(H ⊔ K)) (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))
have hA : H ≤ H ⊔ K
Tactic: rw [codisjoint_iff, ← subgroupOf_sup, subgroupOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hA : H ≤ H ⊔ K
⊢ Codisjoint (α := Subgroup ↥(H ⊔ K)) (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))
have hA' : K ≤ H ⊔ K
Tactic: rw [codisjoint_iff, ← subgroupOf_sup, subgroupOf_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
⊢ Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
have h : ∀ (x : M),
  Eq.{u_6 + 1} (α := N) ((MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : (a : M) → N) x : N)
    (((MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N) : (a : M) → N) x : N)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (hypothesis)
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
⊢ Eq (α := Subgroup N) (Subgroup.map (↑e : M →* N) (range (G := M) (powMonoidHom n))) (range (G := N) (powMonoidHom n))
have H : Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
  (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
Tactic: have H : (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by ext : 1; simp
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
H :
  Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
⊢ Eq (α := Subgroup N) (Subgroup.map (↑e : M →* N) (range (G := M) (powMonoidHom n))) (range (G := N) (powMonoidHom n))
have rw : Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n)))
  (range (G := N) (powMonoidHom n))
Tactic: rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
H :
  Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
rw :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n)))
    (range (G := N) (powMonoidHom n))
⊢ Eq (α := Subgroup N) (Subgroup.map (↑e : M →* N) (range (G := M) (powMonoidHom n))) (range (G := N) (powMonoidHom n))
have rw₁ : Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (powMonoidHom n) (↑e : M →* N)))
  (range (G := N) (powMonoidHom n))
Tactic: rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
H :
  Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
rw :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n)))
    (range (G := N) (powMonoidHom n))
rw₁ :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (powMonoidHom n) (↑e : M →* N)))
    (range (G := N) (powMonoidHom n))
⊢ Eq (α := Subgroup N) (Subgroup.map (↑e : M →* N) (range (G := M) (powMonoidHom n))) (range (G := N) (powMonoidHom n))
have rw₂ : Eq (α := Subgroup N) (Subgroup.map (powMonoidHom n) (range (↑e : M →* N))) (range (G := N) (powMonoidHom n))
Tactic: rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
H :
  Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
rw :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n)))
    (range (G := N) (powMonoidHom n))
rw₁ :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (powMonoidHom n) (↑e : M →* N)))
    (range (G := N) (powMonoidHom n))
rw₂ : Eq (α := Subgroup N) (Subgroup.map (powMonoidHom n) (range (↑e : M →* N))) (range (G := N) (powMonoidHom n))
⊢ Eq (α := Subgroup N) (Subgroup.map (↑e : M →* N) (range (G := M) (powMonoidHom n))) (range (G := N) (powMonoidHom n))
have rw₃ : Eq.{u_6 + 1} (α := Subgroup N) (Subgroup.map (G := N) (powMonoidHom n) ⊤) (range (G := N) (powMonoidHom n))
Tactic: rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Ker (goal)
Goal:
M : Type u_5
N : Type u_6
inst : CommGroup M
inst_1 : CommGroup N
e : M ≃* N
n : ℕ
H :
  Eq (α := M →* N) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n) : M →* N)
    (MonoidHom.comp (powMonoidHom n) (↑e : M →* N) : M →* N)
rw :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (↑e : M →* N) (powMonoidHom n)))
    (range (G := N) (powMonoidHom n))
rw₁ :
  Eq.{u_6 + 1} (α := Subgroup N) (range.{u_5, u_6} (G := M) (MonoidHom.comp (powMonoidHom n) (↑e : M →* N)))
    (range (G := N) (powMonoidHom n))
rw₂ : Eq (α := Subgroup N) (Subgroup.map (powMonoidHom n) (range (↑e : M →* N))) (range (G := N) (powMonoidHom n))
rw₃ : Eq.{u_6 + 1} (α := Subgroup N) (Subgroup.map (G := N) (powMonoidHom n) ⊤) (range (G := N) (powMonoidHom n))
⊢ Eq (α := Subgroup N) (Subgroup.map (↑e : M →* N) (range (G := M) (powMonoidHom n))) (range (G := N) (powMonoidHom n))
have rw₄ : Eq.{u_6 + 1} (α := Subgroup N) (range (G := N) (powMonoidHom n)) (range (G := N) (powMonoidHom n))
Tactic: rw [map_range, H, range_comp, e.range_eq_top, ← range_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : Subgroup G
⊢ (fun (S : AddSubgroup (Additive G)) ↦
        let __src : Submonoid (Multiplicative (Additive G)) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
            S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
      ((fun (S : Subgroup G) ↦
          let __src : AddSubmonoid (Additive G) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
          ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
        x) =
    x
have mk : ∀ (toSubmonoid : Submonoid G) (inv_mem' : ∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier),
  (fun (S : AddSubgroup (Additive G)) ↦
        let __src : Submonoid (Multiplicative (Additive G)) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
            S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := sorry : Subgroup G })
      ((fun (S : Subgroup G) ↦
          let __src : AddSubmonoid (Additive G) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
          ({ toAddSubmonoid := __src, neg_mem' := sorry } : AddSubgroup (Additive G)))
        { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' }) =
    { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' : Subgroup G }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : AddSubgroup (Additive G)
⊢ (fun (S : Subgroup G) ↦
        let __src : AddSubmonoid (Additive G) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
        ({ toAddSubmonoid := __src, neg_mem' := ⋯ } : AddSubgroup (Additive G)))
      ((fun (S : AddSubgroup (Additive G)) ↦
          let __src : Submonoid (Multiplicative (Additive G)) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
              S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ : Subgroup G })
        x) =
    x
have mk : ∀ (toAddSubmonoid : AddSubmonoid (Additive G))
  (neg_mem' : ∀ {x : Additive G}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier),
  (fun (S : Subgroup G) ↦
        let __src : AddSubmonoid (Additive G) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid G) → AddSubmonoid (Additive G)) S.toSubmonoid;
        ({ toAddSubmonoid := __src, neg_mem' := sorry } : AddSubgroup (Additive G)))
      ((fun (S : AddSubgroup (Additive G)) ↦
          let __src : Submonoid (Multiplicative (Additive G)) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid (Additive G)) → Submonoid (Multiplicative (Additive G)))
              S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := sorry : Subgroup G })
        { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' }) =
    { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' : AddSubgroup (Additive G) }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : AddSubgroup A
⊢ (fun (S : Subgroup (Multiplicative A)) ↦
        let __src : AddSubmonoid (Additive (Multiplicative A)) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
            S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
      ((fun (S : AddSubgroup A) ↦
          let __src : Submonoid (Multiplicative A) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
          ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
        x) =
    x
have mk : ∀ (toAddSubmonoid : AddSubmonoid A) (neg_mem' : ∀ {x : A}, x ∈ toAddSubmonoid.carrier → -x ∈ toAddSubmonoid.carrier),
  (fun (S : Subgroup (Multiplicative A)) ↦
        let __src : AddSubmonoid (Additive (Multiplicative A)) :=
          (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
            S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := sorry : AddSubgroup A })
      ((fun (S : AddSubgroup A) ↦
          let __src : Submonoid (Multiplicative A) :=
            (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
          ({ toSubmonoid := __src, inv_mem' := sorry } : Subgroup (Multiplicative A)))
        { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' }) =
    { toAddSubmonoid := toAddSubmonoid, neg_mem' := @neg_mem' : AddSubgroup A }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
A : Type u_2
inst_1 : AddGroup A
x : Subgroup (Multiplicative A)
⊢ (fun (S : AddSubgroup A) ↦
        let __src : Submonoid (Multiplicative A) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
        ({ toSubmonoid := __src, inv_mem' := ⋯ } : Subgroup (Multiplicative A)))
      ((fun (S : Subgroup (Multiplicative A)) ↦
          let __src : AddSubmonoid (Additive (Multiplicative A)) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
              S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ : AddSubgroup A })
        x) =
    x
have mk : ∀ (toSubmonoid : Submonoid (Multiplicative A))
  (inv_mem' : ∀ {x : Multiplicative A}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier),
  (fun (S : AddSubgroup A) ↦
        let __src : Submonoid (Multiplicative A) :=
          (AddSubmonoid.toSubmonoid : (a : AddSubmonoid A) → Submonoid (Multiplicative A)) S.toAddSubmonoid;
        ({ toSubmonoid := __src, inv_mem' := sorry } : Subgroup (Multiplicative A)))
      ((fun (S : Subgroup (Multiplicative A)) ↦
          let __src : AddSubmonoid (Additive (Multiplicative A)) :=
            (Submonoid.toAddSubmonoid : (a : Submonoid (Multiplicative A)) → AddSubmonoid (Additive (Multiplicative A)))
              S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := sorry : AddSubgroup A })
        { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' }) =
    { toSubmonoid := toSubmonoid, inv_mem' := @inv_mem' : Subgroup (Multiplicative A) }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Subsingleton.{u_1 + 1} ↥H
⊢ H = ⊥
have rw : ∀ x ∈ H, x = 1
Tactic: rw [Subgroup.eq_bot_iff_forall]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Subsingleton.{u_1 + 1} ↥H
y : G
hy : y ∈ H
⊢ y = 1
have rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) y hy) : G) = 1
Tactic: rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Subsingleton.{u_1 + 1} ↥H
y : G
hy : y ∈ H
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) y hy) : G) = 1
⊢ y = 1
have rw₁ : Eq.{u_1 + 1} (α := G) (↑1 : G) 1
Tactic: rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : Subsingleton.{u_1 + 1} ↥H
y : G
hy : y ∈ H
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) y hy) : G) = 1
rw₁ : Eq.{u_1 + 1} (α := G) (↑1 : G) 1
⊢ y = 1
have rw₂ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∃ (g : G), (↑H : Set G) = {g}
g : G
hg : (↑H : Set G) = {g}
⊢ Subsingleton.{u_1 + 1} (↑(↑H : Set G) : Type u_1)
have rw : Subsingleton.{u_1 + 1} (↑{g} : Type u_1)
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Nontrivial.{u_1} ↥H ↔ ∃ x ∈ H, x ≠ 1
have rw : (∃ (y : G) (_ : y ∈ H), y ≠ (↑1 : G)) ↔ ∃ x ∈ H, x ≠ 1
Tactic: rw [Subtype.nontrivial_iff_exists_ne (fun x => x ∈ H) (1 : H)]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Nontrivial.{u_1} ↥H ↔ H ≠ ⊥
have rw : (∃ x ∈ H, x ≠ 1) ↔ ¬∀ x ∈ H, x = 1
Tactic: rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (hypothesis)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ H = ⊥ ∨ Nontrivial.{u_1} ↥H
have this : Nontrivial.{u_1} ↥H ↔ H ≠ ⊥
Tactic: have := nontrivial_iff_ne_bot H
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
this : Nontrivial.{u_1} ↥H ↔ H ≠ ⊥
⊢ H = ⊥ ∨ Nontrivial.{u_1} ↥H
have inl : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
this : Nontrivial.{u_1} ↥H ↔ H ≠ ⊥
inl : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
⊢ H = ⊥ ∨ Nontrivial.{u_1} ↥H
have inr : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
this : Nontrivial.{u_1} ↥H ↔ H ≠ ⊥
inl : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inr : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inl₁ : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inr₁ : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
⊢ H = ⊥ ∨ Nontrivial.{u_1} ↥H
have inl₂ : Nontrivial.{u_1} ↥H → H ≠ ⊥ → ¬H = ⊥ → Nontrivial.{u_1} ↥H
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Lattice (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
this : Nontrivial.{u_1} ↥H ↔ H ≠ ⊥
inl : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inr : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inl₁ : Nontrivial.{u_1} ↥H → H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inr₁ : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → H = ⊥ ∨ Nontrivial.{u_1} ↥H
inl₂ : Nontrivial.{u_1} ↥H → H ≠ ⊥ → ¬H = ⊥ → Nontrivial.{u_1} ↥H
⊢ H = ⊥ ∨ Nontrivial.{u_1} ↥H
have inr₂ : ¬Nontrivial.{u_1} ↥H → ¬H ≠ ⊥ → ¬H = ⊥ → Nontrivial.{u_1} ↥H
Tactic: tauto
Cleared hypotheses: this