mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁵ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝³ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
⊢ ∀ {X' X : SheafOfModules S} {Y : SheafOfModules R} (f : X' ⟶ X) (g : X ⟶ (pushforward φ).obj Y),
    (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
                ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X')) Y).trans
            (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X'.val Y.val).trans
              (fullyFaithfulForget S).homEquiv.symm)).symm
        (f ≫ g) =
      (forget S ⋙ PresheafOfModules.pullback φ.hom ⋙ PresheafOfModules.sheafification (𝟙 R.obj)).map f ≫
        (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
                  ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X)) Y).trans
              (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X.val Y.val).trans
                (fullyFaithfulForget S).homEquiv.symm)).symm
          g

Tactic:
intros

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
D' : Type u₃
inst✝⁵ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁴ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝³ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝² : (PresheafOfModules.pushforward φ.hom).IsRightAdjoint
inst✝¹ : HasWeakSheafify K AddCommGrpCat
inst✝ : K.WEqualsLocallyBijective AddCommGrpCat
X'✝ X✝ : SheafOfModules S
Y✝ : SheafOfModules R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (pushforward φ).obj Y✝
⊢ (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
              ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X'✝)) Y✝).trans
          (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X'✝.val Y✝.val).trans
            (fullyFaithfulForget S).homEquiv.symm)).symm
      (f✝ ≫ g✝) =
    (forget S ⋙ PresheafOfModules.pullback φ.hom ⋙ PresheafOfModules.sheafification (𝟙 R.obj)).map f✝ ≫
      (((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).homEquiv
                ((PresheafOfModules.pullback φ.hom).obj ((forget S).obj X✝)) Y✝).trans
            (((PresheafOfModules.pullbackPushforwardAdjunction φ.hom).homEquiv X✝.val Y✝.val).trans
              (fullyFaithfulForget S).homEquiv.symm)).symm
        g✝
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
h : ¬f = 0
⊢ False

Tactic:
exact w (isIso_of_mono_of_nonzero h)

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f → f ≠ 0

Tactic:
intros

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
⊢ f ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ Simple X

Tactic:
by
  constructor; intro Y f hf; constructor
  · intro i
    rw [Subobject.isIso_iff_mk_eq_top] at i
    intro w
    rw [← Subobject.mk_eq_bot_iff_zero] at w
    exact IsSimpleOrder.bot_ne_top (w.symm.trans i)
  · intro i
    rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)
    · rw [Subobject.mk_eq_bot_iff_zero] at h
      exact False.elim (i h)
    · exact (Subobject.isIso_iff_mk_eq_top _).mpr h

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.fst

Tactic:
intros

Goal state after:
C : Type u
inst✝ : SemilatticeInf C
X Y : C
s✝ : BinaryFan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.fst
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.snd

Tactic:
intros

Goal state after:
C : Type u
inst✝ : SemilatticeInf C
X Y : C
s✝ : BinaryFan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.snd
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y) (m : s.pt ⟶ X ⊓ Y), m ≫ homOfLE ⋯ = s.fst → m ≫ homOfLE ⋯ = s.snd → m = homOfLE ⋯

Tactic:
intros

Goal state after:
C : Type u
inst✝ : SemilatticeInf C
X Y : C
s✝ : BinaryFan X Y
m✝ : s✝.pt ⟶ X ⊓ Y
x✝¹ : m✝ ≫ homOfLE ⋯ = s✝.fst
x✝ : m✝ ≫ homOfLE ⋯ = s✝.snd
⊢ m✝ = homOfLE ⋯
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inl

Tactic:
intros

Goal state after:
C : Type u
inst✝ : SemilatticeSup C
X Y : C
s✝ : BinaryCofan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.inl
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inr

Tactic:
intros

Goal state after:
C : Type u
inst✝ : SemilatticeSup C
X Y : C
s✝ : BinaryCofan X Y
⊢ homOfLE ⋯ ≫ homOfLE ⋯ = s✝.inr
Module: Mathlib.CategoryTheory.Limits.Preorder

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y) (m : X ⊔ Y ⟶ s.pt), homOfLE ⋯ ≫ m = s.inl → homOfLE ⋯ ≫ m = s.inr → m = homOfLE ⋯

