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

Goal state before:
pp: case refine_3
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)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ adjoin R (Set.range MvPolynomial.X) →
      y ∈ adjoin R (Set.range MvPolynomial.X) →
        x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
          y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
            x + y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
intro _

Goal state after:
case refine_3
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)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x✝ : RXn
⊢ ∀ (y : RXn),
    x✝ ∈ adjoin R (Set.range MvPolynomial.X) →
      y ∈ adjoin R (Set.range MvPolynomial.X) →
        x✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
          y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
            x✝ + y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
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.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
⊢ LiftableCone G H c

Tactic:
refine ⟨(extendCone (F := F)).obj (liftLimit ((isLimitWhiskerEquiv F _).symm hc)), ?_⟩
    let i := liftedLimitMapsToOriginal (K := (F ⋙ G)) ((isLimitWhiskerEquiv F _).symm hc)
    refine ?_ ≪≫ ((extendCone (F := F)).mapIso i) ≪≫ ((conesEquiv F (G ⋙ H)).counitIso.app _)
    exact Cone.ext (Iso.refl _)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (z ≫ v) ≫ h.left = z ≫ v ≫ h.right

Tactic:
← eq_whisker sq.w

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = z ≫ v ≫ h.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ z ≫ v ≫ h.left = z ≫ v ≫ h.right

Tactic:
rw [← Category.assoc, ← eq_whisker sq.w]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = z ≫ v ≫ h.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (z ≫ v) ≫ h.right

Tactic:
← eq_whisker sq.w

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = z ≫ v ≫ h.right

Tactic:
rw [← Category.assoc, ← eq_whisker sq.w]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right

Tactic:
rw [← Category.assoc, ← eq_whisker sq.w]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FinitePresentation
this : Algebra R S := f.toAlgebra
⊢ Q R S f

Tactic:
obtain ⟨n, g, hg, hg'⟩ := hf

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
hg : Surjective ⇑g
hg' : (ker g.toRingHom).FG
⊢ Q R S f
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✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
g₁ : Z ⟶ X
⊢ ∀ (h : Z ⟶ X), g₁ ≫ f = h ≫ f → g₁ = h

Tactic:
g₂

Goal state after:
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✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
g₁ g₂ : Z ⟶ X
⊢ g₁ ≫ f = g₂ ≫ f → g₁ = g₂
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
⊢ ∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X}, IsPullback f' g' g f → P g → P g'

Tactic:
intro _

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ : C
⊢ ∀ {Y Y' S : C} {f : X✝ ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X✝}, IsPullback f' g' g f → P g → P g'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
⊢ ∀ {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'}, IsPushout g f f' g' → P f → P f'

Tactic:
intro _

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pushouts ≤ P
A✝ : C
⊢ ∀ {A' B B' : C} {f : A✝ ⟶ A'} {g : A✝ ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'}, IsPushout g f f' g' → P f → P f'
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
⊢ W.colimitsOfShape J' ≤ W.colimitsOfShape J

Tactic:
intro _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), W.colimitsOfShape J' f → W.colimitsOfShape J f
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 ↦ K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x ↦
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 ↦ K.obj { as := n_1 }).obj { as := i })
this : PreservesLimit (Discrete.functor fun n_1 ↦ K.obj { as := n_1 }) F
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_iso_diagram F that

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
⊢ (ofObj Y).isoClosure y

Tactic:
have hri : (h a).r ≫ (h a).i = r.r ≫ r.i := by
      rw [Sigma.ext_iff, heq_eq_eq] at h₂
      exact Subtype.ext_iff.1 h₂.2

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : LocallySmall.{w, v, u} C
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁✝ : Q ≤ P
h₂✝ : P ≤ Q.isoClosure
α : Type (max u v) := (X : Subtype Q) × { p // p ≫ p = p }
g : {X Y : C} → Retract Y X → Q X → α := fun {X Y} h hX ↦ ⟨⟨X, hX⟩, ⟨h.r ≫ h.i, ⋯⟩⟩
R : α → Prop := fun a ↦ ∃ X Y h, ∃ (hX : Q X), g h hX = a
X Y : Subtype R → C
h : (a : Subtype R) → Retract (Y a) (X a)
hX : ∀ (a : Subtype R), ∃ (hX : Q (X a)), g (h a) hX = ↑a
y : C
a : Subtype R
h₁ hx : Q (X a)
r : Retract y (X a)
h₂ : g (h a) h₁ = g r hx
hri : (h a).r ≫ (h a).i = r.r ≫ r.i
⊢ (ofObj Y).isoClosure y
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ coproducts.{w, v, u} W f ↔ ∃ J, W.colimitsOfShape (Discrete J) f

Tactic:
simp only [coproducts, iSup_iff]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x ↦ X₁) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₁)
c₂ : Cocone (Discrete.functor fun x ↦ X₂) := coconeOfDiagramInitial h (Discrete.functor fun x ↦ X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x : Discrete PUnit.{w + 1}
⊢ c₁.ι.app x ≫ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x ↦ f) ≫ c₂.ι } = c₁.ι.app x ≫ f

Tactic:
obtain rfl : x = ⊥_ _ := by ext
      rw [IsColimit.fac]
      simp [c₁, c₂]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q ↔ P ≤ Q

Tactic:
constructor
  · exact le_trans P.le_coproducts
  · intro h
    exact le_trans (coproducts_monotone h) Q.coproducts_le

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
A : Type u_3
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
a : C
𝓡 : Coalgebra.Repr R a ι
f g : WithConv (C →ₗ[R] A)
⊢ (f * g).ofConv a = ∑ i ∈ 𝓡.index, f.ofConv (𝓡.left i) * g.ofConv (𝓡.right i)

Tactic:
simp [convMul_def, ← 𝓡.eq]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ Function.Injective (@toMonObj C inst✝¹ inst✝ X)

Tactic:
intro h₁ h₂ e
  suffices h₁.inv = h₂.inv by cases h₁; congr!
  apply lift_left_mul_ext (𝟙 _)
  rw [left_inv]
  convert! @left_inv _ _ _ _ h₁ using 2
  exacts [congr(($e.symm).mul), congr(($e.symm).one)]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u_1
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
  rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h
  have e := (b.constr Kᵐᵒᵖ (M' := K)).symm.trans
    (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Kᵐᵒᵖ)
  rw [e.rank_eq, e.toEquiv.cardinal_eq]
  apply rank_fun_infinite

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
⊢ B.IsAdjointPair B' ⇑f ⇑g

Tactic:
intro _

Goal state after:
case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x✝ : M
⊢ ∀ (y : M₁), (B' (f x✝)) y = (B x✝) (g y)
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
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left = pullbackFst F ≫ F.map WalkingParallelPairHom.right

Tactic:
conv_rhs => rw [pullbackFst_eq_pullback_snd]

Goal state after:
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
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left =
    pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: 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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = r * r * s * s * ((B x) y * (B y) x)
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]

Goal state after:
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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = r * r * s * s * ((B x) y * (B y) x)
hrs : r * r * s * s ≠ 0
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x
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₁
⊢ dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
refine le_antisymm ?_ (sup_dualAnnihilator_le_inf W W')

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₁
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_4
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
← h.iInf_comp,

Goal state after:
case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_4
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ dualAnnihilator (⨅ x, W (h x)) = ⨆ i, dualAnnihilator (W i)
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
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (G.mapCone (Fork.ofι (kernel.ι f) ⋯))

Tactic:
apply (isLimitMapConeForkEquiv' G (kernel.condition f)).symm _

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : HasZeroMorphisms C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
i : IsIso (kernelComparison f G)
⊢ IsLimit (KernelFork.ofι (G.map (kernel.ι f)) ⋯)
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
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ (iso G f).inv = cokernelComparison f G

Tactic:
rw [← cancel_epi (cokernel.π _)]

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G
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 : C
f g : X ⟶ Y
huv : pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) = pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)
hvu :
  pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f = pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g
huu :
  pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ f = pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ g
s : Fork f g
m : s.pt ⟶ (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).pt
h : m ≫ (Fork.ofι (pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)) huu).ι = s.ι
⊢ m ≫ pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) =
    pullback.lift s.ι s.ι ⋯ ≫ pullback.snd (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)

Tactic:
by simpa only [huv.symm, pullback.lift_fst] using! h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ x = 0

Tactic:
apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) := ⋯
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ x ≫ prod.lift (𝟙 A) 0 = 0 ≫ prod.lift (𝟙 A) 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ m = s.ι ≫ prod.fst

Tactic:
apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
this : Mono (prod.lift (𝟙 A) 0)
⊢ m ≫ prod.lift (𝟙 A) 0 = (s.ι ≫ prod.fst) ≫ prod.lift (𝟙 A) 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift a 0 ≫ σ = a

Tactic:
conv_lhs =>
    congr; congr; rw [← Category.comp_id a]
    case a.g => rw [show 0 = a ≫ (0 : Y ⟶ Y) by simp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ prod.lift (a ≫ 𝟙 Y) (a ≫ 0) ≫ σ = a