awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
z : R
hz : z ∈ s
mem : ∀ (x : R) (h : x ∈ s), p x z ⋯ ⋯
⊢ p x z hx ⋯
have mem₁ : p 0 z sorry sorry
Tactic: induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
z : R
hz : z ∈ s
mem : ∀ (x : R) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : p 0 z ⋯ ⋯
⊢ p x z hx ⋯
have mem₂ : ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
  (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y) (h₁ : p x z hx sorry) (h₂ : p y z hy sorry), p (x * y) z sorry sorry
Tactic: induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
z : R
hz : z ∈ s
mem : ∀ (x : R) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : p 0 z ⋯ ⋯
mem₂ :
  ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y) (h₁ : p x z hx ⋯) (h₂ : p y z hy ⋯),
    p (x * y) z ⋯ ⋯
⊢ p x z hx ⋯
have mem₃ : ∀ (x y : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
  (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y) (h₁ : p x z hx sorry) (h₂ : p y z hy sorry), p (x + y) z sorry sorry
Tactic: induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y
⊢ p x y hx hy
have mem : ∀ (z : R) (hz : z ∈ s), p x z hx sorry
Tactic: induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y
mem : ∀ (z : R) (hz : z ∈ s), p x z hx ⋯
⊢ p x y hx hy
have zero : p x 0 hx sorry
Tactic: induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y
mem : ∀ (z : R) (hz : z ∈ s), p x z hx ⋯
zero : p x 0 hx ⋯
⊢ p x y hx hy
have mul : ∀ (x_1 y : R) (hx_1 : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x_1)
  (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
  p x (x_1 * y) hx sorry
Tactic: induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
p :
  (x y : R) →
    Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x →
      Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y)
    (hz : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x
hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y
mem : ∀ (z : R) (hz : z ∈ s), p x z hx ⋯
zero : p x 0 hx ⋯
mul :
  ∀ (x_1 y : R) (hx_1 : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x_1)
    (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
    p x (x_1 * y) hx ⋯
⊢ p x y hx hy
have add : ∀ (x_1 y : R) (hx_1 : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) x_1)
  (hy : Membership.mem (γ := NonUnitalSubsemiring R) (closure s) y) (h₁ : p x x_1 hx hx_1) (h₂ : p x y hx hy),
  p x (x_1 + y) hx sorry
Tactic: induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
ι : Sort u_2
inst_4 : Nonempty ι
f : F
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
s : ι → NonUnitalSubsemiring R
⊢ Eq (α := NonUnitalSubsemiring S) (map f (iInf s)) (⨅ (i : ι), map f (s i))
have a : (↑(map f (iInf s)) : Set S) = (↑(⨅ (i : ι), map f (s i)) : Set S)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i
have refine : Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
Tactic: refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
U : NonUnitalSubsemiring R :=
  NonUnitalSubsemiring.mk' (⋃ (i : ι), (↑(S i) : Set R)) (⨆ (i : ι), (S i).toSubsemigroup) ⋯
    (⨆ (i : ι), (S i).toAddSubmonoid) ⋯
⊢ Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) x → ∃ (i : ι), x ∈ S i
have suffices : ⨆ (i : ι), S i ≤ U
Tactic: suffices ⨆ i, S i ≤ U by simpa [U] using @this x
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (hypothesis)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
have this : Nonempty.{u + 1} (↑S : Type u)
Tactic: haveI : Nonempty S := Sne.to_subtype
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u} ↥(⨆ (i : ι), S i)
have refine : ∀ (a : R),
  Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) a →
    ∀ (b : R), Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) b → a * b = b * a
Tactic: refine .of_setLike_mul_comm ?_
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
⊢ ∀ (a : R),
    Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) a →
      ∀ (b : R), Membership.mem (γ := NonUnitalSubsemiring R) (⨆ (i : ι), S i) b → a * b = b * a
have simp_rw : ∀ (a : R) (x : ι) (h : a ∈ S x) (b : R) (x : ι) (h : b ∈ S x), a * b = b * a
Tactic: simp_rw [← SetLike.mem_coe, coe_iSup_of_directed dir, Set.mem_iUnion,
    SetLike.mem_coe, forall_exists_index]
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst_1 : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative.{u} ↥(S i)
dir : Directed (fun (x1 x2 : NonUnitalSubsemiring R) ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
b : R
j : ι
hb : b ∈ S j
⊢ a * b = b * a
have obtain : ∀ (k : ι) (hik : S i ≤ S k) (hjk : S j ≤ S k), a * b = b * a
Tactic: obtain ⟨k, hik, hjk⟩ := dir i j
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ (↑(srange f) : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
have rw : Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S) = (↑⊤ : Set S) ↔
  Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
Tactic: rw [coe_srange, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
F : Type u_1
inst_1 : FunLike F R S
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalRingHomClass F R S
f : F
rw :
  Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
⊢ (↑(srange f) : Set S) = (↑⊤ : Set S) ↔
    Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
have rw₁ : Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ ↔
  Eq.{v + 1} (α := Set S) (Set.range.{v, u + 1} (ι := R) (⇑f : (a : R) → S)) Set.univ
Tactic: rw [coe_srange, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s t : NonUnitalSubsemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥(srange f)
x' : R
hx' : (f : (a : R) → S) x' = (↑x : S)
⊢ (f : (a : R) → S) (g (↑x : S)) = (↑x : S)
have rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g ((f : (a : R) → S) x')) : S) ((f : (a : R) → S) x' : S)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Basic (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s t : NonUnitalSubsemiring R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_1
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g (⇑f : (a : R) → S)
x : ↥(srange f)
x' : R
hx' : (f : (a : R) → S) x' = (↑x : S)
rw : Eq.{v + 1} (α := S) ((f : (a : R) → S) (g ((f : (a : R) → S) x')) : S) ((f : (a : R) → S) x' : S)
⊢ (f : (a : R) → S) (g (↑x : S)) = (↑x : S)
have rw₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x' : S)
Tactic: rw [← hx', h x']
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Defs (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : (↑sg : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s
have subst : ∀ (hg : (↑sg : Set R) = (↑sa : Set R)) {a b : R}, a ∈ (↑sa : Set R) → b ∈ (↑sa : Set R) → a + b ∈ (↑sa : Set R)
Tactic: subst ha
Cleared hypotheses: s, hg, ha
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Defs (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : (↑sg : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ 0 ∈ s
have subst : ∀ (hg : (↑sg : Set R) = (↑sa : Set R)), 0 ∈ (↑sa : Set R)
Tactic: subst ha
Cleared hypotheses: s, hg, ha