awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
x y : G
H : ({ toSetoid := leftRel f.ker, mul' := ⋯ } : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₁ : (leftRel f.ker : G → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₂ : (leftRel f.ker : G → G → Prop) y x ↔ (Con.ker f : (a : G) → G → Prop) x y
H₃ : y⁻¹ * x ∈ f.ker ↔ (Con.ker f : (a : G) → G → Prop) x y
⊢ (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
have H₄ : y⁻¹ * x ∈ f.ker ↔ Eq.{u_4 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
Tactic: rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
x y : G
H : ({ toSetoid := leftRel f.ker, mul' := ⋯ } : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₁ : (leftRel f.ker : G → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₂ : (leftRel f.ker : G → G → Prop) y x ↔ (Con.ker f : (a : G) → G → Prop) x y
H₃ : y⁻¹ * x ∈ f.ker ↔ (Con.ker f : (a : G) → G → Prop) x y
H₄ : y⁻¹ * x ∈ f.ker ↔ Eq.{u_4 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
⊢ (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
have H₅ : y⁻¹ * x ∈ f.ker ↔ y⁻¹ * x ∈ f.ker
Tactic: rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
x : G
⊢ Eq (α := G ⧸ N) (↑x : G ⧸ N) 1 ↔ x ∈ N
have refine : x⁻¹ * 1 ∈ N ↔ x ∈ N
Tactic: refine QuotientGroup.eq.trans ?_
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
x : G
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N
have rw : x⁻¹ ∈ N ↔ x ∈ N
Tactic: rw [mul_one, Subgroup.inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
x : G
rw : x⁻¹ ∈ N ↔ x ∈ N
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N
have rw₁ : x ∈ N ↔ x ∈ N
Tactic: rw [mul_one, Subgroup.inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ Eq (α := ↥N →* G ⧸ N) (MonoidHom.comp (mk' N) N.subtype) 1
have h : ∀ (x : ↥N),
  Eq (α := G ⧸ N) ((MonoidHom.comp (mk' N) N.subtype : (a : ↥N) → G ⧸ N) x : G ⧸ N) ((1 : (a : ↥N) → G ⧸ N) x : G ⧸ N)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ Eq (α := G ⧸ N) (↑x : G ⧸ N) (↑y : G ⧸ N) ↔ x / y ∈ N
have refine : y⁻¹ * x ∈ N ↔ x / y ∈ N
Tactic: refine eq_comm.trans (QuotientGroup.eq.trans ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
have rw : x * y⁻¹ ∈ N ↔ x / y ∈ N
Tactic: rw [nN.mem_comm_iff, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x y : G
rw : x * y⁻¹ ∈ N ↔ x / y ∈ N
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
have rw₁ : x * y⁻¹ ∈ N ↔ x * y⁻¹ ∈ N
Tactic: rw [nN.mem_comm_iff, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
⊢ (QuotientGroup.con H).subgroup = H
have h : ∀ (x : G), x ∈ (QuotientGroup.con H).subgroup ↔ x ∈ H
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
c : Con G
⊢ QuotientGroup.con c.subgroup = c
have H : ∀ (x y : G), (QuotientGroup.con c.subgroup : (a : G) → G → Prop) x y ↔ (c : (a : G) → G → Prop) x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
c : Con G
x y : G
⊢ (QuotientGroup.con c.subgroup : (a : G) → G → Prop) x y ↔ (c : (a : G) → G → Prop) x y
have H : (c : (a : G) → G → Prop) (x⁻¹ * y) 1 ↔ (c : (a : G) → G → Prop) x y
Tactic: rw [QuotientGroup.con, Con.rel_mk, leftRel_apply, Con.mem_subgroup_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
⊢ ∀ {a b : { N : Subgroup G // N.Normal }},
    LE.le (α := Con G)
        (({ toFun := fun (N : { N : Subgroup G // N.Normal }) ↦ QuotientGroup.con (↑N : Subgroup G),
                invFun := fun (c : Con G) ↦ Subtype.mk (p := fun (N : Subgroup G) ↦ N.Normal) c.subgroup ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : { N : Subgroup G // N.Normal }) → Con G)
            a :
          Con G)
        (({ toFun := fun (N : { N : Subgroup G // N.Normal }) ↦ QuotientGroup.con (↑N : Subgroup G),
                invFun := fun (c : Con G) ↦ Subtype.mk (p := fun (N : Subgroup G) ↦ N.Normal) c.subgroup ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : { N : Subgroup G // N.Normal }) → Con G)
            b :
          Con G) ↔
      a ≤ b
have simp : ∀ {a b : { N : Subgroup G // N.Normal }},
  (∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)) ↔ a ≤ b
Tactic: simp only [QuotientGroup.con, Equiv.coe_fn_mk, Con.le_def, Con.rel_mk, leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
⊢ ∀ {a b : { N : Subgroup G // N.Normal }},
    (∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)) ↔ a ≤ b
have refine : ∀ {a b : { N : Subgroup G // N.Normal }} (h : ∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)),
  ∀ x ∈ (↑a : Subgroup G), x ∈ (↑b : Subgroup G)
Tactic: refine ⟨fun h x _ ↦ ?_, fun hle _ _ h ↦ hle h⟩
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (hypothesis)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
a b : { N : Subgroup G // N.Normal }
h : ∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)
x : G
h_1 : x ∈ (↑a : Subgroup G)
⊢ x ∈ (↑b : Subgroup G)
have h₁ : 1⁻¹ * x ∈ (↑a : Subgroup G) → 1⁻¹ * x ∈ (↑b : Subgroup G)
Tactic: specialize @h 1 x
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN)) (Subgroup.map (mk' N) φ.ker)
have rw : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN))
  (Subgroup.map (mk' N) (MonoidHom.comp (lift N φ HN) (mk' N)).ker)
Tactic: rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
    Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
rw :
  Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN))
    (Subgroup.map (mk' N) (MonoidHom.comp (lift N φ HN) (mk' N)).ker)
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN)) (Subgroup.map (mk' N) φ.ker)
have rw₁ : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN))
  (Subgroup.map (mk' N) (Subgroup.comap (mk' N) (MonoidHom.ker (lift N φ HN))))
Tactic: rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
    Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
rw :
  Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN))
    (Subgroup.map (mk' N) (MonoidHom.comp (lift N φ HN) (mk' N)).ker)
rw₁ :
  Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN))
    (Subgroup.map (mk' N) (Subgroup.comap (mk' N) (MonoidHom.ker (lift N φ HN))))
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN)) (Subgroup.map (mk' N) φ.ker)
have rw₂ : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN)) (MonoidHom.ker (lift N φ HN))
Tactic: rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
    Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* H
hφ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
HN : N = φ.ker
⊢ Injective.{u_1 + 1, u_2 + 1} (α := G ⧸ N) (β := H) (⇑(lift N φ ⋯) : (a : G ⧸ N) → H)
have rw : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ sorry)) ⊥
Tactic: rw [← MonoidHom.ker_eq_bot_iff, ker_lift, ← HN, QuotientGroup.map_mk'_self]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* H
hφ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
HN : N = φ.ker
rw : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ ⋯)) ⊥
⊢ Injective.{u_1 + 1, u_2 + 1} (α := G ⧸ N) (β := H) (⇑(lift N φ ⋯) : (a : G ⧸ N) → H)
have rw₁ : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) φ.ker) ⊥
Tactic: rw [← MonoidHom.ker_eq_bot_iff, ker_lift, ← HN, QuotientGroup.map_mk'_self]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* H
hφ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
HN : N = φ.ker
rw : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ ⋯)) ⊥
rw₁ : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) φ.ker) ⊥
⊢ Injective.{u_1 + 1, u_2 + 1} (α := G ⧸ N) (β := H) (⇑(lift N φ ⋯) : (a : G ⧸ N) → H)
have rw₂ : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) N) ⊥
Tactic: rw [← MonoidHom.ker_eq_bot_iff, ker_lift, ← HN, QuotientGroup.map_mk'_self]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* H
hφ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
HN : N = φ.ker
rw : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ ⋯)) ⊥
rw₁ : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) φ.ker) ⊥
rw₂ : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) N) ⊥
⊢ Injective.{u_1 + 1, u_2 + 1} (α := G ⧸ N) (β := H) (⇑(lift N φ ⋯) : (a : G ⧸ N) → H)
have rw₃ : Eq.{u_1 + 1} (α := Subgroup (G ⧸ N)) ⊥ ⊥
Tactic: rw [← MonoidHom.ker_eq_bot_iff, ker_lift, ← HN, QuotientGroup.map_mk'_self]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)
have refine : N ≤ MonoidHom.ker (MonoidHom.comp (mk' M) f)
Tactic: refine QuotientGroup.lift N ((mk' M).comp f) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ x ∈ MonoidHom.ker (MonoidHom.comp (mk' M) f)
have refine : HMul.hMul (α := H) (β := H) (((f : (a : G) → H) x)⁻¹ : H) (1 : H) ∈ M
Tactic: refine QuotientGroup.eq.2 ?_
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ HMul.hMul (α := H) (β := H) (((f : (a : G) → H) x)⁻¹ : H) (1 : H) ∈ M
have rw : Membership.mem (α := H) M ((f : (a : G) → H) x : H)
Tactic: rw [mul_one, Subgroup.inv_mem_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_2 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (map N M f h)) (Subgroup.map (mk' N) (Subgroup.comap f M))
have simp_rw : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (map N M f h))
  (Subgroup.map (mk' N) (MonoidHom.ker (MonoidHom.comp (mk' M) f)))
Tactic: simp_rw [← ker_mk' M, MonoidHom.comap_ker]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst_2 : Group I
M : Subgroup H
O : Subgroup I
inst_3 : M.Normal
inst_4 : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x : G ⧸ N
⊢ Eq.{u_5 + 1} (α := I ⧸ O)
    (((map M O g hg : MonoidHom.{u_2, u_5} (H ⧸ M) (I ⧸ O)) : (a : H ⧸ M) → I ⧸ O)
        (((map N M f hf : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) x) :
      I ⧸ O)
    (((map N O (g.comp f) hgf : MonoidHom.{u_1, u_5} (G ⧸ N) (I ⧸ O)) : (a : G ⧸ N) → I ⧸ O) x : I ⧸ O)
have refine : ∀ (x : G),
  Eq.{u_5 + 1} (α := I ⧸ O)
    (((map M O g hg : MonoidHom.{u_2, u_5} (H ⧸ M) (I ⧸ O)) : (a : H ⧸ M) → I ⧸ O)
        (((map N M f hf : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) (↑x : G ⧸ N)) :
      I ⧸ O)
    (((map N O (g.comp f) hgf : MonoidHom.{u_1, u_5} (G ⧸ N) (I ⧸ O)) : (a : G ⧸ N) → I ⧸ O) (↑x : G ⧸ N) : I ⧸ O)
Tactic: refine induction_on x fun x => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
⊢ preimage (β := G ⧸ N) mk (mk '' s) = (↑N : Set G) * s
have h : ∀ (a : G), a ∈ preimage (β := G ⧸ N) mk (mk '' s) ↔ a ∈ (↑N : Set G) * s
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
⊢ a ∈ preimage (β := G ⧸ N) mk (mk '' s) ↔ a ∈ (↑N : Set G) * s
have h : a ∈ preimage (β := G ⧸ N) mk (mk '' s) → a ∈ (↑N : Set G) * s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
h : a ∈ preimage (β := G ⧸ N) mk (mk '' s) → a ∈ (↑N : Set G) * s
⊢ a ∈ preimage (β := G ⧸ N) mk (mk '' s) ↔ a ∈ (↑N : Set G) * s
have h₁ : a ∈ (↑N : Set G) * s → a ∈ preimage (β := G ⧸ N) mk (mk '' s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : Eq (α := G ⧸ N) (↑b : G ⧸ N) (↑a : G ⧸ N)
⊢ a ∈ (↑N : Set G) * s
have h₁ : Eq (α := G ⧸ N) (↑(a / b) : G ⧸ N) 1
Tactic: refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ (↑N : Set G)
b : G
hb : b ∈ s
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ preimage (β := G ⧸ N) mk (mk '' s)
have h : Eq (α := G ⧸ N) (↑b : G ⧸ N) (↑((fun (x1 x2 : G) ↦ x1 * x2) a b) : G ⧸ N)
Tactic: refine ⟨b, hb, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ Eq (α := Set (G ⧸ N)) (mk '' s) (mk '' t) ↔ (↑N : Set G) * s = (↑N : Set G) * t
have simp_rw : Eq (α := Set (G ⧸ N)) (mk '' s) (mk '' t) ↔ preimage (β := G ⧸ N) mk (mk '' s) = preimage (β := G ⧸ N) mk (mk '' t)
Tactic: simp_rw [← preimage_image_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst_3 : G'.Normal
inst_4 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : G ⧸ G'
⊢ ((map H' G' (↑e.symm : H →* G) ⋯ : MonoidHom.{u_2, u_1} (H ⧸ H') (G ⧸ G')) : (a : H ⧸ H') → G ⧸ G')
      (((map G' H' (↑e : G →* H) ⋯ : MonoidHom.{u_1, u_2} (G ⧸ G') (H ⧸ H')) : (a : G ⧸ G') → H ⧸ H') x) =
    x
have rw : (map G' G' (MonoidHom.comp (↑e.symm : H →* G) (↑e : G →* H)) sorry : (a : G ⧸ G') → G ⧸ G') x = x
Tactic: rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H))
        (he ▸ (G'.map_equiv_eq_comap_symm e).le)]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst_3 : G'.Normal
inst_4 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : H ⧸ H'
⊢ ((map G' H' (↑e : G →* H) ⋯ : MonoidHom.{u_1, u_2} (G ⧸ G') (H ⧸ H')) : (a : G ⧸ G') → H ⧸ H')
      (((map H' G' (↑e.symm : H →* G) ⋯ : MonoidHom.{u_2, u_1} (H ⧸ H') (G ⧸ G')) : (a : H ⧸ H') → G ⧸ G') x) =
    x
have rw : (map H' H' (MonoidHom.comp (↑e : G →* H) (↑e.symm : H →* G)) sorry : (a : H ⧸ H') → H ⧸ H') x = x
Tactic: rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le)
        (he ▸ G'.le_comap_map (e : G →* H))]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Defs (goal)
Goal:
G : Type u_1
inst : Group G
G' : Subgroup G
inst_1 : G'.Normal
he : Subgroup.map (↑(MulEquiv.refl G) : G →* G) G' = G'
⊢ Eq (α := G ⧸ G' ≃* G ⧸ G') (congr G' G' (MulEquiv.refl G) he) (MulEquiv.refl (G ⧸ G'))
have h : ∀ (x : G ⧸ G') (x : G),
  Eq (α := G ⧸ G')
    ((congr G' G' (MulEquiv.refl G) he : (a : G ⧸ G') → G ⧸ G') (Quot.mk (⇑(leftRel G') : G → G → Prop) x) : G ⧸ G')
    ((MulEquiv.refl (G ⧸ G') : (a : G ⧸ G') → G ⧸ G') (Quot.mk (⇑(leftRel G') : G → G → Prop) x) : G ⧸ G')
Tactic: ext ⟨x⟩
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Finite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
⊢ Finite G ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
have rw : Finite.{u_2 + 1} ((G ⧸ H) × ↥H) ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
Tactic: rw [(groupEquivQuotientProdSubgroup (s := H)).finite_iff, Prod.finite_iff, and_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Finite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
rw : Finite.{u_2 + 1} ((G ⧸ H) × ↥H) ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
⊢ Finite G ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
have rw₁ : Finite.{u_2 + 1} (G ⧸ H) ∧ Finite.{u_2 + 1} ↥H ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
Tactic: rw [(groupEquivQuotientProdSubgroup (s := H)).finite_iff, Prod.finite_iff, and_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Finite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
rw : Finite.{u_2 + 1} ((G ⧸ H) × ↥H) ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
rw₁ : Finite.{u_2 + 1} (G ⧸ H) ∧ Finite.{u_2 + 1} ↥H ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
⊢ Finite G ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
have rw₂ : Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H) ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
Tactic: rw [(groupEquivQuotientProdSubgroup (s := H)).finite_iff, Prod.finite_iff, and_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Finite (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_2 + 1} ↥H
inst_2 : Finite.{u_2 + 1} (G ⧸ H)
⊢ Finite G
have rw : Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
Tactic: rw [finite_iff_subgroup_quotient]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
⊢ a ≡ b [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
have rw : b ≡ a [PMOD p] ↔
  Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
    (↑b : G ⧸ AddSubgroup.zmultiples p)
Tactic: rw [modEq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
⊢ b ≡ a [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
have simp_rw : (∃ (z : ℤ), a = b + z • p) ↔
  Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
    (↑b : G ⧸ AddSubgroup.zmultiples p)
Tactic: simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
simp_rw :
  (∃ (z : ℤ), a = b + z • p) ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
⊢ b ≡ a [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
have simp_rw₁ : (∃ (z : ℤ), a = b + z • p) ↔ Membership.mem (γ := AddSubgroup G) (AddSubgroup.zmultiples p) (a - b)
Tactic: simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
simp_rw :
  (∃ (z : ℤ), a = b + z • p) ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
simp_rw₁ : (∃ (z : ℤ), a = b + z • p) ↔ Membership.mem (γ := AddSubgroup G) (AddSubgroup.zmultiples p) (a - b)
⊢ b ≡ a [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
have simp_rw₂ : (∃ (z : ℤ), a = b + z • p) ↔ ∃ (k : ℤ), k • p = a - b
Tactic: simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.ModEq (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
simp_rw :
  (∃ (z : ℤ), a = b + z • p) ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
simp_rw₁ : (∃ (z : ℤ), a = b + z • p) ↔ Membership.mem (γ := AddSubgroup G) (AddSubgroup.zmultiples p) (a - b)
simp_rw₂ : (∃ (z : ℤ), a = b + z • p) ↔ ∃ (k : ℤ), k • p = a - b
⊢ b ≡ a [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
have simp_rw₃ : (∃ (z : ℤ), a = b + z • p) ↔ ∃ (k : ℤ), b + k • p = a
Tactic: simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.Rank (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
inst_2 : FG G
inst_3 : FG H
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
⊢ rank H ≤ rank G
have obtain : ∀ (S : Finset G) (hS1 : S.card = rank G) (hS2 : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤), rank H ≤ rank G
Tactic: obtain ⟨S, hS1, hS2⟩ := rank_spec G