Tactic:
intros

Goal state after:
C : Type u
inst✝ : SemilatticeSup C
X Y : C
s✝ : BinaryCofan X Y
m✝ : X ⊔ Y ⟶ s✝.pt
x✝¹ : homOfLE ⋯ ≫ m✝ = s✝.inl
x✝ : homOfLE ⋯ ≫ m✝ = s✝.inr
⊢ m✝ = homOfLE ⋯
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
⊢ ∀ (x y : (i : ι) → φ i), (fun i ↦ (x + y) (f i)) = (fun i ↦ x (f i)) + fun i ↦ y (f i)

Tactic:
intros

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
x✝ y✝ : (i : ι) → φ i
⊢ (fun i ↦ (x✝ + y✝) (f i)) = (fun i ↦ x✝ (f i)) + fun i ↦ y✝ (f i)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
⊢ ∀ (m : R) (x : (i : ι) → φ i), (fun i ↦ (m • x) (f i)) = (RingHom.id R) m • fun i ↦ x (f i)

Tactic:
intros

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
α : Type u_6
f : α → ι
m✝ : R
x✝ : (i : ι) → φ i
⊢ (fun i ↦ (m✝ • x✝) (f i)) = (RingHom.id R) m✝ • fun i ↦ x✝ (f i)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
⊢ ∀ (S : ShortComplex (TopModuleCat R)), S.HasHomology

Tactic:
intro S

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
⊢ S.HasHomology
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : Semigrp} {Y : MonCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ MonCat Semigrp).obj Y),
    (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f ≫ g) =
      adjoinOne.map f ≫
        (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g

Tactic:
intros

Goal state after:
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝) =
    adjoinOne.map f✝ ≫
      (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ (↑e ∘SL f).IsInvertible → f.IsInvertible

pp: case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ f.IsInvertible → (↑e ∘SL f).IsInvertible

Tactic:
· rintro ⟨A, hA⟩
    have : f = e.symm ∘L ((e : M₂ →L[R] M₃) ∘L f) := by ext; simp
    rw [this, ← hA]
    simp

Goal state after:
case mpr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ f.IsInvertible → (↑e ∘SL f).IsInvertible
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : M ≃L[R] M
⊢ (↑e)⁻¹ʳ = (↑e).inverse

Tactic:
suffices ((ContinuousLinearEquiv.unitsEquiv _ _).symm e : M →L[R] M)⁻¹ʳ = inverse ↑e by
    convert! this
  simp
  rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i j : J
f : D.obj i ⟶ X
g : D.obj j ⟶ X
h : c.π.app i ≫ f = c.π.app j ≫ g
⊢ ∃ k u v, D.map u ≫ f = D.map v ≫ g

Tactic:
obtain ⟨k, u, v, huv⟩ :=
    (Types.FilteredColimit.isColimit_eq_iff _ (isColimitOfPreserves (yoneda.obj X) hc.op)).mp h

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i j : J
f : D.obj i ⟶ X
g : D.obj j ⟶ X
h : c.π.app i ≫ f = c.π.app j ≫ g
k : Jᵒᵖ
u : op i ⟶ k
v : op j ⟶ k
huv : (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map u)) f = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map v)) g
⊢ ∃ k u v, D.map u ≫ f = D.map v ≫ g
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i j : J
f : D.obj i ⟶ X
g : D.obj j ⟶ X
h : c.π.app i ≫ f = c.π.app j ≫ g
k : Jᵒᵖ
u : op i ⟶ k
v : op j ⟶ k
huv : (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map u)) f = (ConcreteCategory.hom ((D.op ⋙ yoneda.obj X).map v)) g
⊢ ∃ k u v, D.map u ≫ f = D.map v ≫ g

Tactic:
exact ⟨k.unop, u.unop, v.unop, huv⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ (z₁ - z₂) = g₁ (i₁ d)
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂

Tactic:
(HasLeftInverse.injective ⟨ρ, congr_fun hρ⟩).eq_iff

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : z₁ - z₂ = i₁ d
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
⊢ ∀ (xi : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i))
    (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) xi =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj

Tactic:
f₁

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ coyoneda.obj (Opposite.op S)).obj i
⊢ ∀ (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) f₁ =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) f₁ =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
⊢ Y.hom = hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }

Tactic:
refine hd.hom_ext fun j ↦ ?_

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
hd : IsColimit ((proj L X ⋙ L).mapCocone d.cocone) := isColimitOfPreserves (proj L X ⋙ L) d.isColimit
j : J
⊢ ((proj L X ⋙ L).mapCocone d.cocone).ι.app j ≫ Y.hom =
    ((proj L X ⋙ L).mapCocone d.cocone).ι.app j ≫
      hd.desc { pt := X, ι := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
⊢ ∀ {X_1 Y_1 : PullbackCone f g} (f_1 : X_1 ⟶ Y_1),
    (𝟭 (PullbackCone f g)).map f_1 ≫ Y_1.eta.hom =
      X_1.eta.hom ≫
        ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
                map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
                map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
          f_1

Tactic:
intros

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
X✝ Y✝ : PullbackCone f g
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 (PullbackCone f g)).map f✝ ≫ Y✝.eta.hom =
    X✝.eta.hom ≫
      ({ obj := fun c ↦ BinaryFan.mk (Over.homMk c.fst ⋯) (Over.homMk c.snd ⋯),
              map := fun {c₁ c₂} a ↦ { hom := Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun c ↦ PullbackCone.mk (Over.Hom.left c.fst) (Over.Hom.left c.snd) ⋯,
              map := fun {c₁ c₂} a ↦ { hom := Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).map
        f✝
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.cone) := isLimitOfPreserves (proj X L ⋙ L) d.isLimit
⊢ Y.hom = hd.lift { pt := X, π := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } }

Tactic:
refine hd.hom_ext fun j ↦ ?_

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
hd : IsLimit ((proj X L ⋙ L).mapCone d.cone) := isLimitOfPreserves (proj X L ⋙ L) d.isLimit
j : J
⊢ Y.hom ≫ ((proj X L ⋙ L).mapCone d.cone).π.app j =
    hd.lift { pt := X, π := { app := fun j ↦ (d.diag.obj j).hom, naturality := ⋯ } } ≫
      ((proj X L ⋙ L).mapCone d.cone).π.app j
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝¹ : _root_.Finite J
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres : ∀ (j : Discrete J), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅ R.mkUnder ((i : J) → ↑(pres.diag.obj { as := i }).right) :=
  (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }).symm ≪≫
    HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso ⋯) ≪≫
      limit.isoLimitCone
        { cone := CommRingCat.Under.piFan fun i ↦ pres.diag.obj { as := i },
          isLimit := CommRingCat.Under.piFanIsLimit fun i ↦ pres.diag.obj { as := i } }
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ Q)
    ((R.mkUnder ((i : J) → ↑(pres.diag.obj { as := i }).right)).hom ≫ Under.Hom.right e.inv)

Tactic:
(toMorphismProperty Q).cancel_right_of_respectsIso

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
R : CommRingCat
J : Type u
x✝¹ : _root_.Finite J
A : Under R
x✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj.limitsOfShape (Discrete J) A
pres : LimitPresentation (Discrete J) A
hpres : ∀ (j : Discrete J), (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj (pres.diag.obj j)
e : A ≅ R.mkUnder ((i : J) → ↑(pres.diag.obj { as := i }).right) :=
  (limit.isoLimitCone { cone := { pt := A, π := pres.π }, isLimit := pres.isLimit }).symm ≪≫
    HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso ⋯) ≪≫
      limit.isoLimitCone
        { cone := CommRingCat.Under.piFan fun i ↦ pres.diag.obj { as := i },
          isLimit := CommRingCat.Under.piFanIsLimit fun i ↦ pres.diag.obj { as := i } }
this : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ toMorphismProperty (fun {R S} [CommRing R] [CommRing S] ↦ Q)
    (R.mkUnder ((i : J) → ↑(pres.diag.obj { as := i }).right)).hom
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
p : ℕ
inst✝ : CharP R p
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x

Tactic:
by
    rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]

Goal state after: