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

Goal state before:
pp: case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (∑ i ∈ Finset.range 2, if h : i < 2 then A 0 ⟨i, h⟩ * B ⟨i, h⟩ 1 else 0) = A 0 0 * B 0 1 + A 0 1 * B 1 1

Tactic:
Finset.sum_range_succ,

Goal state after:
case refine_2
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ ((∑ x ∈ Finset.range 1, if h : x < 2 then A 0 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
      if h : 1 < 2 then A 0 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 0 0 * B 0 1 + A 0 1 * B 1 1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_3
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (∑ i ∈ Finset.range 2, if h : i < 2 then A 1 ⟨i, h⟩ * B ⟨i, h⟩ 0 else 0) = A 1 0 * B 0 0 + A 1 1 * B 1 0

Tactic:
Finset.sum_range_succ,

Goal state after:
case refine_3
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ ((∑ x ∈ Finset.range 1, if h : x < 2 then A 1 ⟨x, h⟩ * B ⟨x, h⟩ 0 else 0) +
      if h : 1 < 2 then A 1 ⟨1, h⟩ * B ⟨1, h⟩ 0 else 0) =
    A 1 0 * B 0 0 + A 1 1 * B 1 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case refine_4
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (∑ i ∈ Finset.range 2, if h : i < 2 then A 1 ⟨i, h⟩ * B ⟨i, h⟩ 1 else 0) = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
Finset.sum_range_succ,

Goal state after:
case refine_4
R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ ((∑ x ∈ Finset.range 1, if h : x < 2 then A 1 ⟨x, h⟩ * B ⟨x, h⟩ 1 else 0) +
      if h : 1 < 2 then A 1 ⟨1, h⟩ * B ⟨1, h⟩ 1 else 0) =
    A 1 0 * B 0 1 + A 1 1 * B 1 1
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ ∑ c, single c c (f c) j k = if j = k then f j else 0

Tactic:
Finset.sum_eq_single j

Goal state after:
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ single j j (f j) j k = if j = k then f j else 0

case h₀
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ ∀ b ∈ Finset.univ, b ≠ j → single b b (f b) j k = 0

case h₁
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ j ∉ Finset.univ → single j j (f j) j k = 0
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
inhabited_h : Inhabited m
⊢ P 0

Tactic:
inhabit n

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : AddCommMonoid α
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
inhabited_h✝ : Inhabited m
inhabited_h : Inhabited n
⊢ P 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Nonempty n
A : Matrix l m α
ha : Function.Injective fun B ↦ A * B
v w : m → α
hvw : A *ᵥ v = A *ᵥ w
⊢ v = w

Tactic:
inhabit n

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Nonempty n
A : Matrix l m α
ha : Function.Injective fun B ↦ A * B
v w : m → α
hvw : A *ᵥ v = A *ᵥ w
inhabited_h : Inhabited n
⊢ v = w
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l✝
j k : m
l : n
h : j ≠ k
d : α
a : l✝
b : n
h₁ : i = a
⊢ (∑ j_1, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = 0 a b

Tactic:
simp [h₁, h, Finset.sum_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : LinearOrder M
inst✝⁴ : CanonicallyOrderedAdd M
inst✝³ : Sub M
inst✝² : AddLeftReflectLE M
inst✝¹ : OrderedSub M
s : Finset ι
inst✝ : OrderBot M
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup f = s.sup fun i ↦ a + f i

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α × β) = max (lift.{v, u} #α) (lift.{u, v} #β)

Tactic:
mk_prod,

Goal state after:
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α * lift.{u, v} #β = max (lift.{v, u} #α) (lift.{u, v} #β)
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (f i ⟨↑x, hi⟩)

Tactic:
← h i

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i ⟨↑x, hi⟩)
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
⊢ x *ᵥ ∑ i ∈ s, y i = ∑ i ∈ s, x *ᵥ y i

Tactic:
ext
  simp only [mulVec, dotProduct_sum, Finset.sum_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} #(Free.ChooseBasisIndex F K × Free.ChooseBasisIndex K A)

Tactic:
mk_prod,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) *
      lift.{max w v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{w, max v w} (lift.{w, v} #(Free.ChooseBasisIndex F K) * lift.{v, w} #(Free.ChooseBasisIndex K A))
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: 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))
x : M
this : ∀ (x : M), x = e.symm x • e 1
⊢ u x = (c • LinearMap.id) x

Tactic:
this x

Goal state after:
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))
x : M
this : ∀ (x : M), x = e.symm x • e 1
⊢ u (e.symm x • e 1) = (c • LinearMap.id) (e.symm x • e 1)
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
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
c d : R
⊢ (c + d) • LinearMap.id = c • LinearMap.id + d • LinearMap.id

Tactic:
by ext; simp [add_smul]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
⊢ 0 = 1

Tactic:
have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _
      rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Tower

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ U ↔ x ∈ V

Tactic:
by rw [← mem_restrictScalars R, H, mem_restrictScalars]

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

Goal state before:
pp: F : Type v'
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
φ : F
x✝ : B
⊢ (∃ x, φ x = x✝) ↔ x✝ ∈ Set.range ⇑φ

Tactic:
Set.mem_range

Goal state after:
F : Type v'
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
φ : F
x✝ : B
⊢ (∃ x, φ x = x✝) ↔ ∃ y, φ y = x✝
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = hd.prod

Tactic:
induction hd with

Goal state after:
case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : ∀ y ∈ hd :: tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = (hd :: tl).prod
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
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ adjoin R (↑S ∪ ⇑f ⁻¹' {0})

Tactic:
exact Subalgebra.add_mem _
      (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)

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

Goal state before:
pp: case left
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
i₁ : ι₁
i₂ : ι₂
x₁ : M₁ (i₁, i₂).1
x₂ : M₂ (i₁, i₂).2
⊢ ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.lift
                (toModule S ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₁ ↦
                  (toModule R ι₂ (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₂ ↦
                      (AlgebraTensorModule.curry (lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))).flip).flip) ∘ₗ
              toModule S (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i ↦
                AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
            lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)))
        x₁)
      x₂ =
    ((AlgebraTensorModule.curry (LinearMap.id ∘ₗ lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))) x₁) x₂

Tactic:
simp only [coe_comp, Function.comp_apply, toModule_lof, AlgebraTensorModule.map_tmul,
      AlgebraTensorModule.lift_apply, lift.tmul, coe_restrictScalars, flip_apply,
      AlgebraTensorModule.curry_apply, curry_apply, id_comp]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∃ s, ∀ (x : P), (linearCombination R id) (s x) = x) ↔
    ∃ s, ∀ (x : P), (linearCombination R id ∘ₗ s) x = LinearMap.id x

Tactic:
comp_apply,

Goal state after:
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
⊢ (∃ s, ∀ (x : P), (linearCombination R id) (s x) = x) ↔ ∃ s, ∀ (x : P), (linearCombination R id) (s x) = LinearMap.id x
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
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ (p.sum fun a₁ b ↦ (Finsupp.single a₁ (b ⊗ₜ[R] n)) i) = p i ⊗ₜ[R] n

Tactic:
Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp),

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
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ (Finsupp.single i (p i ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
⊢ Projective R P

Tactic:
refine ⟨g.comp i, fun x ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ (linearCombination R id) ((g ∘ₗ i) x) = x
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
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ N
i : ι
⊢ (p.sum fun a₁ b ↦ (Finsupp.single a₁ (m ⊗ₜ[R] b)) i) = m ⊗ₜ[R] p i

Tactic:
Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp),

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

Tactic:
Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp),

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 : ι
⊢ p i • n = (Finsupp.single i (p i • n)) 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
i : ι
⊢ p i • m = p.sum fun a₁ b ↦ (Finsupp.single a₁ (b • m)) i

Tactic:
Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp),

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 : ι
⊢ p i • m = (Finsupp.single i (p i • m)) i
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ a • ↑x ∈ selfAdjoint R

Tactic:
rw [Rat.smul_def]

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R
Module: Mathlib.Algebra.Star.StarRingHom

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝⁸ : Add A
inst✝⁷ : Add B
inst✝⁶ : Mul A
inst✝⁵ : Mul B
inst✝⁴ : Star A
inst✝³ : Star B
inst✝² : Add C
inst✝¹ : Mul C
inst✝ : Star C
e₁ : A ≃⋆+* B
e₂ : B ≃⋆+* C
a : A
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))

Tactic:
rw [e₁.map_star', e₂.map_star']

Goal state after:
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 α
d : ℕ
⊢ M = (↑d)ᴴ ↔ M = ↑d

Tactic:
rw [conjTranspose_natCast]

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
p : Type u_5
q : Type u_6
α : 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 α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
⊢ fromBlocks A B C D * fromBlocks A' B' C' D' =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Tactic:
by
  ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp only [fromBlocks, mul_apply, of_apply,
      Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]

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

Goal state before:
pp: n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
a b : n → α
⊢ (replicateCol ι a * replicateRow ι b).diag = a * b

Tactic:
ext
  simp [Matrix.mul_apply, replicateCol, replicateRow]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.updateRow i b).map star)ᵀ

Tactic:
map_updateRow

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) → m' i → α
⊢ (blockDiagonal' fun k ↦ diagonal (d k)) = diagonal fun ik ↦ d ik.fst ik.snd

Tactic:
by
  ext ⟨i, k⟩ ⟨j, k'⟩
  simp only [blockDiagonal'_apply, diagonal]
  obtain rfl | hij := Decidable.eq_or_ne i j
  · simp
  · simp [hij]

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

Goal state before:
pp: case pred
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℕ
h : LinearEquiv.baseChange R A M M (f ^ (-↑n)) = LinearEquiv.baseChange R A M M f ^ (-↑n)
⊢ LinearEquiv.baseChange R A M M (f ^ (-↑n - 1)) = LinearEquiv.baseChange R A M M f ^ (-↑n - 1)

Tactic:
simp only [zpow_sub_one, LinearEquiv.baseChange_mul, h, LinearEquiv.baseChange_inv]

Goal state after:
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 n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
⊢ r = r ^ m r * ((r ^ n r * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s)

Tactic:
mul_comm (r ^ n r) _,

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 n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
⊢ r = r ^ m r * ((∏ s ∈ S \ {r}, s ^ m s) * r ^ n r * ∏ s ∈ S \ {r}, s ^ n s)
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∉ S
⊢ ¬Subsingleton N

Tactic:
f.subsingleton_iff

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∉ S
⊢ 0 ∉ S
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ f 0 = 0

Tactic:
rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
P : Type u_3
inst✝ : CommMonoidWithZero P
f : S.LocalizationMap N
ms : M × ↥S
eq : 0 * f ↑ms.2 = f ms.1
⊢ f 0 = 0

Tactic:
rw [← zero_mul, map_mul, ← eq, zero_mul, mul_zero]

Goal state after: