mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext H.isColimit <;> refine e.trans ?_

Goal state after:
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ s.π = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ s.π = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : r • x = 0
⊢ x = 0

Tactic:
smul_eq_iff_of_mem (hr := hr)

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : x = Localization.mk 1 ⟨r, hr⟩ • 0
⊢ x = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R' : Type u_6
inst✝⁴ : CommSemiring R'
inst✝³ : Algebra R R'
inst✝² : IsLocalization S R'
inst✝¹ : Module R' M
inst✝ : IsScalarTower R R' M
s : ↥S
⊢ IsUnit ((algebraMap R (End R M)) ↑s)

Tactic:
by
    rw [← (Algebra.lsmul R (A := R') R M).commutes]; exact (IsLocalization.map_units R' s).map _

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T T₁ T₂ : Monad C
h : T₂ ⟶ T₁
A : T₁.Algebra
⊢ T₂.η.app A.A ≫ h.app A.A ≫ A.a = 𝟙 A.A

Tactic:
simp [A.unit]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : SubtractionCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f (-m) s = -mk' f m s

Tactic:
by
  delta mk'
  rw [LocalizedModule.mk_neg, map_neg]

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

Goal state before:
pp: case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J✝ : Ideal R
J K : Submodule R R
hN₁✝ : J.FG
hN₂✝ : K.FG
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ J ^ i * K ^ (n + m - i) ≤ I

Tactic:
exact mul_le_right.trans ((pow_le_pow_right (by lia)).trans hm)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n✝ : ℕ
hI : I.FG
n : ℕ
ih : (I ^ n).FG
⊢ (I ^ n.succ).FG

Tactic:
rw [IsTwoSided.pow_succ]
    exact hI.mul ih

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ IsPreconnected J

Tactic:
by
  apply IsPreconnected.of_constant_of_preserves_morphisms
  intro α F hF j j'
  specialize h j j'
  induction h with
  | refl => rfl
  | tail _ hj ih =>
    rw [ih]
    rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
    exacts [hF hj, (hF hj).symm]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C✝ : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.5, u_1} C✝
inst✝³ : Category.{?u.8, u_2} D
P : MorphismProperty D
Q : MorphismProperty C✝
inst✝² : Q.IsMultiplicative
F : C✝ ⥤ D
X✝ : D
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
W₁ W₂ : MorphismProperty C
inst✝ : W₁.HasFactorization W₂
S : C
X Y : Over S
f : X ⟶ Y
⊢ Nonempty (W₁.over.MapFactorizationData W₂.over f)

Tactic:
let hf := W₁.factorizationData W₂ f.left

Goal state after:
C✝ : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.5, u_1} C✝
inst✝³ : Category.{?u.8, u_2} D
P : MorphismProperty D
Q : MorphismProperty C✝
inst✝² : Q.IsMultiplicative
F : C✝ ⥤ D
X✝ : D
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
W₁ W₂ : MorphismProperty C
inst✝ : W₁.HasFactorization W₂
S : C
X Y : Over S
f : X ⟶ Y
hf : W₁.MapFactorizationData W₂ (Over.Hom.left f) := W₁.factorizationData W₂ (Over.Hom.left f)
⊢ Nonempty (W₁.over.MapFactorizationData W₂.over f)
Module: Mathlib.CategoryTheory.EffectiveEpi.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
B : C
α : Type u_2
α' : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
e : α' ≃ α
P : EffectiveEpiFamilyStruct (fun a ↦ X (e a)) fun a ↦ π (e a)
W✝ : C
x✝¹ : (a : α) → X a ⟶ W✝
x✝ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x✝¹ a₁ = g₂ ≫ x✝¹ a₂
a : α
⊢ π a ≫ P.desc (fun x ↦ x✝¹ (e x)) ⋯ = x✝¹ a

Tactic:
obtain ⟨a, rfl⟩ := e.surjective a

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
B : C
α : Type u_2
α' : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
e : α' ≃ α
P : EffectiveEpiFamilyStruct (fun a ↦ X (e a)) fun a ↦ π (e a)
W✝ : C
x✝¹ : (a : α) → X a ⟶ W✝
x✝ : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ x✝¹ a₁ = g₂ ≫ x✝¹ a₂
a : α'
⊢ π (e a) ≫ P.desc (fun x ↦ x✝¹ (e x)) ⋯ = x✝¹ (e a)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
x : RXm
⊢ (eval₂Hom ((↑f).comp (algebraMap R (MvPolynomial (Fin n) R))) fun i ↦ ↑f (h i)) x = f' x

Tactic:
AlgHom.coe_toRingHom,

Goal state after:
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
x : RXm
⊢ (eval₂Hom ((↑f).comp (algebraMap R (MvPolynomial (Fin n) R))) fun i ↦ f (h i)) x = f' x
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ (algebraMap A B).FinitePresentation ↔ Algebra.FinitePresentation A B

Tactic:
RingHom.FinitePresentation,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso a

Tactic:
by
  rw [←
    show _ = a from
      (Category.comp_id _).symm.trans
        ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit
          WalkingCospan.left)]
  infer_instance

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

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
          (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
        lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
      fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂)

Tactic:
apply pullback.hom_ext
      · apply pullback.hom_ext
        · simp only [Category.assoc, lift_fst, lift_fst_assoc, Category.id_comp]
          rw [condition]
        · simp [Category.assoc, condition]
      · simp only [Category.assoc, lift_snd, lift_fst, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom ℬ (tensorHom ℬ f₁ f₂) f₃ ≫ (BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom =
    (BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom ≫ tensorHom ℬ f₁ (tensorHom ℬ f₂ f₃)

Tactic:
dsimp [tensorHom]
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩
  · simp
  apply (ℬ _ _).isLimit.hom_ext
  rintro ⟨_ | _⟩ <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (Functor.empty C) F
⊢ IsIso (terminalComparison F)

Tactic:
← preservesTerminalIso_hom

Goal state after:
C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CartesianMonoidalCategory C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (Functor.empty C) F
⊢ IsIso (preservesTerminalIso F).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : CartesianMonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : CartesianMonoidalCategory D
F : C ⥤ D
inst✝¹ : F.Monoidal
inst✝ : PreservesFiniteProducts F
⊢ ε F = (preservesTerminalIso F).inv

Tactic:
change (εIso F).symm.inv = _; congr; ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ ∀ (s : PullbackCone μ μ),
    lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A) ≫ μ ▷ A = s.fst

Tactic:
by
      refine fun s => CartesianMonoidalCategory.hom_ext _ _ ?_ (by simp)
      simp only [lift_whiskerRight, lift_fst]
      rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_left]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ fᘁ ▷ X ≫ ε_ X Xᘁ = Yᘁ ◁ f ≫ ε_ Y Yᘁ

Tactic:
by
  apply_fun tensorRightHomEquiv _ X (Xᘁ) _
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
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
b : Basis ι R M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Dual R M ⊗[R] N
⊢ (dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x

Tactic:
rw [← dualTensorHomEquivOfBasis_apply b,
    LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F =
    pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))

Tactic:
convert!
    (eq_whisker pullback.condition Limits.prod.fst :
      (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
j : WalkingParallelPair
⊢ (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv) ≫
      (G.mapCone (equalizerCone K)).π.app j =
    c.π.app j

Tactic:
rcases j with (_ | _) <;>
            simp only [Category.comp_id, PreservesPullback.iso_inv_fst, Cone.ofFork_π, G.map_comp,
              PreservesPullback.iso_inv_fst_assoc, Functor.mapCone_π_app, eqToHom_refl,
              Category.assoc, Fork.ofι_π_app, pullback.lift_fst, pullback.lift_fst_assoc]

Goal state after:
case one
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) = c.π.app WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)

Tactic:
by rw [← F.map_comp, q.rightSection_π, F.map_id]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
this : Module.rank K (Dual K (Dual K V)) < Module.rank K (Dual K (Dual K V))
heq : lift.{max u_5 u_4, u_5} (Module.rank K V) = lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V)))
⊢ False

Tactic:
exact lt_irrefl _ this

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
⊢ False

Tactic:
have h := sub_eq_zero.mpr (sub_eq_zero.mp hz).symm
    rw [sub_eq_add_neg, ← neg_smul, add_comm] at h
    exact (Ne.symm (ne_of_lt (hp x hx))) (LinearIndependent.eq_zero_of_pair hL h).2

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ f.ker.dualAnnihilator = ⊥.dualAnnihilator ↔ Function.Injective ⇑f

Tactic:
Subspace.dualAnnihilator_inj,

Goal state after:
K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ f.ker = ⊥ ↔ Function.Injective ⇑f
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ Codisjoint W W'
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ Codisjoint (dualAnnihilator W) (dualAnnihilator W')

Tactic:
codisjoint_iff

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ (Iso.refl (KernelFork.ofι (Fork.ι (KernelFork.ofι (F.map f) ⋯)) ⋯).pt).hom ≫
      Fork.ι ((Cone.postcomposeEquivalence (compNatIso F)).functor.obj (F.mapCone (KernelFork.ofι f ⋯))) =
    Fork.ι (KernelFork.ofι (Fork.ι (KernelFork.ofι (F.map f) ⋯)) ⋯)

Tactic:
by simp [compNatIso, Fork.ι]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ (map (↑(Finsupp.llift F F F ι)) (span F (Set.range (flip f)))).dualCoannihilator = (Finsupp.linearCombination F f).ker

Tactic:
SetLike.ext'_iff,

Goal state after:
ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ ↑(map (↑(Finsupp.llift F F F ι)) (span F (Set.range (flip f)))).dualCoannihilator =
    ↑(Finsupp.linearCombination F f).ker
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
⊢ s.snd ≫ b ≫ f = s.fst ≫ a ≫ f

Tactic:
by rw [PullbackCone.condition_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: 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
w : Dual R N ⊗[R] Dual R M
z : M ⊗[R] N
⊢ ((dualDistrib R N M) w) ((TensorProduct.comm R M N) z) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) w)) z

Tactic:
induction w <;> induction z <;> simp_all [mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ prod.lift (𝟙 X) 0 ≫ prod.map f f ≫ σ = prod.lift (𝟙 X) 0 ≫ σ ≫ g

Tactic:
by rw [← hg, CokernelCofork.π_ofπ]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
hvu :
  f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
huu :
  f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
s : Cofork f g
m : (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).pt ⟶ s.pt
h : (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).π ≫ m = s.π
⊢ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) ≫ m =
    pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) ≫ pushout.desc s.π s.π ⋯

Tactic:
by simpa only [pushout.inl_desc] using! h

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f ⋯).pt
hg : g ≫ f = Fork.ι A
⊢ g ≫ f = (limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫ f

Tactic:
hg,

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫ Fork.ι (KernelFork.ofι f ⋯) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f ⋯).pt
hg : g ≫ f = Fork.ι A
⊢ Fork.ι A = (limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫ f