mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
i : J.R
a :
  (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst i))) (↑x (WalkingMulticospan.left (J.fst i))) =
    ↑x (WalkingMulticospan.right i)
⊢ (hom (I.fst i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.fst i)) =
    (hom (I.snd i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.snd i))

Tactic:
have b := x.2 (WalkingMulticospan.Hom.snd i)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
i : J.R
a :
  (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.fst i))) (↑x (WalkingMulticospan.left (J.fst i))) =
    ↑x (WalkingMulticospan.right i)
b :
  (hom ((I.multicospan ⋙ forget C).map (WalkingMulticospan.Hom.snd i))) (↑x (WalkingMulticospan.left (J.snd i))) =
    ↑x (WalkingMulticospan.right i)
⊢ (hom (I.fst i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.fst i)) =
    (hom (I.snd i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.snd i))
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case neg
J : MultispanShape
a b : J.R
h : ¬a = b
⊢ Subsingleton (right a ⟶ right b)

Tactic:
have : IsEmpty (right a ⟶ right b) := ⟨by rintro ⟨⟩; simp at h⟩
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ToType D.L₀.X₃
x₂ : ToType D.L₁.X₂
x₁ : ToType D.L₂.X₁
h₂ : (ConcreteCategory.hom D.L₁.g) x₂ = (ConcreteCategory.hom D.v₀₁.τ₃) x₃
h₁ : (ConcreteCategory.hom D.L₂.f) x₁ = (ConcreteCategory.hom D.v₁₂.τ₂) x₂
⊢ (ConcreteCategory.hom D.δ) x₃ = (ConcreteCategory.hom D.v₂₃.τ₁) x₁

Tactic:
by
  have := (forget₂ C Ab).preservesFiniteLimits_of_preservesHomology
  have : PreservesFiniteLimits (forget C) := by
    have : forget₂ C Ab ⋙ forget Ab = forget C := HasForget₂.forget_comp
    simpa only [← this] using comp_preservesFiniteLimits _ _
  have eq := CategoryTheory.congr_fun (D.snd_δ)
    (Limits.Concrete.pullbackMk D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂)
  have eq₁ := Concrete.pullbackMk_fst D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
  have eq₂ := Concrete.pullbackMk_snd D.L₁.g D.v₀₁.τ₃ x₂ x₃ h₂
  rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at eq
  rw [eq₂] at eq
  refine eq.trans (CategoryTheory.congr_arg (D.v₂₃.τ₁) ?_)
  apply (Preadditive.mono_iff_injective' D.L₂.f).1 inferInstance
  rw [← ConcreteCategory.comp_apply, φ₁_L₂_f]
  dsimp [φ₂]
  rw [ConcreteCategory.comp_apply, eq₁]
  exact h₁.symm

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✝ : 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)

Tactic:
apply preservesLimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π

Tactic:
Cocone.w G left,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
G : ReflexiveCofork F
⊢ G.ι.app one = F.map right ≫ G.π
Module: Mathlib.RingTheory.Ideal.IsPrimary

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ I ≠ ⊤

pp: case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
· rintro rfl
    exact (radical_top R ▸ hi).ne_top rfl

Goal state after:
case right
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
⊢ n ∈ M' → IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'

Tactic:
hn

Goal state after:
case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ IsLocalizedModule.mk' f (r • n) s ∈ I • localized₀ p f M'
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case a.refine_1
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
a : M
ha : a ∈ I • M'
s : ↥p
r : R
hr : r ∈ I
n : M
hn : n ∈ M'
⊢ r • IsLocalizedModule.mk' f n s ∈ I • localized₀ p f M'

Tactic:
exact Submodule.smul_mem_smul hr ⟨n, hn, s, rfl⟩

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

Goal state before:
pp: case mpr
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 : Ideal R
z : S
s : ↥M
x : R
hx : x ∈ I
h : z * (algebraMap R S) ↑(⟨x, hx⟩, s).2 = (algebraMap R S) ↑(⟨x, hx⟩, s).1
⊢ ∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z

Tactic:
refine ⟨x, hx, s, ?_⟩

Goal state after:
case mpr
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 : Ideal R
z : S
s : ↥M
x : R
hx : x ∈ I
h : z * (algebraMap R S) ↑(⟨x, hx⟩, s).2 = (algebraMap R S) ↑(⟨x, hx⟩, s).1
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) x s = z
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
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
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ → { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂

Tactic:
exact fun hJ => Ideal.comap_mono hJ

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
N : Submodule R M
h : ∀ (r : ↑s), localized₀ (Submonoid.powers ↑r) (f r) N = ⊥
x✝ : ↑s
⊢ localized₀ (Submonoid.powers ↑x✝) (f x✝) N = localized₀ (Submonoid.powers ↑x✝) (f x✝) ⊥

Tactic:
simp only [h, Submodule.localized₀_bot]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring 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
Mₚ : (P : Ideal S) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal S) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal S) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal S) → [inst : P.IsMaximal] → Module S (Mₚ P)
inst✝¹ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsScalarTower R S (Mₚ P)
f : (P : Ideal S) → [inst : P.IsMaximal] → M →ₗ[S] Mₚ P
inst✝ : ∀ (P : Ideal S) [inst : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)
H :
  ∀ (P : Ideal S) [inst : P.IsMaximal] ⦃P_1 : Type u_1⦄ [inst_1 : AddCommMonoid P_1] [inst_2 : Module R P_1]
    (N : Submodule R P_1), Function.Injective ⇑(lTensor (Mₚ P) N.subtype)
