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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x y z : R
h1 : x - y ∈ carrier
h2 : y - z ∈ carrier
⊢ x - z ∈ carrier

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x y z : R
h1 : x - y ∈ carrier
h2 : y - z ∈ carrier
⊢ x - y + (y - z) ∈ carrier
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I I' J' : TwoSidedIdeal R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } I' ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } J' ↔
    I' ≤ J'

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I I' J' : TwoSidedIdeal R
⊢ I'.ringCon.op ≤ J'.ringCon.op ↔ I'.ringCon ≤ J'.ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
h : ker f = ⊥
x y : R
hxy : f x = f y
⊢ x = y

Tactic:
simpa using

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
h : ker f = ⊥
x y : R
hxy : f x = f y
⊢ x = y
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ ker I.ringCon.mk'
⊢ x✝ ∈ I

Tactic:
simpa using

Goal state after:
R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ ker I.ringCon.mk'
⊢ x✝ ∈ I
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ I
⊢ x✝ - 0 ∈ I

Tactic:
simpa using

Goal state after:
R : Type u_4
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
x✝ : R
h : x✝ ∈ I
⊢ x✝ ∈ I
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: case h
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
d : R
hcd : ∀ (x : M), (c • LinearMap.id) x = (d • LinearMap.id) x
⊢ d = c

Tactic:
simpa using

Goal state after:
case h
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
d : R
hcd : ∀ (x : M), (c • LinearMap.id) x = (d • LinearMap.id) x
⊢ d = c
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
x : A
hx1 : x ∈ I
hx2 : x ≠ 0
⊢ 1 ∈ I

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
x : A
hx1 : x ∈ I
hx2 : x ≠ 0
⊢ 1 ∈ I
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_2
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
h : 1 ∈ I
x : R
x✝ : x ∈ ⊤
⊢ x ∈ I

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝ : NonAssocRing R
I : TwoSidedIdeal R
h : 1 ∈ I
x : R
x✝ : x ∈ ⊤
⊢ x ∈ I
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ ↑(Subalgebra.map f (iInf s)) = ↑(⨅ i, Subalgebra.map f (s i))

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ ⇑f '' ⋂ i, ↑(s i) = ⋂ i, ⇑f '' ↑(s i)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ Subalgebra.toSubmodule (Subalgebra.map f ⊥) = Subalgebra.toSubmodule ⊥

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ Submodule.map f.toLinearMap 1 = 1
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R B
h : S ≤ f.range
⊢ map f (comap f S) = S

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R B
h : S ≤ f.range
⊢ map f (comap f S) = S
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 1 ∈ s

Tactic:
simpa using

Goal state after:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 1 ∈ s
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 0 ∈ s

Tactic:
simpa using

Goal state after:
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
s : Set A
h :
  (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧
    (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s
⊢ 0 ∈ 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

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ T U : Subalgebra R A
h : S✝ ≤ T
α : Type u_1
β : Type u_2
inst✝ : IsDomain A
S : Subalgebra R A
r : ↥S
hr : IsRegular r
⊢ IsRegular ↑r

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S✝ T U : Subalgebra R A
h : S✝ ≤ T
α : Type u_1
β : Type u_2
inst✝ : IsDomain A
S : Subalgebra R A
r : ↥S
hr : IsRegular r
⊢ ¬r = 0
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) ↑i ∈ S.carrier
⊢ (algebraMap ℤ R) (↑i + 1) ∈ S.carrier

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) ↑i ∈ S.carrier
⊢ ↑i + 1 ∈ 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 : Set A
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * z ∈ span R ↑(Subsemigroup.closure s)
hyz : y * z ∈ span R ↑(Subsemigroup.closure s)
⊢ (x + y) * z ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
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
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * z ∈ span R ↑(Subsemigroup.closure s)
hyz : y * z ∈ span R ↑(Subsemigroup.closure s)
⊢ x * z + y * z ∈ span R ↑(Subsemigroup.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 : Set A
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * y ∈ span R ↑(Subsemigroup.closure s)
hyz : x * z ∈ span R ↑(Subsemigroup.closure s)
⊢ x * (y + z) ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
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
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * y ∈ span R ↑(Subsemigroup.closure s)
hyz : x * z ∈ span R ↑(Subsemigroup.closure s)
⊢ x * y + x * z ∈ span R ↑(Subsemigroup.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 : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ r • x * y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
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
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ r • (x * y) ∈ span R ↑(Subsemigroup.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
n : ℕ
⊢ R[↑n] = ⊥

Tactic:
simpa using

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
⊢ R[↑n] = ⊥
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 : Set A
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ x * r • y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
simpa using

Goal state after:
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
x✝³ x✝² y✝ : A
hx✝ : x✝² ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝² ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
r : R
x y : A
x✝¹ : x ∈ span R ↑(Subsemigroup.closure s)
x✝ : y ∈ span R ↑(Subsemigroup.closure s)
hxy : x * y ∈ span R ↑(Subsemigroup.closure s)
⊢ r • (x * y) ∈ span R ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: 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
ι : Sort u_2
inst✝² : Nonempty ι
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalSubalgebra R A
⊢ ↑(NonUnitalSubalgebra.map f (⨅ i, S i)) = ↑(⨅ i, NonUnitalSubalgebra.map f (S i))

Tactic:
simpa using

Goal state after:
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
ι : Sort u_2
inst✝² : Nonempty ι
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalSubalgebra R A
⊢ ⇑f '' ⋂ i, ↑(S i) = ⋂ i, ⇑f '' ↑(S i)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case add
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : f y ∈ adjoin R (⇑f '' (s ∪ {1}))
hz : f z ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f (y + z) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
simpa using

Goal state after:
case add
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : f y ∈ adjoin R (⇑f '' (s ∪ {1}))
hz : f z ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f y + f z ∈ adjoin R (⇑f '' insert 1 s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case mul
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : f y ∈ adjoin R (⇑f '' (s ∪ {1}))
hz : f z ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f (y * z) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
simpa using

Goal state after:
case mul
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : f y ∈ adjoin R (⇑f '' (s ∪ {1}))
hz : f z ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f y * f z ∈ adjoin R (⇑f '' insert 1 s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
n : ℤ
⊢ R[↑n] = ⊥

Tactic:
simpa using

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
n : ℤ
⊢ R[↑n] = ⊥
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
n : ℤ
s : Set A
⊢ adjoin R (insert (↑n) s) = adjoin R s

Tactic:
simpa using

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
n : ℤ
s : Set A
⊢ adjoin R (insert (↑n) s) = adjoin R s
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ S ⊔ adjoin R (⇑f ⁻¹' {0}) ≤ comap f (map f S)

Tactic:
rw [← map_le, Algebra.map_sup, f.map_adjoin]
    apply le_of_eq
    rw [sup_eq_left, Algebra.adjoin_le_iff]
    exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (S.map f).zero_mem)

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ b, (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = x

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ b, (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = x
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsLeftRegular x
a b : R
h : (fun x_1 ↦ x_1 * star x) a = (fun x_1 ↦ x_1 * star x) b
⊢ (fun x_1 ↦ x * x_1) (star a) = (fun x_1 ↦ x * x_1) (star b)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsLeftRegular x
a b : R
h : (fun x_1 ↦ x_1 * star x) a = (fun x_1 ↦ x_1 * star x) b
⊢ x * star a = x * star b
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsRightRegular x
a b : R
h : (fun x_1 ↦ star x * x_1) a = (fun x_1 ↦ star x * x_1) b
⊢ (fun x_1 ↦ x_1 * x) (star a) = (fun x_1 ↦ x_1 * x) (star b)

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsRightRegular x
a b : R
h : (fun x_1 ↦ star x * x_1) a = (fun x_1 ↦ star x * x_1) b
⊢ star a * x = star b * x
Module: Mathlib.Algebra.Star.BigOperators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
s : Finset ι
x : ι → R
h : ∀ i ∈ s, IsSelfAdjoint (x i)
⊢ IsSelfAdjoint (∑ i ∈ s, x i)

Tactic:
simpa using

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
s : Finset ι
x : ι → R
h : ∀ i ∈ s, IsSelfAdjoint (x i)
⊢ ∑ x_1 ∈ s, star (x x_1) = ∑ i ∈ s, x i
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y
Module: Mathlib.Algebra.Module.Rat

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module ℚ M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module ℚ M
n : ℕ
hn : n ≠ 0
x y : M
hxy : (fun a ↦ n • a) x = (fun a ↦ n • a) y
⊢ x = y
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝ : InvolutiveStar R
x : R
⊢ IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : InvolutiveStar R
x : R
⊢ x = star x ↔ star x = x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (x * star x)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint (x * star x)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : StarMul R
x : Rˣ
inst✝ : IsStarNormal ↑x
⊢ Commute (star ↑x⁻¹) ↑x⁻¹

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : StarMul R
x : Rˣ
inst✝ : IsStarNormal ↑x
⊢ Commute (star ↑x) ↑x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ b * a = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ b * a = 0
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
M : Matrix n n α
⊢ M = 1ᴴ ↔ M = 1

Tactic:
rw [conjTranspose_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝¹ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
x : M
x✝ : x ∈ ⊤
⊢ x ∈ span R (Set.range (Fin.cons y (⇑N.subtype ∘ ⇑b)))

Tactic:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x✝¹ y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
span_b : N = span R (Set.range (⇑N.subtype ∘ ⇑b))
x : M
x✝ : x ∈ ⊤
⊢ ∃ a, x + a • y ∈ span R (Set.range (Subtype.val ∘ ⇑b))