awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₂ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₃ :
  s ⊔ t =
    mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₄ : s ⊔ t = mrange s.subtype ⊔ map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₅ : s ⊔ t = mrange s.subtype ⊔ mrange ((s.subtype.coprod t.subtype).comp (inr ↥s ↥t))
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₂ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₃ :
  s ⊔ t =
    mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₄ : s ⊔ t = mrange s.subtype ⊔ map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₅ : s ⊔ t = mrange s.subtype ⊔ mrange ((s.subtype.coprod t.subtype).comp (inr ↥s ↥t))
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₆ : s ⊔ t = mrange s.subtype ⊔ mrange t.subtype
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₂ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₃ :
  s ⊔ t =
    mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₄ : s ⊔ t = mrange s.subtype ⊔ map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₅ : s ⊔ t = mrange s.subtype ⊔ mrange ((s.subtype.coprod t.subtype).comp (inr ↥s ↥t))
rw₆ : s ⊔ t = mrange s.subtype ⊔ mrange t.subtype
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₇ : s ⊔ t = s ⊔ mrange t.subtype
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
s t : Submonoid N
rw : s ⊔ t = map (s.subtype.coprod t.subtype) ⊤
rw₁ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t) ⊔ mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₂ :
  s ⊔ t =
    map (s.subtype.coprod t.subtype) (mrange (F := ↥s →* ↥s × ↥t) (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₃ :
  s ⊔ t =
    mrange ((s.subtype.coprod t.subtype).comp (inl ↥s ↥t)) ⊔
      map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₄ : s ⊔ t = mrange s.subtype ⊔ map (s.subtype.coprod t.subtype) (mrange (F := ↥t →* ↥s × ↥t) (inr ↥s ↥t))
rw₅ : s ⊔ t = mrange s.subtype ⊔ mrange ((s.subtype.coprod t.subtype).comp (inr ↥s ↥t))
rw₆ : s ⊔ t = mrange s.subtype ⊔ mrange t.subtype
rw₇ : s ⊔ t = s ⊔ mrange t.subtype
⊢ s ⊔ t = mrange (s.subtype.coprod t.subtype)
have rw₈ : s ⊔ t = s ⊔ t
Tactic: rw [mrange_eq_map, ← mrange_inl_sup_mrange_inr, map_sup, map_mrange, coprod_comp_inl, map_mrange,
    coprod_comp_inr, mrange_subtype, mrange_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
N : Type u_4
inst : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)
have simp : (∀ (x x_1 : N), x_1 ∈ s → ∀ x_2 ∈ t, x_1 * x_2 = x → P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)
Tactic: simp [mem_sup]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
A : Type u_2
inst : AddMonoid A
x y : A
⊢ Membership.mem (γ := AddSubmonoid A) (closure {x}) y ↔ ∃ (n : ℕ), n • x = y
have rw : (∃ (x_1 : ℕ), (((multiplesHom A : (a : A) → ℕ →+ A) x : ℕ →+ A) : (a : ℕ) → A) x_1 = y) ↔ ∃ (n : ℕ), n • x = y
Tactic: rw [closure_singleton_eq, AddMonoidHom.mem_mrange]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
A : Type u_4
inst : CommMonoid A
a b c : A
⊢ Membership.mem (γ := Submonoid A) (closure {a, b}) c ↔ ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c
have rw : (∃ (y : A),
    Membership.mem (γ := Submonoid A) (closure {a}) y ∧
      ∃ (z : A), Membership.mem (γ := Submonoid A) (closure {b}) z ∧ y * z = c) ↔
  ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c
Tactic: rw [← Set.singleton_union, Submonoid.closure_union, mem_sup]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
A : Type u_4
inst : CommMonoid A
a b c : A
⊢ (∃ (y : A),
      Membership.mem (γ := Submonoid A) (closure {a}) y ∧
        ∃ (z : A), Membership.mem (γ := Submonoid A) (closure {b}) z ∧ y * z = c) ↔
    ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c
have simp_rw : (∃ (y : A), (∃ (n : ℕ), a ^ n = y) ∧ ∃ (z : A), (∃ (n : ℕ), b ^ n = z) ∧ y * z = c) ↔
  ∃ (m : ℕ) (n : ℕ), a ^ m * b ^ n = c
Tactic: simp_rw [mem_closure_singleton, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
M : Type u_1
inst : Monoid M
x : M
⊢ (⇑Additive.ofMul : (a : M) → Additive M) '' (↑(Submonoid.powers x) : Set M) =
    (↑(AddSubmonoid.multiples ((Additive.ofMul : (a : M) → Additive M) x) : AddSubmonoid (Additive M)) :
      Set (Additive M))
have h : ∀ (x_1 : Additive M),
  Membership.mem (γ := Set (Additive M)) ((⇑Additive.ofMul : (a : M) → Additive M) '' (↑(Submonoid.powers x) : Set M))
      x_1 ↔
    x_1 ∈
      (↑(AddSubmonoid.multiples ((Additive.ofMul : (a : M) → Additive M) x) : AddSubmonoid (Additive M)) :
        Set (Additive M))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
A : Type u_2
inst : AddMonoid A
x : A
⊢ (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubmonoid.multiples x) : Set A) =
    (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
      Set (Multiplicative A))
have symm : (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
    Set (Multiplicative A)) =
  (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubmonoid.multiples x) : Set A)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
A : Type u_2
inst : AddMonoid A
x : A
⊢ (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
      Set (Multiplicative A)) =
    (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) '' (↑(AddSubmonoid.multiples x) : Set A)
have rw : (⇑(Equiv.symm Multiplicative.ofAdd) : (a : Multiplicative A) → A) ''
    (↑(Submonoid.powers ((Multiplicative.ofAdd : (a : A) → Multiplicative A) x) : Submonoid (Multiplicative A)) :
      Set (Multiplicative A)) =
  (↑(AddSubmonoid.multiples x) : Set A)
Tactic: rw [Equiv.eq_image_iff_symm_image_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Membership (goal)
Goal:
⊢ Eq (α := AddSubmonoid ℕ) (AddSubmonoid.closure {1}) ⊤
have h : ∀ (x : ℕ), Membership.mem (γ := AddSubmonoid ℕ) (AddSubmonoid.closure {1}) x ↔ Membership.mem (γ := AddSubmonoid ℕ) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.MulOpposite (goal)
Goal:
M : Type u_2
inst : MulOneClass M
s : Set M
⊢ Eq (α := Submonoid Mᵐᵒᵖ) (Submonoid.op (closure s)) (closure (MulOpposite.unop ⁻¹' s))
have simp_rw : Eq.{u_2 + 1} (α := Submonoid Mᵐᵒᵖ) (sInf {a : Submonoid Mᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ)})
  (sInf {S : Submonoid Mᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Mᵐᵒᵖ)})
Tactic: simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Submonoid.coe_unop]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.MulOpposite (goal)
Goal:
M : Type u_2
inst : MulOneClass M
s : Set M
⊢ Eq.{u_2 + 1} (α := Submonoid Mᵐᵒᵖ) (sInf {a : Submonoid Mᵐᵒᵖ | s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ)})
    (sInf {S : Submonoid Mᵐᵒᵖ | MulOpposite.unop ⁻¹' s ⊆ (↑S : Set Mᵐᵒᵖ)})
have e_a : ∀ (a : Submonoid Mᵐᵒᵖ), s ⊆ MulOpposite.op ⁻¹' (↑a : Set Mᵐᵒᵖ) ↔ MulOpposite.unop ⁻¹' s ⊆ (↑a : Set Mᵐᵒᵖ)
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.MulOpposite (goal)
Goal:
M : Type u_2
inst : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ Eq (α := Submonoid M) (Submonoid.unop (closure s)) (closure (MulOpposite.op ⁻¹' s))
have rw : Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
Tactic: rw [← op_inj, op_unop, op_closure]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.MulOpposite (goal)
Goal:
M : Type u_2
inst : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw : Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.MulOpposite (goal)
Goal:
M : Type u_2
inst : MulOneClass M
s : Set Mᵐᵒᵖ
simp_rw : Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ MulOpposite.op (MulOpposite.unop x)) ⁻¹' s))
⊢ Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s))
have simp_rw₁ : Eq (α := Submonoid Mᵐᵒᵖ) (closure s) (closure ((fun (x : Mᵐᵒᵖ) ↦ x) ⁻¹' s))
Tactic: simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S x : Submonoid M
⊢ (fun (S : AddSubmonoid (Additive M)) ↦
        ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
            one_mem' := ⋯ } :
          Submonoid M))
      ((fun (S : Submonoid M) ↦
          ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid (Additive M)))
        x) =
    x
have mk : ∀ (toSubsemigroup : Subsemigroup M) (one_mem' : 1 ∈ toSubsemigroup.carrier),
  (fun (S : AddSubmonoid (Additive M)) ↦
        ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := sorry,
            one_mem' := sorry } :
          Submonoid M))
      ((fun (S : Submonoid M) ↦
          ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := sorry, zero_mem' := sorry } :
            AddSubmonoid (Additive M)))
        { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }) =
    { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid M }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S : Submonoid M
x : AddSubmonoid (Additive M)
⊢ (fun (S : Submonoid M) ↦
        ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := ⋯, zero_mem' := ⋯ } :
          AddSubmonoid (Additive M)))
      ((fun (S : AddSubmonoid (Additive M)) ↦
          ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid M))
        x) =
    x
have mk : ∀ (toAddSubsemigroup : AddSubsemigroup (Additive M)) (zero_mem' : 0 ∈ toAddSubsemigroup.carrier),
  (fun (S : Submonoid M) ↦
        ({ carrier := (⇑Additive.toMul : (a : Additive M) → M) ⁻¹' (↑S : Set M), add_mem' := sorry, zero_mem' := sorry } :
          AddSubmonoid (Additive M)))
      ((fun (S : AddSubmonoid (Additive M)) ↦
          ({ carrier := (⇑Additive.ofMul : (a : M) → Additive M) ⁻¹' (↑S : Set (Additive M)), mul_mem' := sorry,
              one_mem' := sorry } :
            Submonoid M))
        { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' }) =
    { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' : AddSubmonoid (Additive M) }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S : Submonoid M
A : Type u_4
inst_3 : AddZeroClass A
x : AddSubmonoid A
⊢ (fun (S : Submonoid (Multiplicative A)) ↦
        ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
            add_mem' := ⋯, zero_mem' := ⋯ } :
          AddSubmonoid A))
      ((fun (S : AddSubmonoid A) ↦
          ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
              one_mem' := ⋯ } :
            Submonoid (Multiplicative A)))
        x) =
    x
have mk : ∀ (toAddSubsemigroup : AddSubsemigroup A) (zero_mem' : 0 ∈ toAddSubsemigroup.carrier),
  (fun (S : Submonoid (Multiplicative A)) ↦
        ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
            add_mem' := sorry, zero_mem' := sorry } :
          AddSubmonoid A))
      ((fun (S : AddSubmonoid A) ↦
          ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := sorry,
              one_mem' := sorry } :
            Submonoid (Multiplicative A)))
        { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' }) =
    { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' : AddSubmonoid A }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S : Submonoid M
A : Type u_4
inst_3 : AddZeroClass A
x : Submonoid (Multiplicative A)
⊢ (fun (S : AddSubmonoid A) ↦
        ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := ⋯,
            one_mem' := ⋯ } :
          Submonoid (Multiplicative A)))
      ((fun (S : Submonoid (Multiplicative A)) ↦
          ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
              add_mem' := ⋯, zero_mem' := ⋯ } :
            AddSubmonoid A))
        x) =
    x
have mk : ∀ (toSubsemigroup : Subsemigroup (Multiplicative A)) (one_mem' : 1 ∈ toSubsemigroup.carrier),
  (fun (S : AddSubmonoid A) ↦
        ({ carrier := (⇑Multiplicative.toAdd : (a : Multiplicative A) → A) ⁻¹' (↑S : Set A), mul_mem' := sorry,
            one_mem' := sorry } :
          Submonoid (Multiplicative A)))
      ((fun (S : Submonoid (Multiplicative A)) ↦
          ({ carrier := (⇑Multiplicative.ofAdd : (a : A) → Multiplicative A) ⁻¹' (↑S : Set (Multiplicative A)),
              add_mem' := sorry, zero_mem' := sorry } :
            AddSubmonoid A))
        { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' }) =
    { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' : Submonoid (Multiplicative A) }
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S_1 : Submonoid M
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
a b : M
ha : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) a
hb : Membership.mem (γ := Set M) ((⇑f : (a : M) → N) ⁻¹' (↑S : Set N)) b
⊢ Membership.mem (α := N) S ((f : (a : M) → N) (a * b) : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N) ∈ S
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S_1 : Submonoid M
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
⊢ Membership.mem (α := N) S ((f : (a : M) → N) 1 : N)
have rw : 1 ∈ S
Tactic: rw [map_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S_1 : Submonoid M
F : Type u_4
inst_3 : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid M
x : M
hx : x ∈ (↑S : Set M)
y : M
hy : y ∈ (↑S : Set M)
⊢ (f : (a : M) → N) (x * y) = HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
have rw : HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N) =
  HMul.hMul (α := N) (β := N) ((f : (a : M) → N) x : N) ((f : (a : M) → N) y : N)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
ι : Sort u_5
inst_3 : Nonempty ι
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
s : ι → Submonoid M
⊢ Eq (α := Submonoid N) (map f (iInf s)) (⨅ (i : ι), map f (s i))
have a : (↑(map f (iInf s)) : Set N) = (↑(⨅ (i : ι), map f (s i)) : Set N)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Disjoint H K
⊢ Disjoint (α := Submonoid N) (map f H) (map f K)
have rw : Eq (α := Submonoid N) (map f H ⊓ map f K) ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Disjoint H K
rw : Eq (α := Submonoid N) (map f H ⊓ map f K) ⊥
⊢ Disjoint (α := Submonoid N) (map f H) (map f K)
have rw₁ : Eq (α := Submonoid N) (map f (H ⊓ K)) ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Disjoint H K
rw : Eq (α := Submonoid N) (map f H ⊓ map f K) ⊥
rw₁ : Eq (α := Submonoid N) (map f (H ⊓ K)) ⊥
⊢ Disjoint (α := Submonoid N) (map f H) (map f K)
have rw₂ : Eq (α := Submonoid N) (map f ⊥) ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
N : Type u_2
inst : MulOneClass M
inst_1 : MulOneClass N
F : Type u_4
inst_2 : FunLike F M N
mc : MonoidHomClass F M N
f : F
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Disjoint H K
rw : Eq (α := Submonoid N) (map f H ⊓ map f K) ⊥
rw₁ : Eq (α := Submonoid N) (map f (H ⊓ K)) ⊥
rw₂ : Eq (α := Submonoid N) (map f ⊥) ⊥
⊢ Disjoint (α := Submonoid N) (map f H) (map f K)
have rw₃ : Eq.{u_2 + 1} (α := Submonoid N) ⊥ ⊥
Tactic: rw [disjoint_iff, ← map_inf _ _ f hf, disjoint_iff.mp h, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t ↔ map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t
have mp : u ≤ s.prod t → map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
mp : u ≤ s.prod t → map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t
⊢ u ≤ s.prod t ↔ map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t
have mpr : map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t → u ≤ s.prod t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t
have mp : map (F := M × N →* M) (fst M N) u ≤ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
mp : map (F := M × N →* M) (fst M N) u ≤ s
⊢ map (F := M × N →* M) (fst M N) u ≤ s ∧ map (F := M × N →* N) (snd M N) u ≤ t
have mp₁ : map (F := M × N →* N) (snd M N) u ≤ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ s.prod t ≤ u ↔ map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u
have mp : s.prod t ≤ u → map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
mp : s.prod t ≤ u → map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u
⊢ s.prod t ≤ u ↔ map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u
have mpr : map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u → s.prod t ≤ u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
⊢ map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u
have mp : map (F := M →* M × N) (inl M N) s ≤ u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
N : Type u_2
inst : MulOneClass N
M : Type u_5
inst_1 : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
mp : map (F := M →* M × N) (inl M N) s ≤ u
⊢ map (F := M →* M × N) (inl M N) s ≤ u ∧ map (F := N →* M × N) (inr M N) t ≤ u
have mp₁ : map (F := N →* M × N) (inr M N) t ≤ u
Tactic: constructor