Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_1.refine_2
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ x ∈ ↑(NonUnitalSubsemiring.closure s), x * 0 ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

pp: case refine_1.refine_3
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x y : A),
    x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
      y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        (∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
          (∀ x ∈ ↑(NonUnitalSubsemiring.closure s), x * y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
            ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s),
              x_1 * (x + y) ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

pp: case refine_1.refine_4
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s),
      (∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
        ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * a • x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
· exact fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _

Goal state after:
case refine_1.refine_3
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x y : A),
    x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
      y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        (∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
          (∀ x ∈ ↑(NonUnitalSubsemiring.closure s), x * y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
            ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s),
              x_1 * (x + y) ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

case refine_1.refine_4
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s),
      (∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
        ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * a • x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)