awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
rw₂ :
  HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x * y)
have rw₃ : HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
x y : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
hy : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) y : B) ((ψ : (a : A) → B) y : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (x * y) : B) ((ψ : (a : A) → B) (x * y) : B)
rw₁ : HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) = (ψ : (a : A) → B) (x * y)
rw₂ :
  HMul.hMul (α := B) (β := B) ((ϕ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
rw₃ :
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ϕ : (a : A) → B) y : B) =
    HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (x * y)
have rw₄ : HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B) =
  HMul.hMul (α := B) (β := B) ((ψ : (a : A) → B) x : B) ((ψ : (a : A) → B) y : B)
Tactic: rw [Set.mem_setOf_eq, map_mul, map_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (r • x)
have rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (r • x) : B) ((ψ : (a : A) → B) (r • x) : B)
Tactic: rw [Set.mem_setOf_eq, map_smul, map_smul, hx]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (r • x) : B) ((ψ : (a : A) → B) (r • x) : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (r • x)
have rw₁ : HSMul.hSMul (β := B) r ((ϕ : (a : A) → B) x : B) = (ψ : (a : A) → B) (r • x)
Tactic: rw [Set.mem_setOf_eq, map_smul, map_smul, hx]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (r • x) : B) ((ψ : (a : A) → B) (r • x) : B)
rw₁ : HSMul.hSMul (β := B) r ((ϕ : (a : A) → B) x : B) = (ψ : (a : A) → B) (r • x)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (r • x)
have rw₂ : HSMul.hSMul (β := B) r ((ϕ : (a : A) → B) x : B) = HSMul.hSMul (β := B) r ((ψ : (a : A) → B) x : B)
Tactic: rw [Set.mem_setOf_eq, map_smul, map_smul, hx]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : NonUnitalNonAssocSemiring C
inst_6 : Module R C
inst_7 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
ϕ ψ : F
r : R
x : A
hx : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) x : B) ((ψ : (a : A) → B) x : B)
rw : Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) (r • x) : B) ((ψ : (a : A) → B) (r • x) : B)
rw₁ : HSMul.hSMul (β := B) r ((ϕ : (a : A) → B) x : B) = (ψ : (a : A) → B) (r • x)
rw₂ : HSMul.hSMul (β := B) r ((ϕ : (a : A) → B) x : B) = HSMul.hSMul (β := B) r ((ψ : (a : A) → B) x : B)
⊢ Membership.mem (γ := Set A) {a : A | Eq.{w + 1} (α := B) ((ϕ : (a : A) → B) a : B) ((ψ : (a : A) → B) a : B)} (r • x)
have rw₃ : HSMul.hSMul (β := B) r ((ψ : (a : A) → B) x : B) = HSMul.hSMul (β := B) r ((ψ : (a : A) → B) x : B)
Tactic: rw [Set.mem_setOf_eq, map_smul, map_smul, hx]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a * b)
have refine_1 : ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
  Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ ha
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a * b)
have refine_2 : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (0 * b)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ ha
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
refine_2 : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (0 * b)
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a * b)
have refine_3 : ∀ (x y : A) (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
  (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
  Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (y * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) ((x + y) * b)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ ha
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
refine_2 : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (0 * b)
refine_3 :
  ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (y * b) →
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) ((x + y) * b)
⊢ Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a * b)
have refine_4 : ∀ (a : R) (x : A)
  (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
  Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b) →
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (a • x * b)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ ha
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
have refine_1 : ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 : A)
  (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
  Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 : A)
    (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
have refine_1₁ : ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
  Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * 0)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 : A)
    (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)
refine_1₁ :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * 0)
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
have refine_1₂ : ∀ (x y : A) (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
  (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
  (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
    (∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * y)) →
      ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A))
          (x_1 * (x + y))
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hb
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : NonUnitalNonAssocSemiring B
inst_4 : Module R B
inst_5 : FunLike F A B
inst_6 : NonUnitalAlgHomClass F R A B
inst_7 : IsScalarTower R A A
inst_8 : SMulCommClass R A A
s : Set A
a b : A
ha : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) a
hb : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) b
refine_1 :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 : A)
    (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)
refine_1₁ :
  ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * 0)
refine_1₂ :
  ∀ (x y : A)
    (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x)
    (hy : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) y),
    (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
        Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
      (∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * y)) →
        ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
          Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A))
            (x_1 * (x + y))
⊢ ∀ (x : A) (h : x ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
    Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x * b)
have refine_1₃ : ∀ (a : R) (x : A)
  (hx : Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) x),
  (∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * x)) →
    ∀ (x_1 : A) (h : x_1 ∈ (↑(NonUnitalSubsemiring.closure s) : Set A)),
      Membership.mem (γ := Submodule R A) (Submodule.span R (↑(NonUnitalSubsemiring.closure s) : Set A)) (x_1 * a • x)
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ hb
-- 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
⊢ p x z hx ⋯
have mem : ∀ (x : A) (h : x ∈ s), p x 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