awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ LE.le (α := Submonoid M) (closure s) (closure (s ^ n))
have grw : LE.le (α := Submonoid M) (closure s) (closure s)
Tactic: grw [← subset_pow hs hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
H K : Submonoid M
⊢ closure (↑H : Set M) ⊔ closure (↑K : Set M) ≤ H ⊔ K
have rw : H ⊔ closure (↑K : Set M) ≤ H ⊔ K
Tactic: rw [closure_eq, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
H K : Submonoid M
rw : H ⊔ closure (↑K : Set M) ≤ H ⊔ K
⊢ closure (↑H : Set M) ⊔ closure (↑K : Set M) ≤ H ⊔ K
have rw₁ : H ⊔ K ≤ H ⊔ K
Tactic: rw [closure_eq, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
N : Type u_7
inst : CommMonoid N
H K : Submonoid N
⊢ (↑(H ⊔ K) : Set N) = (↑H : Set N) * (↑K : Set N)
have h : ∀ (x : N), x ∈ (↑(H ⊔ K) : Set N) ↔ x ∈ (↑H : Set N) * (↑K : Set N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x : N
hx : x ∈ s
⊢ (fun (x : N) ↦ r • x) x = HPow.hPow (β := ℕ) r 1 • x
have rw : (fun (x : N) ↦ r • x) x = r • x
Tactic: rw [pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))
have mul : ∀ (nx : ℕ) (hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)) (ny : ℕ)
  (hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)),
  ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))
Tactic: obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
nx : ℕ
hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)
ny : ℕ
hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))
have h : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ (ny + nx) • (x * y))
Tactic: use ny + nx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x_1 x y : N
hx_1 : Membership.mem (γ := Submonoid N) (closure s) x
hy_1 : Membership.mem (γ := Submonoid N) (closure s) y
hx_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
hy_2 : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)
nx : ℕ
hx : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ nx • x)
ny : ℕ
hy : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y)
⊢ Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ (ny + nx) • (x * y))
have h : Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ ny • y * r ^ nx • x)
Tactic: rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x : N
hx : Membership.mem (γ := Submonoid N) (closure s) x
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
have mem : ∀ (x : N) (hx : x ∈ s), ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
Tactic: induction hx using closure_induction with
  | mem x hx => exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
  | one => exact ⟨0, by simp⟩
  | mul x y _ _ hx hy =>
    obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
    use ny + nx
    rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
    exact mul_mem hy hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x : N
hx : Membership.mem (γ := Submonoid N) (closure s) x
mem : ∀ (x : N) (hx : x ∈ s), ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
have one : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (HSMul.hSMul (β := N) (r ^ n) 1)
Tactic: induction hx using closure_induction with
  | mem x hx => exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
  | one => exact ⟨0, by simp⟩
  | mul x y _ _ hx hy =>
    obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
    use ny + nx
    rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
    exact mul_mem hy hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
M : Type u_3
inst : Monoid M
N : Type u_7
inst_1 : CommMonoid N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
r : M
s : Set N
x : N
hx : Membership.mem (γ := Submonoid N) (closure s) x
mem : ∀ (x : N) (hx : x ∈ s), ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
one : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (HSMul.hSMul (β := N) (r ^ n) 1)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x)
have mul : ∀ (x y : N),
  Membership.mem (γ := Submonoid N) (closure s) x →
    Membership.mem (γ := Submonoid N) (closure s) y →
      ∀ (hx : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • x))
        (hy : ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • y)),
        ∃ (n : ℕ), Membership.mem (γ := Submonoid N) (closure (r • s)) (r ^ n • (x * y))
Tactic: induction hx using closure_induction with
  | mem x hx => exact ⟨1, subset_closure ⟨_, hx, by rw [pow_one]⟩⟩
  | one => exact ⟨0, by simp⟩
  | mul x y _ _ hx hy =>
    obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
    use ny + nx
    rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
    exact mul_mem hy hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
a b : G
ha : a ∈ (↑S : Set G)⁻¹
hb : b ∈ (↑S : Set G)⁻¹
⊢ a * b ∈ (↑S : Set G)⁻¹
have rw : b⁻¹ * a⁻¹ ∈ (↑S : Set G)
Tactic: rw [mem_inv, mul_inv_rev]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S_1 : Type u_6
inst : Monoid M
inst_1 : AddMonoid A
s t u : Set M
inst_2 : Group G
S : Submonoid G
⊢ 1⁻¹ ∈ (↑S : Set G)
have rw : 1 ∈ (↑S : Set G)
Tactic: rw [inv_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ Eq (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹
have a : LE.le (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
a : LE.le (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹
⊢ Eq (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹
have a₁ : LE.le (α := Submonoid G) (closure s)⁻¹ (closure s⁻¹)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ LE.le (α := Submonoid G) (closure s⁻¹) (closure s)⁻¹
have a : s ⊆ (↑(closure s) : Set G)
Tactic: rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
⊢ LE.le (α := Submonoid G) (closure s)⁻¹ (closure s⁻¹)
have a : s⁻¹ ⊆ (↑(closure s⁻¹) : Set G)
Tactic: rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
x : G
⊢ Membership.mem (γ := Submonoid G) (closure s⁻¹) x ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹
have rw : Membership.mem (γ := Submonoid G) (closure s)⁻¹ x ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹
Tactic: rw [closure_inv, mem_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
x : G
rw : Membership.mem (γ := Submonoid G) (closure s)⁻¹ x ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹
⊢ Membership.mem (γ := Submonoid G) (closure s⁻¹) x ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹
have rw₁ : Membership.mem (γ := Submonoid G) (closure s) x⁻¹ ↔ Membership.mem (γ := Submonoid G) (closure s) x⁻¹
Tactic: rw [closure_inv, mem_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (↑(Submonoid.closure s) : Set α).IsPWO
have rw : IsPWO.{u_1} (α := α) (List.prod '' {l : List α | ∀ x ∈ l, x ∈ s})
Tactic: rw [Submonoid.closure_eq_image_prod]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Pointwise (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ IsPWO.{u_1} (α := α) (List.prod '' {l : List α | ∀ x ∈ l, x ∈ s})
have refine : ∀ (a₁ : List α),
  Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₁ →
    ∀ (a₂ : List α),
      Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s} a₂ →
        List.SublistForall₂ (fun (x1 x2 : α) ↦ x1 ≤ x2) a₁ a₂ → a₁.prod ≤ a₂.prod
Tactic: refine (h.partiallyWellOrderedOn_sublistForall₂ (· ≤ ·)).image_of_monotone_on ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x x_1 : M
hxy : x * x_1 ∈ InfSet.sInf f
⊢ x ∈ InfSet.sInf f ∧ x_1 ∈ InfSet.sInf f
have simp_rw : ∀ (hxy : ∀ p ∈ f, x * x_1 ∈ p), (∀ p ∈ f, x ∈ p) ∧ ∀ p ∈ f, x_1 ∈ p
Tactic: simp_rw [mem_sInf] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
a b : M
hx : Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) a
hy : Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) b
⊢ Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) (a * b)
have rw : ∀ (hx : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), a ∈ (↑i : Set M))
  (hy : ∀ (i : SaturatedSubmonoid M) (j : i ∈ f), b ∈ (↑i : Set M)) (i : SaturatedSubmonoid M) (j : i ∈ f),
  a * b ∈ (↑i : Set M)
Tactic: rw [Set.mem_iInter₂] at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ Submonoid.MulSaturated.{u_1} (M := M) { carrier := ⋂ s ∈ f, (↑s : Set M), mul_mem' := ⋯, one_mem' := ⋯ }
have h : Eq.{u_1 + 1} (α := Set M) (⋂ s ∈ f, (↑s : Set M)) (Subsemigroup.carrier (sInf (toSubmonoid '' f)).1)
Tactic: convert! Submonoid.MulSaturated.sInf (f := toSubmonoid '' f) (by simp)
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : MulOneClass M
f : Set (SaturatedSubmonoid M)
⊢ Eq.{u_1 + 1} (α := Set M) (⋂ s ∈ f, (↑s : Set M)) (Subsemigroup.carrier (sInf (toSubmonoid '' f)).1)
have h : ∀ (x : M),
  Membership.mem (γ := Set M) (⋂ s ∈ f, (↑s : Set M)) x ↔
    Membership.mem (γ := Set M) (Subsemigroup.carrier (sInf (toSubmonoid '' f)).1) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ (y : M), x * y ∈ s
have refine : ∀ (h : x ∈ s.saturation), ∃ (y : M), x * y ∈ s
Tactic: refine ⟨fun h ↦ ?_, fun ⟨y, hxy⟩ ↦ (s.saturation.2 <| le_toSubmonoid_saturation hxy).1⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x_1 y : M
hx : x_1 ∈ s.saturation
hy : y ∈ s.saturation
ih₁ : ∃ (y : M), x_1 * y ∈ s
ih₂ : ∃ (y_1 : M), y * y_1 ∈ s
y₁ : M
h₁ : x_1 * y₁ ∈ s
y₂ : M
h₂ : y * y₂ ∈ s
⊢ x_1 * y * (y₁ * y₂) ∈ s
have rw : x_1 * y₁ * (y * y₂) ∈ s
Tactic: rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy : x₁ * x₂ ∈ s.saturation
ih : ∃ (y : M), x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₂ * (x₁ * y) ∈ s
have rwa : x₁ * (x₂ * y) ∈ s
Tactic: rwa [mul_left_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
h : x ∈ s.saturation
⊢ ∃ (y : M), x * y ∈ s
have mem : ∀ (x : M) (hx : x ∈ s), ∃ (y : M), x * y ∈ s
Tactic: induction h using saturation_induction with
  | mem _ hx => exact ⟨1, by simpa⟩
  | mul _ _ _ _ ih₁ ih₂ =>
    exact ih₁.elim fun y₁ h₁ ↦ ih₂.elim fun y₂ h₂ ↦
      ⟨y₁ * y₂, by rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂⟩
  | of_mul x₁ x₂ _ ih =>
    exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
h : x ∈ s.saturation
mem : ∀ (x : M) (hx : x ∈ s), ∃ (y : M), x * y ∈ s
⊢ ∃ (y : M), x * y ∈ s
have mul : ∀ (x y : M),
  x ∈ s.saturation →
    y ∈ s.saturation → ∀ (ih₁ : ∃ (y : M), x * y ∈ s) (ih₂ : ∃ (y_1 : M), y * y_1 ∈ s), ∃ (y_1 : M), x * y * y_1 ∈ s
Tactic: induction h using saturation_induction with
  | mem _ hx => exact ⟨1, by simpa⟩
  | mul _ _ _ _ ih₁ ih₂ =>
    exact ih₁.elim fun y₁ h₁ ↦ ih₂.elim fun y₂ h₂ ↦
      ⟨y₁ * y₂, by rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂⟩
  | of_mul x₁ x₂ _ ih =>
    exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
h : x ∈ s.saturation
mem : ∀ (x : M) (hx : x ∈ s), ∃ (y : M), x * y ∈ s
mul :
  ∀ (x y : M),
    x ∈ s.saturation →
      y ∈ s.saturation → ∀ (ih₁ : ∃ (y : M), x * y ∈ s) (ih₂ : ∃ (y_1 : M), y * y_1 ∈ s), ∃ (y_1 : M), x * y * y_1 ∈ s
⊢ ∃ (y : M), x * y ∈ s
have of_mul : ∀ (x₁ x₂ : M),
  x₁ * x₂ ∈ s.saturation → ∀ (ih : ∃ (y : M), x₁ * x₂ * y ∈ s), (∃ (y : M), x₁ * y ∈ s) ∧ ∃ (y : M), x₂ * y ∈ s
Tactic: induction h using saturation_induction with
  | mem _ hx => exact ⟨1, by simpa⟩
  | mul _ _ _ _ ih₁ ih₂ =>
    exact ih₁.elim fun y₁ h₁ ↦ ih₂.elim fun y₂ h₂ ↦
      ⟨y₁ * y₂, by rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂⟩
  | of_mul x₁ x₂ _ ih =>
    exact ih.elim fun y h ↦ ⟨⟨x₂ * y, by rwa [← mul_assoc]⟩,
      ⟨x₁ * y, by rwa [mul_left_comm, ← mul_assoc]⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ (y : M), y * x ∈ s
have simp_rw : (∃ (y : M), x * y ∈ s) ↔ ∃ (y : M), y * x ∈ s
Tactic: simp_rw [mem_saturation_iff, mul_comm x]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m
have simp_rw : x ∈ s.saturation ↔ ∃ m ∈ s, ∃ (c : M), m = x * c
Tactic: simp_rw [dvd_def, existsAndEq, and_true, mem_saturation_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
simp_rw : x ∈ s.saturation ↔ ∃ m ∈ s, ∃ (c : M), m = x * c
⊢ x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m
have simp_rw₁ : x ∈ s.saturation ↔ ∃ (c : M), x * c ∈ s ∧ True
Tactic: simp_rw [dvd_def, existsAndEq, and_true, mem_saturation_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
s : Submonoid M
x : M
simp_rw : x ∈ s.saturation ↔ ∃ m ∈ s, ∃ (c : M), m = x * c
simp_rw₁ : x ∈ s.saturation ↔ ∃ (c : M), x * c ∈ s ∧ True
⊢ x ∈ s.saturation ↔ ∃ m ∈ s, x ∣ m
have simp_rw₂ : x ∈ s.saturation ↔ ∃ (c : M), x * c ∈ s
Tactic: simp_rw [dvd_def, existsAndEq, and_true, mem_saturation_iff]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
⊢ Membership.mem (γ := SaturatedSubmonoid M) ⊥ x ↔ IsUnit x
have simp_rw : Membership.mem (γ := SaturatedSubmonoid M) (Submonoid.saturation ⊥) x ↔ IsUnit x
Tactic: simp_rw [bot_def, Submonoid.mem_saturation_iff, Submonoid.mem_bot, isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
simp_rw : Membership.mem (γ := SaturatedSubmonoid M) (Submonoid.saturation ⊥) x ↔ IsUnit x
⊢ Membership.mem (γ := SaturatedSubmonoid M) ⊥ x ↔ IsUnit x
have simp_rw₁ : (∃ (y : M), Membership.mem (γ := Submonoid M) ⊥ (x * y)) ↔ IsUnit x
Tactic: simp_rw [bot_def, Submonoid.mem_saturation_iff, Submonoid.mem_bot, isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Saturation (goal)
Goal:
M : Type u_1
inst : CommMonoid M
x : M
simp_rw : Membership.mem (γ := SaturatedSubmonoid M) (Submonoid.saturation ⊥) x ↔ IsUnit x
simp_rw₁ : (∃ (y : M), Membership.mem (γ := Submonoid M) ⊥ (x * y)) ↔ IsUnit x
⊢ Membership.mem (γ := SaturatedSubmonoid M) ⊥ x ↔ IsUnit x
have simp_rw₂ : (∃ (y : M), x * y = 1) ↔ IsUnit x
Tactic: simp_rw [bot_def, Submonoid.mem_saturation_iff, Submonoid.mem_bot, isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Support (hypothesis)
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
h : M.mulSupport = ⊥
x : G
⊢ x ∈ M → x⁻¹ ∈ M → x = 1
have h₁ : (x ∈ M.mulSupport) = Membership.mem (γ := Subgroup G) ⊥ x
Tactic: apply_fun (x ∈ ·) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Support (hypothesis)
Goal:
G : Type u_1
inst : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : M ≤ N
⊢ N ≤ M
have h₁ : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
Tactic: rw [SetLike.le_def] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gˣ
⊢ x ∈ H.units ↔ (↑x : G) ∈ H
have simp_rw : (↑x : G) ∈ H.toSubmonoid ∧ (↑x⁻¹ : G) ∈ H.toSubmonoid ↔ (↑x : G) ∈ H
Tactic: simp_rw [Submonoid.mem_units_iff, mem_toSubmonoid, val_inv_eq_inv_val, inv_mem_iff, and_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gˣ
simp_rw : (↑x : G) ∈ H.toSubmonoid ∧ (↑x⁻¹ : G) ∈ H.toSubmonoid ↔ (↑x : G) ∈ H
⊢ x ∈ H.units ↔ (↑x : G) ∈ H
have simp_rw₁ : (↑x : G) ∈ H ∧ (↑x⁻¹ : G) ∈ H ↔ (↑x : G) ∈ H
Tactic: simp_rw [Submonoid.mem_units_iff, mem_toSubmonoid, val_inv_eq_inv_val, inv_mem_iff, and_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gˣ
simp_rw : (↑x : G) ∈ H.toSubmonoid ∧ (↑x⁻¹ : G) ∈ H.toSubmonoid ↔ (↑x : G) ∈ H
simp_rw₁ : (↑x : G) ∈ H ∧ (↑x⁻¹ : G) ∈ H ↔ (↑x : G) ∈ H
⊢ x ∈ H.units ↔ (↑x : G) ∈ H
have simp_rw₂ : (↑x : G) ∈ H ∧ (↑x : G)⁻¹ ∈ H ↔ (↑x : G) ∈ H
Tactic: simp_rw [Submonoid.mem_units_iff, mem_toSubmonoid, val_inv_eq_inv_val, inv_mem_iff, and_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : Gˣ
simp_rw : (↑x : G) ∈ H.toSubmonoid ∧ (↑x⁻¹ : G) ∈ H.toSubmonoid ↔ (↑x : G) ∈ H
simp_rw₁ : (↑x : G) ∈ H ∧ (↑x⁻¹ : G) ∈ H ↔ (↑x : G) ∈ H
simp_rw₂ : (↑x : G) ∈ H ∧ (↑x : G)⁻¹ ∈ H ↔ (↑x : G) ∈ H
⊢ x ∈ H.units ↔ (↑x : G) ∈ H
have simp_rw₃ : (↑x : G) ∈ H ∧ (↑x : G) ∈ H ↔ (↑x : G) ∈ H
Tactic: simp_rw [Submonoid.mem_units_iff, mem_toSubmonoid, val_inv_eq_inv_val, inv_mem_iff, and_self]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gˣ
x : G
⊢ x ∈ H.ofUnits ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
have simp_rw : (∃ y ∈ H, (↑y : G) = x) ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
Tactic: simp_rw [mem_ofUnits_iff, toUnits.surjective.exists, val_toUnits_apply, exists_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gˣ
x : G
simp_rw : (∃ y ∈ H, (↑y : G) = x) ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
⊢ x ∈ H.ofUnits ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
have simp_rw₁ : (∃ (x_1 : G),
    Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x_1 : Gˣ) ∧ (↑((toUnits : (a : G) → Gˣ) x_1) : G) = x) ↔
  Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
Tactic: simp_rw [mem_ofUnits_iff, toUnits.surjective.exists, val_toUnits_apply, exists_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gˣ
x : G
simp_rw : (∃ y ∈ H, (↑y : G) = x) ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
simp_rw₁ :
  (∃ (x_1 : G),
      Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x_1 : Gˣ) ∧ (↑((toUnits : (a : G) → Gˣ) x_1) : G) = x) ↔
    Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
⊢ x ∈ H.ofUnits ↔ Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
have simp_rw₂ : (∃ (x_1 : G), Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x_1 : Gˣ) ∧ x_1 = x) ↔
  Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) x : Gˣ)
Tactic: simp_rw [mem_ofUnits_iff, toUnits.surjective.exists, val_toUnits_apply, exists_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
x : G
⊢ Membership.mem (α := Gˣ) H.units ((toUnits : (a : G) → Gˣ) x : Gˣ) ↔ x ∈ H
have simp_rw : (↑((toUnits : (a : G) → Gˣ) x) : G) ∈ H ↔ x ∈ H
Tactic: simp_rw [mem_units_iff_val_mem, val_toUnits_apply]
-- Lean 4 proof step from Mathlib.Algebra.Group.Submonoid.Units (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup Gˣ
x : Gˣ
⊢ (↑x : G) ∈ H.ofUnits ↔ x ∈ H
have simp_rw : Membership.mem (α := Gˣ) H ((toUnits : (a : G) → Gˣ) (↑x : G) : Gˣ) ↔ x ∈ H
Tactic: simp_rw [mem_ofUnits_iff_toUnits_mem, toUnits_val_apply]