awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : M
hx : x ∈ (↑s : Set M)
⊢ Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x : M × N)
have mp : Membership.mem (α := M × N) (s.prod t) ((inl M N : (a : M) → M × N) x : M × N)
Tactic: apply h
-- 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
x : N
hx : x ∈ (↑t : Set N)
⊢ Membership.mem (α := M × N) u ((inr M N : (a : N) → M × N) x : M × N)
have mp : Membership.mem (α := M × N) (s.prod t) ((inr M N : (a : N) → M × N) x : M × N)
Tactic: apply h
-- 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)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
⊢ Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
have a : Membership.mem (α := M × N) (γ := Submonoid (M × N)) (map (F := M →* M × N) (inl M N) s)
  ((inl M N : (a : M) → M × N) x1 : M × N)
Tactic: apply hH
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (hypothesis)
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)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
⊢ (x1, x2) ∈ u
have h1' : Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
Tactic: have h1' : inl M N x1 ∈ u := by
      apply hH
      simpa using h1
-- 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)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
h1' : Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
⊢ Membership.mem (α := M × N) u ((inr M N : (a : N) → M × N) x2 : M × N)
have a : Membership.mem (α := M × N) (γ := Submonoid (M × N)) (map (F := N →* M × N) (inr M N) t)
  ((inr M N : (a : N) → M × N) x2 : M × N)
Tactic: apply hK
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (hypothesis)
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)
hH : map (F := M →* M × N) (inl M N) s ≤ u
hK : map (F := N →* M × N) (inr M N) t ≤ u
x1 : M
x2 : N
h1 : (x1, x2).1 ∈ (↑s : Set M)
h2 : (x1, x2).2 ∈ (↑t : Set N)
h1' : Membership.mem (α := M × N) u ((inl M N : (a : M) → M × N) x1 : M × N)
⊢ (x1, x2) ∈ u
have h2' : Membership.mem (α := M × N) u ((inr M N : (a : N) → M × N) x2 : M × N)
Tactic: have h2' : inr M N x2 ∈ u := by
      apply hK
      simpa using h2
-- 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
⊢ (↑(mrange f) : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
have rw : Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
  Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
Tactic: rw [coe_mrange, coe_top]
-- 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
rw :
  Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N) = (↑⊤ : Set N) ↔
    Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
⊢ (↑(mrange f) : Set N) = (↑⊤ : Set N) ↔
    Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
have rw₁ : Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ ↔
  Eq.{u_2 + 1} (α := Set N) (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N)) Set.univ
Tactic: rw [coe_mrange, coe_top]
-- 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
⊢ Eq (α := Submonoid N) (closure (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N))) (mrange f)
have rw : Eq (α := Submonoid N) (closure (Set.image.{u_1, u_2} (α := M) (⇑f : (a : M) → N) Set.univ)) (mrange f)
Tactic: rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]
-- 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
rw : Eq (α := Submonoid N) (closure (Set.image.{u_1, u_2} (α := M) (⇑f : (a : M) → N) Set.univ)) (mrange f)
⊢ Eq (α := Submonoid N) (closure (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N))) (mrange f)
have rw₁ : Eq (α := Submonoid N) (map f (closure Set.univ)) (mrange f)
Tactic: rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]
-- 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
rw : Eq (α := Submonoid N) (closure (Set.image.{u_1, u_2} (α := M) (⇑f : (a : M) → N) Set.univ)) (mrange f)
rw₁ : Eq (α := Submonoid N) (map f (closure Set.univ)) (mrange f)
⊢ Eq (α := Submonoid N) (closure (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N))) (mrange f)
have rw₂ : Eq (α := Submonoid N) (map f (closure Set.univ)) (map f ⊤)
Tactic: rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]
-- 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
rw : Eq (α := Submonoid N) (closure (Set.image.{u_1, u_2} (α := M) (⇑f : (a : M) → N) Set.univ)) (mrange f)
rw₁ : Eq (α := Submonoid N) (map f (closure Set.univ)) (mrange f)
rw₂ : Eq (α := Submonoid N) (map f (closure Set.univ)) (map f ⊤)
⊢ Eq (α := Submonoid N) (closure (Set.range.{u_2, u_1 + 1} (ι := M) (⇑f : (a : M) → N))) (mrange f)
have rw₃ : Eq (α := Submonoid N) (map f ⊤) (map f ⊤)
Tactic: rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]
-- 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
S : Type u_5
inst_4 : SetLike S M
inst_5 : SubmonoidClass S M
M' : S
A : Type u_6
inst_6 : CommMonoid A
⊢ Eq (α := MonoidHom.{u_1, u_6} (↥M') A) (restrict 1 M') 1
have h : ∀ (x : ↥M'), Eq.{u_6 + 1} (α := A) ((restrict 1 M' : (a : ↥M') → A) x : A) ((1 : (a : ↥M') → A) x : A)
Tactic: ext
-- 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
S : Type u_5
inst_4 : SetLike S M
inst_5 : SubmonoidClass S M
M' : S
A : Type u_6
inst_6 : CommMonoid A
x x_1 : M →* A
⊢ (x * x_1).restrict M' = HMul.hMul (α := MonoidHom.{u_1, u_6} (↥M') A) (x.restrict M') (x_1.restrict M')
have h : ∀ (x_2 : ↥M'),
  Eq.{u_6 + 1} (α := A) (((x * x_1).restrict M' : (a : ↥M') → A) x_2 : A)
    ((HMul.hMul (α := MonoidHom.{u_1, u_6} (↥M') A) (x.restrict M') (x_1.restrict M') : (a : ↥M') → A) x_2 : A)
Tactic: ext
-- 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 : M →* N
⊢ Eq (α := Submonoid M) (mker f.mrangeRestrict) (mker f)
have h : ∀ (x : M), Membership.mem (γ := Submonoid M) (mker f.mrangeRestrict) x ↔ Membership.mem (γ := Submonoid M) (mker f) x
Tactic: ext x
-- 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 : M →* N
x : M
⊢ Membership.mem (γ := Submonoid M) (mker f.mrangeRestrict) x ↔ Membership.mem (γ := Submonoid M) (mker f) x
have h : Eq.{u_2 + 1} (α := ↥(mrange f))
    (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (mrange f) x) ((f : (a : M) → N) x) sorry :
      ↥(mrange f))
    (Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submonoid N) (mrange f) x) 1 sorry : ↥(mrange f)) ↔
  Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x : N) (1 : N)