x✝² : Type u_1
x✝¹ : AddCommMonoid x✝²
x✝ : Module R x✝²
N : Submodule R x✝²
P : Ideal S
hP : P.IsMaximal
⊢ Function.Injective
    ⇑((IsLocalizedModule.map P.primeCompl ((AlgebraTensorModule.rTensor R ↥N) (f P))
          ((AlgebraTensorModule.rTensor R x✝²) (f P)))
        ((AlgebraTensorModule.lTensor S M) N.subtype))

Tactic:
simpa [IsLocalizedModule.map_lTensor] using H P N

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

Goal state before:
pp: 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
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑1 * (↑a * (y₂ * ↑s₁))

Tactic:
convert! e using 1

Goal state after:
case e'_2
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
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑a * (y₁ * ↑s₂)

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
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₂ * ↑s₁)) = ↑a * (y₂ * ↑s₁)
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ 0 = mk' S 1 1

Tactic:
@comm _ Eq,

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ mk' S 1 1 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}

Tactic:
change (mapOfCompatibleSMul A R A M N).ker ≤ S

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ S
Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : ((MvPolynomial.eval fun p ↦ 1 p.1 p.2).mapMatrix (mvPolynomialX m m R)).det = 1
⊢ False

Tactic:
← RingHom.map_det,

Goal state after:
m : Type u_1
R : Type u_3
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h_det : (mvPolynomialX m m R).det = 0
this : (MvPolynomial.eval fun p ↦ 1 p.1 p.2) (mvPolynomialX m m R).det = 1
⊢ False
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case empty
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ M (∑ n ∈ ∅, C (p.coeff n) * T n)

Tactic:
convert! h_C 0

Goal state after:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
⊢ ∑ n ∈ ∅, C (p.coeff n) * T n = C 0
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)) =
    AddMonoidAlgebra.single (0 + m) (a * 1) * AddMonoidAlgebra.single n 1

Tactic:
single_mul_single

Goal state after:
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)) = AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
v : n → α
⊢ (diagonal v).adjugate = diagonal fun i ↦ ∏ j ∈ univ.erase i, v j

Tactic:
ext i j
  simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]
  obtain rfl | hij := eq_or_ne i j
  · rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,
      prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]
  · rw [diagonal_apply_ne _ hij]
    refine det_eq_zero_of_row_eq_zero j fun k => ?_
    obtain rfl | hjk := eq_or_ne k j
    · rw [updateCol_self, Pi.single_eq_of_ne' hij]
    · rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]

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

Goal state before:
pp: n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f (M.adjugate i k) = (f.mapMatrix (M.updateRow k (Pi.single i 1))).det

Tactic:
← RingHom.map_det,

Goal state after:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f (M.adjugate i k) = f (M.updateRow k (Pi.single i 1)).det
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) 1 * ((kroneckerMapBilinear f) 1) B).det =
    (blockDiagonal fun x ↦ A.map fun a ↦ (f a) 1).det * (blockDiagonal fun x ↦ B.map fun b ↦ (f 1) b).det

Tactic:
det_mul,

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹³ : Semiring S
inst✝¹² : Semiring R
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : DecidableEq n
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : NonAssocSemiring β
inst✝⁵ : CommRing γ
inst✝⁴ : Module R α
inst✝³ : Module S β
inst✝² : Module R γ
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) 1).det * (((kroneckerMapBilinear f) 1) B).det =
    (blockDiagonal fun x ↦ A.map fun a ↦ (f a) 1).det * (blockDiagonal fun x ↦ B.map fun b ↦ (f 1) b).det
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: case e_a.e_a.e_a
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)
⊢ C * (V * (⅟A * A)) + C * (V * (⅟A * (U * (C * V)))) = (C + C * V * ⅟A * U * C) * V

Tactic:
simp only [Matrix.add_mul, invOf_mul_self', Matrix.mul_one, add_right_inj]

Goal state after:
case e_a.e_a.e_a
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)
⊢ C * (V * (⅟A * (U * (C * V)))) = C * V * ⅟A * U * C * V
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible

Goal state after:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A * A⁻¹ = 1
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible

Goal state after:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A⁻¹ * A = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x✝¹ x✝ : m
h : b x✝ < b x✝¹
⊢ (-M) x✝¹ x✝ = 0

Tactic:
neg_apply,

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝¹ : LT α
inst✝ : NegZeroClass R
M : Matrix m m R
hM : M.BlockTriangular b
x✝¹ x✝ : m
h : b x✝ < b x✝¹
⊢ -M x✝¹ x✝ = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
by_cases h : IsUnit A.det
  · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩
  · exact Or.inr (nonsing_inv_apply_not_isUnit _ h)

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

Goal state before:
pp: case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
⊢ (M.toSquareBlockProp fun i ↦ b i = k).det * (M.toSquareBlockProp fun i ↦ ¬b i = k).det =
    ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
rw [this, prod_insert (notMem_erase _ _)]

Goal state after:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst : DecidableEq m_1] [inst_1 : Fintype m_1],
      M.BlockTriangular b_1 →
        image b_1 univ = (image b univ).erase s → M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
⊢ (M.toSquareBlockProp fun i ↦ b i = k).det * (M.toSquareBlockProp fun i ↦ ¬b i = k).det =
    (M.toSquareBlock b k).det * ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
let L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
    List.ofFn fun i : Fin r =>
      ⟨inr unit, inl i, by simp, -M (inr unit) (inl i) / M (inr unit) (inr unit)⟩

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal