awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
mem : ∀ (x : A) (h : x ∈ s), p x z ⋯ ⋯
⊢ p x z hx ⋯
have mem₁ : p 0 z sorry sorry
Tactic: induction hx using adjoin_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₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
mem : ∀ (x : A) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : p 0 z ⋯ ⋯
⊢ p x z hx ⋯
have mem₂ : ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
  (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y) (h₁ : p x z hx sorry) (h₂ : p y z hy sorry),
  p (x * y) z sorry sorry
Tactic: induction hx using adjoin_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₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
z : A
hz : z ∈ s
mem : ∀ (x : A) (h : x ∈ s), p x z ⋯ ⋯
mem₁ : p 0 z ⋯ ⋯
mem₂ :
  ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y) (h₁ : p x z hx ⋯) (h₂ : p y z hy ⋯),
    p (x * y) z ⋯ ⋯
⊢ p x z hx ⋯
have mem₃ : ∀ (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
  (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y) (h₁ : p x z hx sorry) (h₂ : p y z hy sorry),
  p (x + y) z sorry sorry
Tactic: induction hx using adjoin_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₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
⊢ p x y hx hy
have mem : ∀ (z : A) (hz : z ∈ s), p x z hx sorry
Tactic: induction hy using adjoin_induction with
  | mem z hz =>
    induction hx using adjoin_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₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | smul _ _ _ h => exact smul_right _ _ _ _ _ h
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p 0 x ⋯ hx
zero_right : ∀ (x : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x), p x 0 hx ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
smul_left :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p (r • x) y ⋯ hy
smul_right :
  ∀ (r : R) (x y : A) (hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (r • y) hx ⋯
x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
mem : ∀ (z : A) (hz : z ∈ s), p x z hx ⋯
⊢ p x y hx hy
have zero : p x 0 hx sorry
Tactic: induction hy using adjoin_induction with
  | mem z hz =>
    induction hx using adjoin_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₂
    | smul _ _ _ h => exact smul_left _ _ _ _ _ h
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | smul _ _ _ h => exact smul_right _ _ _ _ _ h
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
⊢ Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) (span R (↑(Subsemigroup.closure s) : Set A))
have a : LE.le (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) (span R (↑(Subsemigroup.closure s) : Set A))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
a :
  LE.le (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) (span R (↑(Subsemigroup.closure s) : Set A))
⊢ Eq (α := Submodule R A) (NonUnitalSubalgebra.toSubmodule (adjoin R s)) (span R (↑(Subsemigroup.closure s) : Set A))
have a₁ : LE.le (α := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (NonUnitalSubalgebra.toSubmodule (adjoin R s))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
have apply : ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
  Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
Tactic: apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
apply :
  ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
have apply₁ : ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
  (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
  (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
  Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)
Tactic: apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
apply :
  ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
apply₁ :
  ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
have apply₂ : ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
  (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
  (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
  Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * (y + z))
Tactic: apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
x_1 x y : A
hx : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) x
hy : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) y
hpx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x
hpy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y
apply :
  ∀ (x y : A) (hx : x ∈ (↑(Subsemigroup.closure s) : Set A)) (hy : y ∈ (↑(Subsemigroup.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
apply₁ :
  ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (y * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) ((x + y) * z)
apply₂ :
  ∀ (x y z : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y)
    (hz : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) z),
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
      Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * z) →
        Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * (y + z))
⊢ Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y)
have apply₃ : ∀ (r : R) (x y : A) (hx : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) x)
  (hy : Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) y),
  Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (x * y) →
    Membership.mem (γ := Submodule R A) (span R (↑(Subsemigroup.closure s) : Set A)) (r • x * y)
Tactic: apply span_induction₂ ?Hs (by simp) (by simp) ?Hadd_l ?Hadd_r ?Hsmul_l ?Hsmul_r hpx hpy