Tactic: change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1
-- 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
⊢ Eq (α := Submonoid M) (mker (F := M →* N) 1) ⊤
have h : ∀ (x : M), Membership.mem (γ := Submonoid M) (mker (F := M →* N) 1) x ↔ Membership.mem (γ := Submonoid M) ⊤ x
Tactic: ext
-- 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
M' : Type u_5
N' : Type u_6
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* N
g : M' →* N'
⊢ Eq (α := Submonoid (M × M')) (mker (f.prodMap g)) (prod (mker f) (mker g))
have rw : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (mker f) (mker g))
Tactic: rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_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
M' : Type u_5
N' : Type u_6
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* N
g : M' →* N'
rw : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (mker f) (mker g))
⊢ Eq (α := Submonoid (M × M')) (mker (f.prodMap g)) (prod (mker f) (mker g))
have rw₁ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (mker g))
Tactic: rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_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
M' : Type u_5
N' : Type u_6
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* N
g : M' →* N'
rw : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (mker f) (mker g))
rw₁ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (mker g))
⊢ Eq (α := Submonoid (M × M')) (mker (f.prodMap g)) (prod (mker f) (mker g))
have rw₂ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (comap g ⊥))
Tactic: rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_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
M' : Type u_5
N' : Type u_6
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* N
g : M' →* N'
rw : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (mker f) (mker g))
rw₁ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (mker g))
rw₂ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (comap g ⊥))
⊢ Eq (α := Submonoid (M × M')) (mker (f.prodMap g)) (prod (mker f) (mker g))
have rw₃ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (comap (f.prodMap g) (prod ⊥ ⊥))
Tactic: rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_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
M' : Type u_5
N' : Type u_6
inst_2 : MulOneClass M'
inst_3 : MulOneClass N'
f : M →* N
g : M' →* N'
rw : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (mker f) (mker g))
rw₁ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (mker g))
rw₂ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (prod (comap f ⊥) (comap g ⊥))
rw₃ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (comap (f.prodMap g) (prod ⊥ ⊥))
⊢ Eq (α := Submonoid (M × M')) (mker (f.prodMap g)) (prod (mker f) (mker g))
have rw₄ : Eq (α := Submonoid (M × M')) (comap (f.prodMap g) ⊥) (comap (f.prodMap g) ⊥)
Tactic: rw [← comap_bot', ← comap_bot', ← comap_bot', ← prod_map_comap_prod', bot_prod_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
⊢ Eq (α := Submonoid M) (mker (F := M →* M × N) (inl M N)) ⊥
have h : ∀ (x : M),
  Membership.mem (γ := Submonoid M) (mker (F := M →* M × N) (inl M N)) x ↔ Membership.mem (γ := Submonoid M) ⊥ x
Tactic: ext x
-- 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
⊢ Eq (α := Submonoid N) (mker (F := N →* M × N) (inr M N)) ⊥
have h : ∀ (x : N),
  Membership.mem (γ := Submonoid N) (mker (F := N →* M × N) (inr M N)) x ↔ Membership.mem (γ := Submonoid N) ⊥ x
Tactic: ext x
-- 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 : M →* N
N' : Submonoid N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : ↥N'
⊢ ∃ (a : ↥(comap f N')), (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N') a = y
have obtain : ∀ (x : M) (hx : (f : (a : M) → N) x = (↑y : N)),
  ∃ (a : ↥(comap f N')), (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N') a = y
Tactic: obtain ⟨x, hx⟩ := hf y
-- 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 : M →* N
N' : Submonoid N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : ↥N'
x : M
hx : (f : (a : M) → N) x = (↑y : N)
⊢ ∃ (a : ↥(comap f N')), (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N') a = y
have h : (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N')
    (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (comap f N') x) x sorry) =
  y
Tactic: use ⟨x, mem_comap.mpr (hx ▸ y.2)⟩
-- 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 : M →* N
N' : Submonoid N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : ↥N'
x : M
hx : (f : (a : M) → N) x = (↑y : N)
⊢ (f.submonoidComap N' : (a : ↥(comap f N')) → ↥N')
      (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (comap f N') x) x ⋯) =
    y
have h : (↑((f.submonoidComap N' : (a : ↥(comap f N')) → ↥N')
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (comap f N') x) x sorry)) :
    N) =
  (↑y : N)
Tactic: apply Subtype.val_injective
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M : Type u_1
inst : MulOneClass M
S : Submonoid M
inst_1 : Subsingleton.{u_1 + 1} ↥S
⊢ S = ⊥
have rw : ∀ x ∈ S, x = 1
Tactic: rw [eq_bot_iff_forall]
-- 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
inst_3 : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Codisjoint H K
⊢ Codisjoint (α := Submonoid N) (map f H) (map f K)
have rw : Eq (α := Submonoid N) (map f H ⊔ map f K) ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]
-- 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
inst_3 : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Codisjoint H K
rw : Eq (α := Submonoid N) (map f H ⊔ map f K) ⊤
⊢ Codisjoint (α := Submonoid N) (map f H) (map f K)
have rw₁ : Eq (α := Submonoid N) (map f (H ⊔ K)) ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]
-- 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
inst_3 : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Codisjoint H K
rw : Eq (α := Submonoid N) (map f H ⊔ map f K) ⊤
rw₁ : Eq (α := Submonoid N) (map f (H ⊔ K)) ⊤
⊢ Codisjoint (α := Submonoid N) (map f H) (map f K)
have rw₂ : Eq (α := Submonoid N) (map f ⊤) ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]
-- 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
inst_3 : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Codisjoint 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 ⊤) ⊤
⊢ Codisjoint (α := Submonoid N) (map f H) (map f K)
have rw₃ : Eq (α := Submonoid N) (mrange f) ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]
-- 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
inst_3 : MonoidHomClass F M N
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
H K : Submonoid M
h : Codisjoint 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 ⊤) ⊤
rw₃ : Eq (α := Submonoid N) (mrange f) ⊤
⊢ Codisjoint (α := Submonoid N) (map f H) (map f K)
have rw₄ : Eq.{u_2 + 1} (α := Submonoid N) ⊤ ⊤
Tactic: rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
ι : Type u_4
M : ι → Type u_5
inst : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ pi (M := M) Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥
have simp_rw : (↑(pi (M := M) Set.univ S) : Set ((i : ι) → M i)) = (↑⊥ : Set ((i : ι) → M i)) ↔
  ∀ (i : ι), (↑(S i) : Set (M i)) = (↑⊥ : Set (M i))
Tactic: simp_rw [SetLike.ext'_iff]
-- 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 T : Submonoid M
f : M →* N
g : N → M
h : LeftInverse g (⇑f : (a : M) → N)
x : ↥(MonoidHom.mrange f)
x' : M
hx' : (f : (a : M) → N) x' = (↑x : N)
⊢ (f : (a : M) → N) (g (↑x : N)) = (↑x : N)
have rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (g ((f : (a : M) → N) x')) : N) ((f : (a : M) → N) x' : N)
Tactic: rw [← hx', h 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 T : Submonoid M
f : M →* N
g : N → M
h : LeftInverse g (⇑f : (a : M) → N)
x : ↥(MonoidHom.mrange f)
x' : M
hx' : (f : (a : M) → N) x' = (↑x : N)
rw : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) (g ((f : (a : M) → N) x')) : N) ((f : (a : M) → N) x' : N)
⊢ (f : (a : M) → N) (g (↑x : N)) = (↑x : N)
have rw₁ : Eq.{u_2 + 1} (α := N) ((f : (a : M) → N) x' : N) ((f : (a : M) → N) x' : N)
Tactic: rw [← hx', h x']
-- 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
S : Submonoid M
e : M ≃* N
⊢ S.equivMapOfInjective (↑e : M →* N) ⋯ = e.submonoidMap S
have h : ∀ (x : ↥S),
  Eq.{u_2 + 1} (α := N)
    (↑(((S.equivMapOfInjective (↑e : M →* N) sorry : MulEquiv.{u_1, u_2} ↥S ↥(map (F := M →* N) (↑e : M →* N) S)) :
            (a : ↥S) → ↥(map (↑e : M →* N) S))
          x) :
      N)
    (↑((e.submonoidMap S : (a : ↥S) → ↥(map (↑e : M →* N) S)) x) : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Operations (goal)
Goal:
M_1 : Type u_1
N : Type u_2
P : Type u_3
inst : MulOneClass M_1
inst_1 : MulOneClass N
inst_2 : MulOneClass P
S : Submonoid M_1
M : Type u_4
inst_3 : Monoid M
x y : Mˣ
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑(x * y) : M) ⋯ =
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑x : M) ⋯ *
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑y : M) ⋯
have simp_rw : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) ((↑x : M) * (↑y : M)) sorry =
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑x : M) sorry *
    Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submonoid M) (IsUnit.submonoid M) x) (↑y : M) sorry
Tactic: simp_rw [Units.val_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
S : Type u_6
inst : Monoid M
inst_1 : SetLike S M
inst_2 : SubmonoidClass S M
n : ℕ
h : n + 2 ≠ 0
H : S
⊢ (↑H : Set M) ^ (n + 2) = (↑H : Set M)
have rw : (↑H : Set M) ^ (n + 1) * (↑H : Set M) = (↑H : Set M)
Tactic: rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
S : Type u_6
inst : Monoid M
inst_1 : SetLike S M
inst_2 : SubmonoidClass S M
n : ℕ
h : n + 2 ≠ 0
H : S
rw : (↑H : Set M) ^ (n + 1) * (↑H : Set M) = (↑H : Set M)
⊢ (↑H : Set M) ^ (n + 2) = (↑H : Set M)
have rw₁ : (↑H : Set M) * (↑H : Set M) = (↑H : Set M)
Tactic: rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
S : Type u_6
inst : Monoid M
inst_1 : SetLike S M
inst_2 : SubmonoidClass S M
n : ℕ
h : n + 2 ≠ 0
H : S
rw : (↑H : Set M) ^ (n + 1) * (↑H : Set M) = (↑H : Set M)
rw₁ : (↑H : Set M) * (↑H : Set M) = (↑H : Set M)
⊢ (↑H : Set M) ^ (n + 2) = (↑H : Set M)
have rw₂ : (↑H : Set M) = (↑H : Set M)
Tactic: rw [pow_succ, coe_set_pow n.succ_ne_zero, coe_mul_coe]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
s : Set M
S : Submonoid M
n : ℕ
hs : s ⊆ (↑S : Set M)
⊢ s ^ n ⊆ (↑S : Set M)
have zero : HPow.hPow (β := ℕ) s 0 ⊆ (↑S : Set M)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
s : Set M
S : Submonoid M
n : ℕ
hs : s ⊆ (↑S : Set M)
zero : HPow.hPow (β := ℕ) s 0 ⊆ (↑S : Set M)
⊢ s ^ n ⊆ (↑S : Set M)
have succ : ∀ (n : ℕ), s ^ n ⊆ (↑S : Set M) → s ^ (n + 1) ⊆ (↑S : Set M)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
s : Set M
m n : ℕ
hmn : m ∣ n
⊢ LE.le (α := Submonoid M) (closure (s ^ n)) (closure (s ^ m))
have obtain : ∀ (k : ℕ), LE.le (α := Submonoid M) (closure (s ^ (m * k))) (closure (s ^ m))
Tactic: obtain ⟨k, rfl⟩ := hmn
Cleared hypotheses: n, hmn