mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ Pi.single j x ᵥ* diagonal v = Pi.single j (x * v j)

Tactic:
ext i

Goal state after:
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
i : n
⊢ (Pi.single j x ᵥ* diagonal v) i = Pi.single j (x * v j) i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
u v : m → α
w : n → α
⊢ u ᵥ* vecMulVec v w = (u ⬝ᵥ v) • w

Tactic:
ext i

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
u v : m → α
w : n → α
i : n
⊢ (u ᵥ* vecMulVec v w) i = ((u ⬝ᵥ v) • w) i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
u : m → α
v w : n → α
⊢ vecMulVec u v *ᵥ w = MulOpposite.op (v ⬝ᵥ w) • u

Tactic:
ext i

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype n
u : m → α
v w : n → α
i : m
⊢ (vecMulVec u v *ᵥ w) i = (MulOpposite.op (v ⬝ᵥ w) • u) i
Module: Mathlib.LinearAlgebra.Matrix.StdBasis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
m : Type u_4
n : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
i : m
j : n
k : ι
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ (Basis.matrix m n b) (i, j, k) = Matrix.single i j (b k)

Tactic:
by
  simp [Basis.matrix, Matrix.single_eq_of_single_single]

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
i : m
j : n
h : ∀ (i : n), M.col i = N.col i
⊢ M i j = N i j

Tactic:
exact congrFun (h j) i

Goal state after:
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
⊢ ∑ i, (of β i) (x i) = x

Tactic:
ext i

Goal state after:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : ⨁ (i : ι), β i
i : ι
⊢ (∑ i, (of β i) (x i)) i = x i
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ (fromAddMonoid ((of (fun i ↦ γ →+ β i) i) f)) x = (of β i) (f x)

Tactic:
by
      rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]

Goal state after:
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
ι : Sort u_1
S : ι → Subalgebra R A
⊢ (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring

Tactic:
simp only [iInf, sInf_toSubsemiring, ← Set.range_comp, Function.comp_def]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_1
inst✝² : DecidableEq ι
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ε : M →ₗ[R] N
m : ι →₀ M
⊢ (lmap fun x ↦ ε) ((finsuppLEquivDirectSum R M ι) m) = (finsuppLEquivDirectSum R N ι) (Finsupp.mapRange ⇑ε ⋯ m)

Tactic:
ext i

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_1
inst✝² : DecidableEq ι
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ε : M →ₗ[R] N
m : ι →₀ M
i : ι
⊢ ((lmap fun x ↦ ε) ((finsuppLEquivDirectSum R M ι) m)) i = ((finsuppLEquivDirectSum R N ι) (Finsupp.mapRange ⇑ε ⋯ m)) i
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: 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✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT) ((inclusion h) x) = (f i) x

Tactic:
subst T
  dsimp [iSupLift]
  apply Set.iUnionLift_inclusion
  exact h

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ leftComm R M N P =
    (TensorProduct.assoc R M N P).symm ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
      TensorProduct.assoc R N M P

Tactic:
by
  apply LinearEquiv.toLinearMap_injective; ext; rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
⊢ rightComm R M N P =
    TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
      (TensorProduct.assoc R M P N).symm

Tactic:
by
  apply LinearEquiv.toLinearMap_injective; ext; rfl

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

Goal state before:
pp: R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A'
inst✝⁴ : AddCommMonoid B'
inst✝³ : AddCommMonoid C'
inst✝² : Module R A'
inst✝¹ : Module R B'
inst✝ : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
x : A ⊗[R] B ⊗[R] C
⊢ (TensorProduct.assoc R A B C) x =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      x

Tactic:
induction x with

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
⊢ (finsuppScalarLeft R N ι) (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m • n)

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = (p.sum fun i m ↦ Finsupp.single i (m • n)) i
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v : N
⊢ mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (r • v)))) =
    (RingHom.id S) r • mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm v)))

Tactic:
ext i

Goal state after:
R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
r : S
v i : N
⊢ (mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (r • v))))) i =
    ((RingHom.id S) r • mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm v)))) i
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

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✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
⊢ (finsuppScalarRight R S M ι) (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (n • m)

Tactic:
ext i

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : Algebra R S
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ ((finsuppScalarRight R S M ι) (m ⊗ₜ[R] p)) i = (p.sum fun i n ↦ Finsupp.single i (n • m)) i
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
x✝ : M
a✝ : N
⊢ ((AlgebraTensorModule.curry
            (AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id))
          x✝ ∘ₗ
        lsingle a✝)
      1 =
    ((AlgebraTensorModule.curry LinearMap.id) x✝ ∘ₗ lsingle a✝) 1

Tactic:
simp [hsM _]

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

Goal state before:
pp: R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(b.mkFinSnoc y hli hsp) = Fin.snoc (Subtype.val ∘ ⇑b) y

Tactic:
by
  unfold mkFinSnoc
  exact coe_mk (v := Fin.snoc (N.subtype ∘ b) y) _ _

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ b.repr ((b.prod b') (Sum.inr i)).1 = b.repr 0

Tactic:
ext i

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ : ι'
i : ι
⊢ (b.repr ((b.prod b') (Sum.inr i✝)).1) i = (b.repr 0) i
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ b'.repr ((b.prod b') (Sum.inr i)).2 = b'.repr (b' i)

Tactic:
ext i

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ i : ι'
⊢ (b'.repr ((b.prod b') (Sum.inr i✝)).2) i = (b'.repr (b' i✝)) i
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i

Tactic:
ext <;> cases i <;>
    simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
      Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
⊢ fromBlocks A B C D *ᵥ x = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr)

Tactic:
ext i

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
i : n ⊕ o
⊢ (fromBlocks A B C D *ᵥ x) i = Sum.elim (A *ᵥ x ∘ Sum.inl + B *ᵥ x ∘ Sum.inr) (C *ᵥ x ∘ Sum.inl + D *ᵥ x ∘ Sum.inr) i
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
⊢ x ᵥ* fromBlocks A B C D = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D)

Tactic:
ext i

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
i : l ⊕ m
⊢ (x ᵥ* fromBlocks A B C D) i = Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) i
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
⊢ vecCons x v ᵥ* of B = x • vecHead B + v ᵥ* of (vecTail B)

Tactic:
ext i

Goal state after:
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin n.succ → o' → α
i : o'
⊢ (vecCons x v ᵥ* of B) i = (x • vecHead B + v ᵥ* of (vecTail B)) i
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
⊢ v ᵥ* of (vecCons w B) = vecHead v • w + vecTail v ᵥ* of B

Tactic:
ext i

Goal state after:
α : Type u
n : ℕ
o' : Type uₒ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin n.succ → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ (v ᵥ* of (vecCons w B)) i = (vecHead v • w + vecTail v ᵥ* of B) i
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
⊢ of (vecCons v A) *ᵥ w = vecCons (v ⬝ᵥ w) (of A *ᵥ w)

Tactic:
ext i

Goal state after:
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ (of (vecCons v A) *ᵥ w) i = vecCons (v ⬝ᵥ w) (of A *ᵥ w) i
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
⊢ of A *ᵥ vecCons x v = x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v

Tactic:
ext i

Goal state after:
n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
i : m'
⊢ (of A *ᵥ vecCons x v) i = (x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v) i
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)

Tactic:
ext i

Goal state after:
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ vecMulVec (vecCons x v) w i j✝ = vecCons (x • w) (vecMulVec v w) i j✝
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
⊢ a ∈ closure ↑?m.238

Tactic:
hSgen

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
⊢ a ∈ ⊤
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
⊢ b ∈ closure ↑?m.266

Tactic:
hSgen

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
⊢ b ∈ ⊤
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
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
⊢ add' (r₁, s₁).fst (r₁, s₁).snd x = add' (r₂, s₂).fst (r₂, s₂).snd x

Tactic:
induction x with

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₂, 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₃) = add' (r₂, s₂).fst (r₂, s₂).snd (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
x y z : OreLocalization S X
⊢ x + y + z = x + (y + z)

Tactic:
induction x with

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
y z : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)
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
f : (m → R) →ₗ[R] n → R
j : m
⊢ (vecMulLinear ((fun f i j ↦ f ((single R (fun x ↦ R) i) 1) j) f)) ((Pi.basisFun R m) j) = f ((Pi.basisFun R m) j)

Tactic:
ext i

Goal state after:
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
f : (m → R) →ₗ[R] n → R
j : m
i : n
⊢ (vecMulLinear ((fun f i j ↦ f ((single R (fun x ↦ R) i) 1) j) f)) ((Pi.basisFun R m) j) i = f ((Pi.basisFun R m) j) i
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
y z : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ r₁ /ₒ s₁ + y + z = r₁ /ₒ s₁ + (y + z)

Tactic:
induction y with | _ r₂ s₂
   =>  _ 

Goal state after:
case c.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
z : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
j : n
⊢ ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin ((Pi.basisFun R n) j) = f ((Pi.basisFun R n) j)

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
f : (n → R) →ₗ[R] m → R
j : n
i : m
⊢ ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin ((Pi.basisFun R n) j) i = f ((Pi.basisFun R n) j) i
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case zero
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ toLin' (M ^ 0) = toLin' M ^ 0

Tactic:
simp [End.one_eq_id]

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₂
f : M₁ →ₗ[R] M₂
x : M₁
⊢ (toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x) = ⇑(v₂.repr (f x))

Tactic:
ext i

Goal state after:
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₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ((toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x)) i = (v₂.repr (f x)) i
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 R
⊢ x • 0 = 0

Tactic:
induction x with

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 : R
s : ↥S
⊢ (r /ₒ s) • 0 = 0
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
z : OreLocalization S R
x y : OreLocalization S X
⊢ z • (x + y) = z • x + z • y

Tactic:
induction x with

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
z : OreLocalization S R
y : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ z • (r₁ /ₒ s₁ + y) = z • (r₁ /ₒ s₁) + z • y
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
z : OreLocalization S R
y : OreLocalization S X
r₁ : X
s₁ : ↥S
⊢ z • (r₁ /ₒ s₁ + y) = z • (r₁ /ₒ s₁) + z • y

Tactic:
induction y with | _ r₂ s₂
   =>  _ 

Goal state after:
case c.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
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ z • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = z • (r₁ /ₒ s₁) + z • (r₂ /ₒ s₂)