mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (reflectorAdjunction R).unit.app (R.obj ((reflector R).obj X.A)) ≫ R.map ((reflector R).map X.a) =
    𝟙 (R.obj ((reflector R).obj X.A))

Tactic:
rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ R.map ((reflector R).map ((reflectorAdjunction R).unit.app X.A ≫ X.a)) = 𝟙 (R.obj ((reflector R).obj X.A))
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
⊢ PreservesLimit K (monadicLeftAdjoint R)

Tactic:
let : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) := by
      constructor
      intro c h
      have : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
      have : HasLimit F := hasLimit_of_reflective F R
      constructor
      apply isLimitChangeEmptyCone D (limit.isLimit F)
      apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans
      apply (monadicLeftAdjoint R).mapIso
      letI := monadicCreatesLimits.{v, v} R
      let A := CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit F R
      apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
this : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) :=
  {
    preserves := fun {c} h ↦
      have this := { exists_limit := Nonempty.intro { cone := c, isLimit := h } };
      have this_1 := hasLimit_of_reflective F R;
      Nonempty.intro
        (isLimitChangeEmptyCone D (limit.isLimit F) ((monadicLeftAdjoint R).mapCone c)
          ((asIso ((monadicAdjunction R).counit.app (limit.cone F).1)).symm ≪≫
            (monadicLeftAdjoint R).mapIso
              (let A := preservesLimit_of_createsLimit_and_hasLimit F R;
              (isLimitOfPreserves R (limit.isLimit F)).conePointUniqueUpToIso h))) }
⊢ PreservesLimit K (monadicLeftAdjoint R)
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
⊢ PreservesColimit (F ⋙ R) (comonadicRightAdjoint R)

Tactic:
constructor
      intro c h
      have : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
      have : HasColimit F := hasColimit_of_coreflective F R
      constructor
      apply isColimitChangeEmptyCocone D (colimit.isColimit F)
      apply (asIso ((comonadicAdjunction R).unit.app _)).trans
      apply (comonadicRightAdjoint R).mapIso
      letI := comonadicCreatesColimits.{v, v} R
      let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F R
      apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
⊢ PreservesColimit K (comonadicRightAdjoint R)

Tactic:
let : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) := by
      constructor
      intro c h
      have : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
      have : HasColimit F := hasColimit_of_coreflective F R
      constructor
      apply isColimitChangeEmptyCocone D (colimit.isColimit F)
      apply (asIso ((comonadicAdjunction R).unit.app _)).trans
      apply (comonadicRightAdjoint R).mapIso
      letI := comonadicCreatesColimits.{v, v} R
      let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F R
      apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := empty D
this : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) :=
  {
    preserves := fun {c} h ↦
      have this := { exists_colimit := Nonempty.intro { cocone := c, isColimit := h } };
      have this_1 := hasColimit_of_coreflective F R;
      Nonempty.intro
        (isColimitChangeEmptyCocone D (colimit.isColimit F) ((comonadicRightAdjoint R).mapCocone c)
          (asIso ((comonadicAdjunction R).unit.app (colimit.cocone F).1) ≪≫
            (comonadicRightAdjoint R).mapIso
              (let A := preservesColimit_of_createsColimit_and_hasColimit F R;
              (isColimitOfPreserves R (colimit.isColimit F)).coconePointUniqueUpToIso h))) }
⊢ PreservesColimit K (comonadicRightAdjoint R)
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N P : Submodule R M
⊢ (map N.mkQ P).annihilator = N.colon ↑P

Tactic:
by
  ext
  rw [mem_annihilator, mem_colon]
  exact ⟨fun H p hp ↦ (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
    fun H _ ⟨p, hp, hpm⟩ ↦ hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ a ^ n = 0

Tactic:
simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulRight R a ^ n = 0

Tactic:
simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢

Goal state after:
case h
R : Type u_1
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0
Module: Mathlib.RingTheory.Localization.Ideal

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
inst✝ : IsLocalization M S
I J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * (↑m * ↑mj) = j * (↑m * ↑mi)
⊢ ∃ a b, x * (algebraMap R S) ↑b = (algebraMap R S) ↑a

Tactic:
refine ⟨⟨i * (m * mj : M), I.mul_mem_right _ hi, hm ▸ J.mul_mem_right _ hj⟩, mi * (m * mj), ?_⟩

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I J : Ideal R
x : S
i : R
hi : i ∈ I
mi : ↥M
j : R
hj : j ∈ J
mj : ↥M
hi' : x = mk' S i mi
hj' : x = mk' S j mj
m : ↥M
hm : i * (↑m * ↑mj) = j * (↑m * ↑mi)
⊢ x * (algebraMap R S) ↑(mi * (m * mj)) = (algebraMap R S) ↑⟨i * ↑(m * mj), ⋯⟩
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ I = ⊤

Tactic:
Ideal.eq_top_iff_one

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
I : Ideal S
inst✝ : I.IsPrime
J : Ideal R
H : J ≤ Ideal.under R I
hI : (Ideal.under R I).IsMaximal
r m : R
hm : m ∈ M
hM : (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) I)) m = 0
⊢ 1 ∈ I
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hy : M ≤ Submonoid.comap g T
x y : ↥(ker g)
⊢ ⟨(algebraMap R S) ↑(x + y), ⋯⟩ = ⟨(algebraMap R S) ↑x, ⋯⟩ + ⟨(algebraMap R S) ↑y, ⋯⟩

Tactic:
simp only [Submodule.coe_add, map_add, AddMemClass.mk_add_mk]

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

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ (algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩ = (algebraMap R T) ↑⟨y, hy⟩

Tactic:
exact (IsScalarTower.algebraMap_apply _ _ _ _).symm

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z * (x * (algebraMap R S) ↑s) = 0 * (algebraMap R S) ↑s

Tactic:
e,

Goal state after:
case h
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
z : R
hz : z * (y, s).1 = 0
⊢ (algebraMap R S) z * (algebraMap R S) (y, s).1 = 0 * (algebraMap R S) ↑s
Module: Mathlib.RingTheory.Localization.Submodule

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
inst✝ : IsLocalization M S
h : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
rw [isNoetherianRing_iff, isNoetherian_iff] at h ⊢
  exact OrderEmbedding.wellFounded (IsLocalization.orderEmbedding M S).dual h

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝² : Algebra S R := e.symm.toRingHom.toAlgebra
this✝¹ : IsLocalization.Away 1 R
this✝ : IsLocalization.Away (f 1) T
this : RingHomInvPair ↑e ↑e.symm
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1

Tactic:
have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f :=
      IsLocalization.map_comp ..

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this✝³ : Algebra S R := e.symm.toRingHom.toAlgebra
this✝² : IsLocalization.Away 1 R
this✝¹ : IsLocalization.Away (f 1) T
this✝ : RingHomInvPair ↑e ↑e.symm
this : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ (algebraMap R S) α * x ∈ pS

Tactic:
e,

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
y : ↥pS
s c : ↥(algebraMapSubmonoid S p.primeCompl)
hc : ↑c * (x * ↑(y, s).2) = ↑c * ↑(y, s).1
α : R
hα : α ∈ ↑p.primeCompl
e : (algebraMap R S) α = ↑(c * s)
⊢ ↑(c * s) * x ∈ pS
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
⊢ x ∈ pS

Tactic:
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ β * α = 1 + γ := by
    obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
    refine ⟨β, β * α - 1, ?_, ?_⟩
    · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
        map_mul, hβ, inv_mul_cancel₀, sub_self]
      rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
    · rw [add_sub_cancel]

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
α : R
hα : α ∉ p
hαx : α • x ∈ pS
β γ : R
hγ : γ ∈ p
hβ : β * α = 1 + γ
⊢ x ∈ pS
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A.updateRow i (Pi.single j 1)).det = (A.updateCol j (Pi.single i 1)).det

Tactic:
det_apply',

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ σ, ↑↑(sign σ) * ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = (A.updateCol j (Pi.single i 1)).det
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
⊢ A.updateRow (σ j) (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single (σ j) 1) (σ j') j'

Tactic:
have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff

Goal state after:
case pos.e_f
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
j : n
σ : Perm n
a✝ : σ ∈ univ
j' : n
this : σ j' = σ j ↔ j' = j
⊢ A.updateRow (σ j) (Pi.single j 1) (σ j') j' = A.updateCol j (Pi.single (σ j) 1) (σ j') j'
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j k : n
⊢ A i k * A.adjugate k j = Aᵀ.cramer (Pi.single k (A i k)) j

Tactic:
by
  rw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← map_smul, ← Pi.single_smul',
    smul_eq_mul, mul_one]

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
⊢ t.inv.toMatrix * t.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩
  simp [toMatrix, transvection_mul_transvection_same, t_hij]

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

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
⊢ t.toMatrix * t.inv.toMatrix = 1

Tactic:
rcases t with ⟨_, _, t_hij⟩
  simp [toMatrix, transvection_mul_transvection_same, t_hij]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case MX
R : Type u_3
inst✝ : CommSemiring R
a✝¹ : Nontrivial R
p✝ : R[X]
hp : p✝ ≠ 0
a✝ : toLaurent p✝.reverse = invert (toLaurent p✝) * T ↑p✝.natDegree
⊢ toLaurent (p✝ * X).reverse = invert (toLaurent (p✝ * X)) * T ↑(p✝ * X).natDegree

Tactic:
| MX _ hp =>

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

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
by
  simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]
  rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]
  rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ ⅟A * A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * A + ⅟A * U * C * V -
      ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    1 + ⅟A * U * C * V - (⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V)

Tactic:
rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * C * V - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V =
    1 + ⅟A * U * C * V - (⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V)
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ (A + U * C * V) * (⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) = 1

Tactic:
simp only [Matrix.mul_sub, Matrix.add_mul, mul_invOf_self']

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ 1 + U * C * V * ⅟A -
      (A * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A) +
        U * C * V * (⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A)) =
    1
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : CommMagma R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ = kroneckerMap (fun x1 x2 ↦ x1 * x2) xᴴ yᴴ

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝¹ : Mul R
inst✝ : StarMul R
x : Matrix l m R
y : Matrix n p R
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) x y)ᴴ = (kroneckerMap (fun x1 x2 ↦ x1 * x2) yᴴ xᴴ).submatrix Prod.swap Prod.swap

Tactic:
by
  ext; simp

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

Goal state before:
pp: R : Type u_1
α : Type u_3
β : Type u_5
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid α
inst✝⁷ : AddCommMonoid β
inst✝⁶ : Module R α
inst✝⁵ : Module R β
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid α
inst✝² : StarAddMonoid β
inst✝¹ : StarModule R α
inst✝ : StarModule R β
x : Matrix l m α
y : Matrix n p β
⊢ (kroneckerMap (tmul R) x y)ᴴ = kroneckerMap (tmul R) xᴴ yᴴ

Tactic:
by
  ext; simp

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ A.det * B.det = 1

Tactic:
by rw [mul_comm, ← det_mul, h, det_one]

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

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ B.det * A.det = 1

Tactic:
by rw [mul_comm, ← det_mul, h, det_one]

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

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix m n α
h : B * A⁻¹ = C
⊢ B = B * A⁻¹ * A

Tactic:
inv_mul_cancel_right_of_invertible

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
B C : Matrix m n α
h : B * A⁻¹ = C
⊢ B = B
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case pos
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b k < b i
⊢ (fun j ↦ M i j) k * (fun j_1 ↦ N j_1 j) k = 0

pp: case neg
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b i ≤ b k
⊢ (fun j ↦ M i j) k * (fun j_1 ↦ N j_1 j) k = 0

Tactic:
· simp_rw [hM hki, zero_mul]

Goal state after:
case neg
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : LinearOrder α
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring R
M N : Matrix m m R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b i ≤ b k
⊢ (fun j ↦ M i j) k * (fun j_1 ↦ N j_1 j) k = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ ((reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M).det =
    (fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
        (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j)).det

Tactic:
det_apply',

Goal state after:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ ∑ σ, ↑↑(Equiv.Perm.sign σ) * ∏ i, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i =
    (fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
        (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j)).det