mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: case inl
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
j : ι
x : ↥(A j)
⊢ ↑(((of (fun i ↦ ↥(A i)) j) x) j) = ↑(if j = j then x else 0)

pp: case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
·

Goal state after:
case inl
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
j : ι
x : ↥(A j)
⊢ ↑(((of (fun i ↦ ↥(A i)) j) x) j) = ↑(if j = j then x else 0)
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)

Tactic:
·

Goal state after:
case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ ↑(((of (fun i ↦ ↥(A i)) i) x) j) = ↑(if i = j then x else 0)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩

Goal state after:
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:
·

Goal state after:
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)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
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:
·

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)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
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:
·

Goal state after:
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)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case 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)
⊢ 0 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

pp: case 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 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
          y * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
            (x + y) * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

pp: case 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 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        a • x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
·

Goal state after:
case 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)
⊢ 0 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case 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 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
          y * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
            (x + y) * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

pp: case 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 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        a • x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
·

Goal state after:
case 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 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
          y * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
            (x + y) * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case 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 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        a • x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
·

Goal state after:
case 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 * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        a • x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
k : ι
⊢ k = i ∨ k = j

Tactic:
simpa using Set.ext_iff.mp h k

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case a
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ (adjoin R s).toSubmodule ≤ span R ↑(Subsemigroup.closure s)

pp: case a
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule

Tactic:
·

Goal state after:
case a
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ (adjoin R s).toSubmodule ≤ span R ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case refine_1
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
a : A
ha : a ∈ s
⊢ ⟨a, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
·

Goal state after:
case refine_1
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
a : A
ha : a ∈ s
⊢ ⟨a, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
·

Goal state after:
case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
·

Goal state after:
case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
·

Goal state after:
case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case a
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule

Tactic:
·

Goal state after:
case a
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
⊢ span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)

pp: case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ span R ↑(Submonoid.closure s) ≤ Subalgebra.toSubmodule (adjoin R s)

Tactic:
·

Goal state after:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Subalgebra.toSubmodule (adjoin R s) ≤ span R ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
z : ?m.153
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = hd.prod
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Tactic:
← hzr

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
z : ?m.153
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = hd.prod
⊢ z • r ∈ span R ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩

Goal state after: