mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_4
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (x y : MvPolynomial (Fin n) A),
    x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) →
      y ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) →
        x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid →
          y ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid →
            x * y ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
· intro x₁ x₂ _ _ h₁ h₂
        obtain ⟨_, ⟨p₁, rfl⟩, q₁, hq₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
        obtain ⟨_, ⟨p₂, rfl⟩, q₂, hq₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
        rw [add_mul, mul_add, add_assoc, ← map_mul]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · refine add_mem (Ideal.mul_mem_left _ _ hq₂) (Ideal.mul_mem_right _ _ hq₁)

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
by
    refine ⟨isColimitExtendCoconeEquiv (G := G ⋙ H) F (H.mapCocone c) ?_⟩
    let hc' := isColimitOfPreserves H ((isColimitExtendCoconeEquiv F c).symm hc)
    exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
t : Relation.EqvGen (F ⋙ coyoneda.obj (op d)).ColimitTypeRel ⟨X₁, f₁⟩ ⟨X₂, f₂⟩
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
exact Final.zigzag_of_eqvGen_colimitTypeRel t

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cocone D
hc : IsColimit c
j : J
inst✝ : (Under.forget j).Final
this : Nonempty (Under j)
⊢ IsColimit (c.underPost j)

Tactic:
letI c'' := Under.liftCocone (CategoryTheory.Under.forget j ⋙ D) (X := D.obj j)
    ((Functor.constComp _ _ _).inv ≫ Functor.whiskerRight ((Under.forgetCone j).π) D)
    (c.whisker (CategoryTheory.Under.forget j)) (c.ι.app j) (by cat_disch)

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
D : J ⥤ C
c : Cocone D
hc : IsColimit c
j : J
inst✝ : (Under.forget j).Final
this : Nonempty (Under j)
c'' : Cocone
  (Under.lift (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)) :=
  Under.liftCocone (Under.forget j ⋙ D)
    ((Functor.constComp (Under j) j D).inv ≫ Functor.whiskerRight (Under.forgetCone j).π D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
⊢ IsColimit (c.underPost j)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ P.RespectsIso

Tactic:
apply RespectsIso.of_respects_arrow_iso

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ ∀ (f g : Arrow C) (x : f ≅ g), P f.hom → P g.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ CommSq (fst f g ≫ f) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)

Tactic:
constructor
    ext <;> simp [condition]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝³ : P.ContainsZero
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
Z : C
h₁ : IsZero Z
h₂ : P Z
⊢ ∃ Z, IsZero Z ∧ P.map F Z

Tactic:
exact ⟨F.obj Z, F.map_isZero h₁, P.prop_map_obj F h₂⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ∀ {X Y : C} (x : Retract X Y), P.retractClosure Y → P.retractClosure X

Tactic:
by
    rintro X Y r₁ ⟨Z, hZ, ⟨r₂⟩⟩
    refine ⟨Z, hZ, ⟨r₁.trans r₂⟩⟩

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

Goal state before:
pp: case h₀.h₀.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₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (fst f' g') i₁ ≫ fst f' g'

Tactic:
condition

Goal state after:
case h₀.h₀.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₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁.h₀.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₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (fst f' g') i₁ ≫ fst f' g'

Tactic:
condition

Goal state after:
case h₁.h₀.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₃
⊢ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁ =
    fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁ ≫ i₁
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₃
⊢ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂ ≫ snd f' g'

Tactic:
condition

Goal state after:
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₃
⊢ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂ =
    snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂ ≫ i₂
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ∀ {X Y Z : C} (e : X ≅ Y) (f : Y ⟶ Z), P.universally f → P.universally (e.hom ≫ f)

Tactic:
intro X Y Z e f hf X' Z' i₁ i₂ f' H
    have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv :=
      IsPullback.of_horiz_isIso
        ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩
    exact hf _ _ _
      (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H)

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

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

Tactic:
lift_comp_inv_left,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (lift (toUnit (A ⊗ A) ≫ η) (snd A A) ≫ μ) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = lift (snd A A ≫ ι) (snd A A) ≫ μ

Tactic:
lift_comp_inv_left,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : GrpObj A
⊢ μ ≫ toUnit A ≫ η = toUnit (A ⊗ A) ≫ η
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 μ μ
this : lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ = lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ ι) ≫ μ
⊢ lift (s.snd ≫ snd A A) (lift ((s.fst ≫ snd A A) ≫ ι) (s.fst ≫ snd A A) ≫ μ) ≫ μ = s.snd ≫ snd A A

Tactic:
lift_comp_inv_left,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
this : lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ = lift (s.snd ≫ snd A A) (s.fst ≫ snd A A ≫ ι) ≫ μ
⊢ lift (s.snd ≫ snd A A) (toUnit s.pt ≫ η) ≫ μ = s.snd ≫ snd A A
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      (α_ X (𝟙_ C) ((ihom Y).obj Z)).inv ≫ (X ◁ curry' f ≫ (ihom.ev X).app Y) ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z

Tactic:
whiskerLeft_curry'_ihom_ev_app,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
⊢ X ◁ (λ_ ((ihom Y).obj Z)).inv ≫
      (α_ X (𝟙_ C) ((ihom Y).obj Z)).inv ≫ ((ρ_ X).hom ≫ f) ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z =
    f ▷ (ihom Y).obj Z ≫ (ihom.ev Y).app Z
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫
      (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ Y ◁ curry' f ≫ (ihom.ev Y).app Z =
    (ihom.ev X).app Y ≫ f

Tactic:
whiskerLeft_curry'_ihom_ev_app,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ X ◁ (ρ_ ((ihom X).obj Y)).inv ≫ (α_ X ((ihom X).obj Y) (𝟙_ C)).inv ≫ (ihom.ev X).app Y ▷ 𝟙_ C ≫ (ρ_ Y).hom ≫ f =
    (ihom.ev X).app Y ≫ f
Module: Mathlib.Logic.Equiv.Finset

Goal state before:
pp: l : List ℕ
m n : ℕ
h : m < n
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2)
    (m ::
      match l, n with
      | [], x => []
      | m :: l, n => (m + n) :: raise' l (m + n + 1))

Tactic:
cases l with

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
x : WType (Operands s)
⊢ -WType.elim (↥(closure s)) (operate s) x ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
exact ⟨WType.mk (.inl 2) fun _ ↦ x, rfl⟩

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ {x : ↥(closure s)},
    x ∈ Set.range (WType.elim (↥(closure s)) (operate s)) → -x ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
by rintro _ ⟨x, rfl⟩; exact ⟨WType.mk (.inl 2) fun _ ↦ x, rfl⟩

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₁ X₂ Y₁ Y₂ : C
inst✝¹ : ExactPairing X₁ Y₁
inst✝ : ExactPairing X₂ Y₂
⊢ (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ ((Y₁ ⊗ X₁) ◁ η_ X₂ Y₂ ≫ ε_ X₁ Y₁ ▷ (X₂ ⊗ Y₂)) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁) =
    (Y₂ ⊗ Y₁) ◁ η_ X₁ Y₁ ⊗≫ Y₂ ◁ (ε_ X₁ Y₁ ▷ 𝟙_ C ≫ 𝟙_ C ◁ η_ X₂ Y₂) ▷ Y₁ ⊗≫ ε_ X₂ Y₂ ▷ (Y₂ ⊗ Y₁)

Tactic:
by
        rw [whisker_exchange]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      toLinearMapRight'.toEquiv a ∘ₗ toLinearMapRight'.toEquiv a_1 = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
LinearEquiv.coe_toEquiv,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      toLinearMapRight' a ∘ₗ toLinearMapRight' a_1 = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R₁ M₁
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
⊢ B.IsOrtho 0 x

Tactic:
dsimp only [IsOrtho]
  rw [map_zero B, zero_apply]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
⊢ -(B x) y = (B y) x

Tactic:
have H1 : B (y + x) (y + x) = 0 := self_eq_zero H (y + x)

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
H1 : (B (y + x)) (y + x) = 0
⊢ -(B x) y = (B y) x
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' ((f - f') x)) x✝ = (B x) ((g - g') x✝)

Tactic:
rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']

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

Goal state before:
pp: V : Type uV
inst✝³ : AddCommMonoid V
R : Type u_1
inst✝² : Semiring R
inst✝¹ : Module R V
inst✝ : Projective R V
v : V
h : ∀ (φ : Dual R V), φ v = 0
⊢ v = 0

Tactic:
contrapose! h

Goal state after:
V : Type uV
inst✝³ : AddCommMonoid V
R : Type u_1
inst✝² : Semiring R
inst✝¹ : Module R V
inst✝ : Projective R V
v : V
h : v ≠ 0
⊢ ∃ φ, φ v ≠ 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case refine_3.left
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one

pp: case refine_3.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one

Tactic:
· simp only [BinaryCofan.ι_app_left, BinaryCofan.mk_inl, ←
              G.map_comp_assoc, coprod.inl_desc]

Goal state after:
case refine_3.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one
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
h : (B x) x • y + -((B x) y • x) = 0
⊢ False

Tactic:
← neg_smul,

Goal state after:
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
h : (B x) x • y + -(B x) y • x = 0
⊢ False
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = s.ι
x : ↑s.pt
⊢ ↑((Hom.hom m) x) = ↑((Hom.hom (↟(LinearMap.codRestrict (Hom.hom f).ker (Hom.hom s.ι) ⋯))) x)

Tactic:
simp [← h]

Goal state after:
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
s : Fork f 0
m : s.pt ⟶ (kernelCone f).pt
h : m ≫ Fork.ι (kernelCone f) = s.ι
x : ↑s.pt
⊢ ↑((Hom.hom m) x) =
    ↑((Hom.hom (↟(LinearMap.codRestrict (Hom.hom f).ker (Hom.hom (Fork.ι (kernelCone f)) ∘ₗ Hom.hom m) ⋯))) x)
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ G.map (i ≫ s) = G.map (i ≫ t)

Tactic:
apply congrArg G.map

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : P ⟶ Q := ⋯
t : P ⟶ Q := ⋯
I : C := ⋯
i : I ⟶ P := ⋯
⊢ i ≫ s = i ≫ t
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : P ⟶ Q := ⋯
t : P ⟶ Q := ⋯
I : C := ⋯
i : I ⟶ P := ⋯
⊢ i ≫ s = i ≫ t

Tactic:
exact equalizer.condition s t

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ IsLimit (G.mapCone c) ≃ IsLimit (c.map G)

Tactic:
refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
  refine parallelPair.ext (Iso.refl _) (Iso.refl _) ?_ ?_ <;> simp
  exact Cone.ext (Iso.refl _) (by rintro (_ | _) <;> cat_disch)

Goal state after: