mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case e'_2
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ + x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)

pp: case e'_3
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ + x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)

Tactic:
<;>

Goal state after:
case e'_2
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ + x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)

case e'_3
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ + x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ + ⟨x✝², x✝⟩)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case e'_2
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ ⟨x✝³, x✝¹⟩ * φ₁ ⟨x✝², x✝⟩

pp: case e'_3
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³, x✝¹⟩ * φ₂ ⟨x✝², x✝⟩

Tactic:
<;>

Goal state after:
case e'_2
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ ⟨x✝³, x✝¹⟩ * φ₁ ⟨x✝², x✝⟩

case e'_3
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ ⟨x✝³, x✝¹⟩ * φ₂ ⟨x✝², x✝⟩
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case e'_2
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)

pp: case e'_3
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)

Tactic:
<;>

Goal state after:
case e'_2
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ * x✝², ⋯⟩ = φ₁ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)

case e'_3
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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₂ ⟨x✝³ * x✝², ⋯⟩ = φ₂ (⟨x✝³, x✝¹⟩ * ⟨x✝², x✝⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: case zero
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
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) 0) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) 0)

pp: case tmul
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
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ ⊗ₜ[R] y✝))

pp: case add
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
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisRight 𝒞) x✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisRight 𝒞) y✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) y✝)
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ + y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ + y✝))

Tactic:
<;>

Goal state after:
case zero
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
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) 0) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) 0)

case tmul
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
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ ⊗ₜ[R] y✝))

case add
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
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisRight 𝒞) x✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisRight 𝒞) y✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) y✝)
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ + y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ + y✝))
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) 0) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) 0)

pp: case tmul
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ ⊗ₜ[R] y✝))

pp: case add
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisLeft ℬ) x✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisLeft ℬ) y✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) y✝)
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ + y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ + y✝))

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) 0) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) 0)

case tmul
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ ⊗ₜ[R] y✝))

case add
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisLeft ℬ) x✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisLeft ℬ) y✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) y✝)
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ + y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ + y✝))
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n : M₂'
i : ι₁
⊢ ((directSumLeft R S M₁ M₂') (m ⊗ₜ[R] n)) i = m i ⊗ₜ[R] n

Tactic:
by
  suffices (DirectSum.component S ι₁ _ i) ∘ₗ (directSumLeft R S M₁ M₂').toLinearMap ∘ₗ
      ((AlgebraTensorModule.mk R S (⨁ i, M₁ i) M₂').flip n) =
        ((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n) ∘ₗ (DirectSum.component S ι₁ M₁ i) by
    simpa using! LinearMap.congr_fun this m
  ext j n
  by_cases hj : j = i
  · subst hj; simp
  · simp [DirectSum.component.of, hj]

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : i' = i
h✝ : k' = k
⊢ m ⊗ₜ[R] n = m ⊗ₜ[R] n

pp: case neg
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : i' = i
h✝ : ¬k' = k
⊢ 0 = m ⊗ₜ[R] 0

pp: case pos
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : ¬i' = i
h✝ : k' = k
⊢ 0 = 0 ⊗ₜ[R] n

pp: case neg
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : ¬i' = i
h✝ : ¬k' = k
⊢ 0 = 0 ⊗ₜ[R] 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : i' = i
h✝ : k' = k
⊢ m ⊗ₜ[R] n = m ⊗ₜ[R] n

case neg
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : i' = i
h✝ : ¬k' = k
⊢ 0 = m ⊗ₜ[R] 0

case pos
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : ¬i' = i
h✝ : k' = k
⊢ 0 = 0 ⊗ₜ[R] n

case neg
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h✝¹ : ¬i' = i
h✝ : ¬k' = k
⊢ 0 = 0 ⊗ₜ[R] 0
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (-x)

Tactic:
simp only [isSelfAdjoint_iff, star_neg, hx.star_eq]

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)

Tactic:
ha.eq,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: case hl.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).1 = ↑x

pp: case hl.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).2 = 0

pp: case hr.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).1 = 0

pp: case hr.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).2 = ↑x

Tactic:
<;>

Goal state after:
case hl.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).1 = ↑x

case hl.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(selfAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑x + ↑0)).2 = 0

case hr.fst
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).1 = 0

case hr.snd
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : ↥(skewAdjoint A)
⊢ ↑(((selfAdjointPart R).prod (skewAdjointPart R)) (↑0 + ↑x)).2 = ↑x
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : n
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝) j = M (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : o
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝) j = M (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : n
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝) j = M (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
j : l ⊕ m
val✝ : o
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝) j = M (Sum.inr val✝) j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inl val✝) =
    M (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inr val✝) =
    M (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inl val✝) =
    M (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inr val✝) =
    M (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inl val✝) =
    M (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inr val✝) =
    M (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inl val✝) =
    M (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inr val✝) =
    M (Sum.inr val✝¹) (Sum.inr val✝)
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : n
⊢ (fromBlocks A B C D).map f (Sum.inl val✝) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val✝) j

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : o
⊢ (fromBlocks A B C D).map f (Sum.inr val✝) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val✝) j

Tactic:
<;>

Goal state after:
case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : n
⊢ (fromBlocks A B C D).map f (Sum.inl val✝) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inl val✝) j

case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
β : Type u_13
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
j : l ⊕ m
val✝ : o
⊢ (fromBlocks A B C D).map f (Sum.inr val✝) j = fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) (Sum.inr val✝) j