mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
hγ : ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ π₂ ≫ π₁ ≫ y₂ = π ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f

Tactic:
obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ := hγ

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : ∀ ⦃A : C⦄ (y : A ⟶ S₂.homology), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ homologyMap φ
A : C
y₂ : A ⟶ S₂.X₂
hy₂ : y₂ ≫ S₂.g = 0
A₁ : C
π₁ : A₁ ⟶ A
hπ₁ : Epi π₁
γ : A₁ ⟶ S₁.homology
A₂ : C
π₂ : A₂ ⟶ A₁
hπ₂ : Epi π₂
x₂ : A₂ ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
fac : π₂ ≫ γ = S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ
A₃ : C
π₃ : A₃ ⟶ A₂
hπ₃ : Epi π₃
x₁ : A₃ ⟶ S₂.X₁
hx₁ : π₃ ≫ π₂ ≫ π₁ ≫ y₂ = π₃ ≫ x₂ ≫ φ.τ₂ + x₁ ≫ S₂.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ S₁.g = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.τ₂ + y₁ ≫ S₂.f
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ (pullback.fst S₁.L₁.g S₁.v₀₁.τ₃ ≫ S₁.v₁₂.τ₂) ≫ f.f₂.τ₂ =
    pullback.map S₁.L₁.g S₁.v₀₁.τ₃ S₂.L₁.g S₂.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ ⋯ ⋯ ≫
      pullback.fst S₂.L₁.g S₂.v₀₁.τ₃ ≫ S₂.v₁₂.τ₂

Tactic:
simp only [assoc, pullback.lift_fst_assoc, ← comp_τ₂, f.comm₁₂]

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.pt.a ≫ T.map (s.ι.f ≫ T.ε.app X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a

Tactic:
rw [Functor.map_comp, reassoc_of% h₂, Comonad.right_counit]

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
s : Fork (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)
h₁ : s.ι.f ≫ T.map X.a = s.ι.f ≫ T.δ.app X.A
h₂ : s.pt.a ≫ T.map s.ι.f = s.ι.f ≫ T.δ.app X.A
⊢ s.ι.f ≫ 𝟙 (T.obj X.A) = (s.ι.f ≫ T.ε.app X.A) ≫ X.a
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
n✝ : ℕ
hi : n✝ + 1 < n + 1 + 1
j : ℕ
hj : j + 1 < n + 1 + 1
hjk : ⟨j + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨n✝ + 1, hi⟩ ≤ ⟨j + 1, hj⟩
⊢ map F f ⟨n✝ + 1, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨n✝ + 1, hi⟩ ⟨j + 1, hj⟩ hij ≫ map F f ⟨j + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
· obtain _ | k := k
      · simp [Fin.ext_iff] at hjk
      · dsimp
        rw [← F.map_comp, homOfLE_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
⊢ ∀ (j_1 : WalkingMultispan J), colimit.ι I.multispan j_1 ≫ i = colimit.ι I.multispan j_1 ≫ j

Tactic:
rintro (a | b)
      · simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]
      · apply h

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ CreatesLimit (parallelPair f g) F

Tactic:
apply +allowSynthFailures comonadicCreatesLimitOfPreservesLimit

Goal state after:
case inst
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ PreservesLimit (parallelPair f g ⋙ F) (comonadicRightAdjoint F ⋙ F)

case inst
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : ComonadicLeftAdjoint F
A B : C
f g : A ⟶ B
inst✝ : F.IsCosplitPair f g
⊢ PreservesLimit ((parallelPair f g ⋙ F) ⋙ comonadicRightAdjoint F ⋙ F) (comonadicRightAdjoint F ⋙ F)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' (eqToIso h).hom 0 ⋯ = (eqToIso h₀).hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
w

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ (eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯) ≫ app' (eqToIso h).hom 0 ⋯ =
    (eqToIso h₀).hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((beckEqualizer X).lift (counitFork X))

Tactic:
change
          IsIso
            (IsLimit.conePointUniqueUpToIso (beckEqualizer X)
                (counitLimitOfPreservesEqualizer X)).inv

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
X : adj.toComonad.Coalgebra
⊢ IsIso ((beckEqualizer X).conePointUniqueUpToIso (counitLimitOfPreservesEqualizer X)).inv
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Flat (ULift.{t, u} R) M ↔ Flat R M

Tactic:
by
  refine ⟨fun h ↦ .trans _ (ULift R) _, fun h ↦ ?_⟩
  have : Module.Flat (ULift.{t} R) R := .of_ulift
  let _ := ULift.algebra'
  exact .trans _ R _

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
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
⊢ HasLimit F

Tactic:
let t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit _)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ HasLimit F
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n, r ^ n • ⊤ = ⊥

Tactic:
simp_rw [S.mkQ_surjective.forall, ← map_smul, ne_eq, ← LinearMap.mem_ker, ker_mkQ]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
x✝ : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ n, r ^ n • ⊤ ≤ S) ↔ ∀ (r : R), ∀ x ∉ S, r • x ∈ S → ∃ n, r ^ n • ⊤ = ⊥
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ p ∈ {p | I.radical.IsMinimalPrime p}

Tactic:
· refine ⟨⟨a, a.radical_le_iff.2 ha⟩, ?_⟩
    simp only [and_imp] at *
    exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4

Goal state after:
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 : Ideal R
n : ℕ
x : R
s : ↥M
hn : ∃ s ∈ M, s * x ^ n ∈ I
⊢ ∃ s ∈ M, s * x ∈ I.radical

Tactic:
obtain ⟨s, hs, h⟩ := hn

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 : Ideal R
n : ℕ
x : R
s✝ : ↥M
s : R
hs : s ∈ M
h : s * x ^ n ∈ I
⊢ ∃ s ∈ M, s * x ∈ I.radical
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
⊢ (localRingHom I J f hIJ) (mk' (Localization I.primeCompl) x y) = mk' (Localization J.primeCompl) (f x) ⟨f ↑y, ⋯⟩

Tactic:
localRingHom_mk'

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit ((localRingHom I J f hIJ) (mk' (Localization.AtPrime I) r s))
⊢ IsUnit (mk' (Localization.AtPrime I) r s)

Tactic:
localRingHom_mk'

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
r : R
s : ↥I.primeCompl
hx : IsUnit (mk' (Localization.AtPrime J) (f r) ⟨f ↑s, ⋯⟩)
⊢ IsUnit (mk' (Localization.AtPrime I) r s)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] ↦
    P

Tactic:
introv _ _ hf

Goal state after:
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R✝ S
r : R✝
inst✝ : IsLocalization.Away r S
f : S →+* T
hf : (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (f.comp (algebraMap R✝ S))
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] {R S} [CommRing R] [CommRing S] ↦
    P

Tactic:
introv _ _ hf

Goal state after:
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R✝ S T : Type u
inst✝⁴ : CommRing R✝
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
s : S
inst✝ : IsLocalization.Away s T
f : R✝ →+* S
hf : (fun {R S} [CommRing R] [CommRing S] ↦ P) f
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ ∀ (R' S' : Type u) [inst : CommRing R'] [inst_1 : CommRing S'] [inst_2 : Algebra R R'] [inst_3 : Algebra S S']
    [inst_4 : IsLocalization.Away r R'] [inst_5 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)

Tactic:
R'

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
R' : Type u
⊢ ∀ (S' : Type u) [inst : CommRing R'] [inst_1 : CommRing S'] [inst_2 : Algebra R R'] [inst_3 : Algebra S S']
    [inst_4 : IsLocalization.Away r R'] [inst_5 : IsLocalization.Away (f r) S'],
    (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ P) (IsLocalization.Away.map R' S' f r)
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 = C * A
⊢ C * A * A⁻¹ = C

Tactic:
mul_inv_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 = C * A
⊢ C = C
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' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i ↦ { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
have B : L'.map toMatrix = listTransvecRow M := by simp [L', listTransvecRow, Function.comp_def]

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 ()) }
A : List.map toMatrix L = listTransvecCol M
B : List.map toMatrix L' = listTransvecRow M
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this✝ : Invertible (M.toBlock p p)
this : (fun i ↦ k ≤ b i) = q
⊢ (M⁻¹.toBlock q fun i ↦ b i < k) = M⁻¹.toBlock q p * M.toBlock p p * (M.toBlock p p)⁻¹

Tactic:
mul_inv_cancel_right_of_invertible

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0
this✝ : Invertible (M.toBlock p p)
this : (fun i ↦ k ≤ b i) = q
⊢ (M⁻¹.toBlock q fun i ↦ b i < k) = M⁻¹.toBlock q p
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case H.inl
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hbi : b i = k
⊢ M⁻¹ i j = 0

Tactic:
have : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, hbi.ge⟩ ⟨j, hbi ▸ hij⟩ = 0 := by
      simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]

Goal state after:
case H.inl
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m] [Invertible M],
      M.BlockTriangular b → image b univ = t → M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := (image b univ).max' ⋯
b' : { a // b a < k } → α := fun i ↦ b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := M.toBlock (fun i ↦ b i < k) fun j ↦ b j < k
hbi : b i = k
this : M⁻¹.toBlock (fun i ↦ k ≤ b i) (fun i ↦ b i < k) ⟨i, ⋯⟩ ⟨j, ⋯⟩ = 0
⊢ M⁻¹ i j = 0
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: n : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_3
inst✝ : CommRing R
A : Matrix n n R[X]
M : Matrix n n R
⊢ eval 0 (A + X • M.map ⇑C).det = eval 0 A.det

Tactic:
by
  simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, map_mul]
  simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X,
    mul_zero, add_zero]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank

Tactic:
rw [← generators_card p, lift_spanRank_le_iff_exists_span_set_card_le]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
⊢ ∃ s, Cardinal.lift.{u, v} (Cardinal.mk ↑s) ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑p.generators) ∧ span S s = map f p
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ 1 ↔ x ∈ Subalgebra.toSubmodule ⊥

Tactic:
Algebra.toSubmodule_bot

Goal state after:
case empty
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
his : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ 1 ↔ x ∈ 1
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ↑p.coeffs ⊆ Set.range ⇑f
n : ℕ
hn : ¬p.coeff n = 0
⊢ p.coeff n ∈ Set.range ⇑f

Tactic:
· exact h <| coeff_mem_coeffs hn

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«1»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 1 = (X ^ 2 - C M.trace * X + C M.det).coeff 1

pp: case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«2»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 2 = (X ^ 2 - C M.trace * X + C M.det).coeff 2

Tactic:
· simp [trace_eq_neg_charpoly_coeff, hn]

Goal state after:
case pos.«_@».Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff.4094078725._hygCtx._hyg.105.«2»
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
M : Matrix n n R
inst✝ : Nontrivial R
hn : Fintype.card n = 2
this : Nonempty n
⊢ M.charpoly.coeff 2 = (X ^ 2 - C M.trace * X + C M.det).coeff 2
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case succ.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * (n + k + 1).choose (k + 1) = (n + k + 1).choose (n + 1) * (n + 1)

Tactic:
← choose_symm_of_eq_add this,

Goal state after:
case succ.e_a.e_a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
this : n + k + 1 = n + (k + 1)
⊢ (k + 1) * (n + k + 1).choose n = (n + k + 1).choose (n + 1) * (n + 1)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
D : (n → R[X]) [⋀^n]→ₗ[R[X]] R[X] := detRowAlternating
h_map : ∀ (s : Finset n), (s.piecewise (fun i ↦ M.map (⇑C) i) fun i ↦ 1 i) = map (s.piecewise M 1) ⇑C
s : Finset n
⊢ (map (s.piecewise M 1) ⇑C).det = C (det (s.piecewise M 1))

Tactic:
exact (RingHom.map_det C _).symm

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
hf : ¬f = 0
⊢ ((taylor r) f).coeff f.natDegree = f.leadingCoeff

Tactic:
· rw [taylor_coeff, hasseDeriv_natDegree_eq_C, eval_C]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ f = 0

Tactic:
← taylor_eq_zero r

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
h : ∀ (k : ℕ), eval r ((hasseDeriv k) f) = 0
⊢ (taylor r) f = 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.scaleRoots 0).coeff n = (p.leadingCoeff • X ^ p.natDegree).coeff n

Tactic:
simp only [coeff_scaleRoots, tsub_eq_zero_iff_le, zero_pow_eq, mul_ite,
    mul_one, mul_zero, coeff_smul, coeff_X_pow, smul_eq_mul]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (if p.natDegree ≤ n then p.coeff n else 0) = if n = p.natDegree then p.leadingCoeff else 0
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left✝ : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ ↑(p.coeff n) ∈ ↑T

Tactic:
exact Subtype.mem (coeff p n : T)

Goal state after: