mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) =
    !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ((curry
          ((curry
              (lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) ∘ₗ
                lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q))))
            x✝²))
        x✝¹)
      x✝ =
    ((curry ((curry LinearMap.id) x✝²)) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) ∘ₗ
                lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
⊢ y' = ∑ x, c x • M.subtype (b'M x)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
i : ι
x✝ : i ∈ Finset.univ
⊢ (b'M.coord i) ⟨y, ⋯⟩ • b'M i = (b'M.repr ⟨y, ⋯⟩) i • b'M i

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
r₃ : X
s₃ : ↥S
⊢ add'' (r₃, s₃).fst (r₃, s₃).snd (r₁, s₁).fst (r₁, s₁).snd = add'' (r₃, s₃).fst (r₃, s₃).snd (r₂, s₂).fst (r₂, s₂).snd

Tactic:
dsimp only at *

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
⊢ add'' r₃ s₃ r₁ s₁ = add'' r₃ s₃ r₂ s₂
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r r' : X
s s' : ↥S
⊢ r /ₒ s + r' /ₒ s' = (oreDenom (↑s) s' • r + oreNum (↑s) s' • r') /ₒ (oreDenom (↑s) s' * s)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (toLinearMapRight' M') ((toLinearMapRight' M) x) = x

Tactic:
by
      rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrix v₁ v₁) id = 1

Tactic:
by
  ext i j
  simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x✝ : OreLocalization S X
⊢ 0 • x✝ = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x✝¹ : ℕ
x✝ : OreLocalization S X
⊢ (x✝¹ + 1) • x✝ = x✝¹ • x✝ + x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
z : O
zM : z ∈ M
⊢ M.subtype ⟨z, zM⟩ + -(ϕ ⟨z, zM⟩ • M.subtype ⟨y', y'M⟩) = z + -(ϕ ⟨z, zM⟩ • y')

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
⊢ (toMatrix b' b) ↑(b'.equiv b (Equiv.refl l)) = 1

Tactic:
by
  ext i j
  simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₁
inst✝ : SMulCommClass G R M₁
g : G
f : M₁ →ₗ[R] M₂
⊢ (toMatrix (g • v₁) v₂) f = (toMatrix v₁ v₂) (f ∘ₗ DistribSMul.toLinearMap R M₁ g)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁹ : Fintype n
inst✝⁸ : Finite m
inst✝⁷ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
G : Type u_7
inst✝² : Group G
inst✝¹ : DistribMulAction G M₂
inst✝ : SMulCommClass G R M₂
g : G
f : M₁ →ₗ[R] M₂
⊢ (toMatrix v₁ (g • v₂)) f = (toMatrix v₁ v₂) (DistribSMul.toLinearMap R M₂ g⁻¹ ∘ₗ f)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Finite m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M₃ →ₗ[R] M₂
g : M₁ ≃ₗ[R] M₃
⊢ (toMatrix (v₁.map g) v₂) f = (toMatrix v₁ v₂) (f ∘ₗ ↑g)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Finite m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₃
g : M₂ ≃ₗ[R] M₃
⊢ (toMatrix v₁ (v₂.map g)) f = (toMatrix v₁ v₂) (↑g.symm ∘ₗ f)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : Field K
s : Set K
x : K
⊢ x ∈ commClosure s ↔ ∃ y ∈ Subring.closure s, ∃ z ∈ Subring.closure s, y / z = x

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) = -r /ₒ s

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
⊢ (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) (x * y)) = (toMatrix b b) ((lmul R S) x) * (toMatrix b b) ((lmul R S) y)

Tactic:
by
    rw [map_mul, LinearMap.toMatrix_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case pos
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
r : R
i✝ j✝ : ι
x✝ : M
h✝ : i✝ = j✝
⊢ r • x✝ = (r • LinearMap.id) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case neg
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
r : R
i✝ j✝ : ι
x✝ : M
h✝ : ¬i✝ = j✝
⊢ 0 = 0 x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
r : R
⊢ (endVecRingEquivMatrixEnd ι A M).toFun ((algebraMap R (End A (ι → M))) r) = (algebraMap R (Matrix ι ι (End A M))) r

Tactic:
by
    ext
    simp only [endVecRingEquivMatrixEnd, RingEquiv.toEquiv_eq_coe, Module.algebraMap_end_eq_smul_id,
      Equiv.toFun_as_coe, EquivLike.coe_coe, RingEquiv.coe_mk, Equiv.coe_fn_mk,
      LinearMap.smul_apply, id_coe, id_eq, Pi.smul_apply, Pi.single_apply, smul_ite, smul_zero,
      LinearMap.coe_mk, AddHom.coe_mk, algebraMap_matrix_apply]
    split_ifs <;> rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm ((algebraMap R S) r • s • x) = r • (addEquiv R S M).symm (s • x)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1.inr
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
j : ι
ne : j ≠ i
⊢ (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₂ * r₁)) j = (↑⟨update 0 i ↑s, ⋯⟩ * (↑s₁ * r₂)) j

Tactic:
simp [update_of_ne ne]

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ↑g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_6
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ (map W l hl) ((map Q g hy) x) = ((map W l hl).comp (map Q g hy)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case surj
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ (z : S), ∃ x, z * (algebraMap P S) ↑x.2 = (algebraMap P S) x.1

Tactic:
intro y
    obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M y
    refine ⟨⟨h x, _, _, s.prop, rfl⟩, ?_⟩
    dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply] at e ⊢
    convert! e <;> exact h.symm_apply_apply _

Goal state after: