mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Pairwise

Goal state before:
pp: ι : Type v
α : Type u
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ ∀ b ∈ Set.range U, b ≤ s.pt

Tactic:
rintro _ ⟨j, rfl⟩

Goal state after:
ι : Type v
α : Type u
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
j : ι
⊢ U j ≤ s.pt
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
Y : D
⊢ Sieve.functorPullback G (Sieve.ofObjects P.X (G.obj Y)) ≤ Sieve.ofObjects (fun i ↦ i.fst) Y

Tactic:
intro Z

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁸ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝⁷ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝⁵ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁴ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝³ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝² : G.IsContinuous K J
inst✝¹ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (SheafOfModules.pushforward φ).obj (unit R) ≅ unit S
inst✝ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
h :
  ∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (SheafOfModules.pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
M : SheafOfModules R
P : M.QuasicoherentData
Y Z : D
⊢ ∀ (f : Z ⟶ Y),
    (Sieve.functorPullback G (Sieve.ofObjects P.X (G.obj Y))).arrows f → (Sieve.ofObjects (fun i ↦ i.fst) Y).arrows f
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
⊢ ∀ (x_1 : ↑X) (hx : x_1 ∈ V x ⊓ V y),
    (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V y)).op)) (sf x)) =
      (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLERight (V y)).op)) (sf y))

Tactic:
intro z hz

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
z : ↑X
hz : z ∈ V x ⊓ V y
⊢ (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) z hz))
      ((ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V y)).op)) (sf x)) =
    (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) z hz))
      ((ConcreteCategory.hom (F.obj.map ((V x).infLERight (V y)).op)) (sf y))
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ↑T (↑T⁻¹ x) = x

Tactic:
by rw [← mul_apply_eq_comp, Units.mul_inv, one_apply_eq_self]

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
f : X ⟶ Y
x✝ : IsIso ((forget Semigrp).map f)
i : (forget Semigrp).obj X ≅ (forget Semigrp).obj Y := asIso ((forget Semigrp).map f)
e : ↑X ≃* ↑Y :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := __src.toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact e.toSemigrpIso.isIso_hom

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e ∘ ⇑e.symm = id

Tactic:
ext x
  exact apply_symm_apply e x

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ (TensorProduct.map g (AlgHom.id R S)) (s ⊗ₜ[R] 1) = 1 ⊗ₜ[R] s

Tactic:
sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ (TensorProduct.map g (AlgHom.id R S)) (1 ⊗ₜ[R] s) = 1 ⊗ₜ[R] s
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²² : Semiring R
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommMonoid V
inst✝¹⁹ : Module R V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : Module S V
inst✝¹⁶ : ContinuousConstSMul S V
inst✝¹⁵ : AddCommMonoid W
inst✝¹⁴ : Module R W
inst✝¹³ : TopologicalSpace W
inst✝¹² : Module S W
inst✝¹¹ : ContinuousConstSMul S W
inst✝¹⁰ : AddCommMonoid G
inst✝⁹ : Module R G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module S G
inst✝⁶ : ContinuousConstSMul S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ (α • e).trans f = α • e.trans f

Tactic:
by
  ext; simp [LinearMapClass.map_smul_of_tower f]

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

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
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
obtain ⟨s, γ, δ, h₁, h₂⟩ := IsFiltered.bowtie
    (IsFiltered.leftToMax i₀ j) β (IsFiltered.rightToMax i₀ j) α
  dsimp [coconeιApp]
  rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_id_assoc]

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

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
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ h.coconeιApp j ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i

Tactic:
h.coconeιApp_eq j _ β α,

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
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ (F.map β ≫ (h.isoMap α ⋯).inv) ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
wlog hR' : Q' R generalizing R

Goal state after:
case inr
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
this : ∀ (R : CommRingCat), Q R → ∀ (φ : R ⟶ S), (Hom.hom φ).FiniteType → Q' R → (ObjectProperty.ofObj f).isoClosure S
hR' : ¬Q' R
⊢ (ObjectProperty.ofObj f).isoClosure S

P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
hR' : Q' R
⊢ (ObjectProperty.ofObj f).isoClosure S
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
i : ι
⊢ f i ≫ a ≫ F.map (b (i₀, i) ≫ c (i₀, i)) = f i₀ ≫ a ≫ F.map (b (i₀, i) ≫ c (i₀, i))

Tactic:
Functor.map_comp,

Goal state after:
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : Nonempty ι
l : J₁
a : k ⟶ F.obj l
m : ι × ι → J₁
b : (i : ι × ι) → l ⟶ m i
hb : ∀ (a_1 b_1 : ι), f a_1 ≫ a ≫ F.map (b (a_1, b_1)) = f b_1 ≫ a ≫ F.map (b (a_1, b_1))
n : J₁
c : (i : ι × ι) → m i ⟶ n
d : l ⟶ n
hn : ∀ (i : ι × ι), b i ≫ c i = d
i₀ : ι := Classical.arbitrary ι
i : ι
⊢ f i ≫ a ≫ F.map (b (i₀, i)) ≫ F.map (c (i₀, i)) = f i₀ ≫ a ≫ F.map (b (i₀, i)) ≫ F.map (c (i₀, i))
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B : CommRingCat
inst✝ : TopologicalSpace ↑R
f✝ : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f✝)
this : IsEmbedding fun x ↦ x ∘ ⇑(Hom.hom f✝)
f g : B ⟶ R
e : (↑↑f.hom').1 = (↑↑g.hom').1
⊢ f = g

Tactic:
by ext a; exact congr($e a)

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (f ≫ a ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (f ≫ b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))

Tactic:
reassoc_of% ha,

Goal state after:
case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (α.app i ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (f ≫ b ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case h₁
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
hf : (CommRingCat.Hom.hom f).EssFiniteType
i : J
a : S ⟶ F.obj i
ha : f ≫ a = α.app i
j : J
b : S ⟶ F.obj j
hb : f ≫ b = α.app j
hab : a ≫ c.ι.app i = b ≫ c.ι.app j
hc' : IsColimit ((forget CommRingCat).mapCocone c)
k : ↑S → J
f₁ : (x : ↑S) → i ⟶ k x
f₂ : (x : ↑S) → j ⟶ k x
h :
  ∀ (x : ↑S),
    (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₁ x))) (a.hom' x) =
      (ConcreteCategory.hom ((F ⋙ forget CommRingCat).map (f₂ x))) (b.hom' x)
J' : MulticospanShape := { L := Unit ⊕ Unit, R := ↥hf.finset, fst := fun x ↦ Sum.inl (), snd := fun x ↦ Sum.inr () }
D : MulticospanIndex J' J :=
  { left := Sum.elim (fun x ↦ i) fun x ↦ j, right := fun x ↦ k ↑x, fst := fun x ↦ f₁ ↑x, snd := fun x ↦ f₂ ↑x }
c' : Cocone D.multicospan
⊢ CommRingCat.Hom.hom (α.app i ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inl ())))) =
    CommRingCat.Hom.hom (α.app j ≫ F.map (c'.ι.app (WalkingMulticospan.left (Sum.inr ()))))

Tactic:
simp [← α.naturality]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R S : CommRingCat
inst✝² : Algebra ↑R ↑S
ι : Type u
P : ι → Under R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
⊢ (tensorProductFan S P).proj i =
    (Algebra.TensorProduct.piRight ↑R ↑S ↑S fun i ↦ ↑(P i).right).toUnder.hom ≫ (tensorProductFan' S P).proj i

Tactic:
dsimp only [tensorProductFan, Fan.mk_pt, fan_mk_proj, tensorProductFan']
    apply CommRingCat.mkUnder_ext
    intro c
    induction c
    · simp only [map_zero, Under.comp_right]
    · simp only [AlgHom.toUnder_right, Algebra.TensorProduct.map_tmul, AlgHom.coe_id, id_eq,
        Pi.evalAlgHom_apply, Under.comp_right, comp_apply, AlgEquiv.toUnder_hom_right_apply,
        Algebra.TensorProduct.piRight_tmul]
    · simp_all

Goal state after:
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 : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ m = Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s))

Tactic:
have := hc.uniq (pushoutCoconeEquivBinaryCofan.functor.obj s) (Under.homMk m <| by
        simp [← hm₁, dsimp% c.inl.w_assoc])
        (by rintro (_ | _) <;> ext <;> simpa)

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
this : Under.homMk m ⋯ = hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s)
⊢ m = Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s))
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case hfg
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderBaseChange
f : X ⟶ Y
inst✝² : P.HasPullbacksAlong f
inst✝¹ : P.IsStableUnderBaseChangeAlong f
inst✝ : Q.HasOfPostcompProperty Q
hPf : P f
hQf : Q f
A : P.Over Q X
⊢ Q (pullback.lift (𝟙 ((𝟭 (P.Over Q X)).obj A).left) A.hom ⋯ ≫ pullback.fst ((map Q hPf).obj A).hom f)

Tactic:
simpa using Q.of_isIso _

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

Goal state before:
pp: case hfg
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A : P.Under Q Y
⊢ Q (pushout.inl ((map Q hPf).obj A).hom f ≫ pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯)

Tactic:
simpa using Q.of_isIso _

Goal state after:
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit ↑n
⊢ ¬p ∣ n

Tactic:
by
    have := CharP.nontrivial_of_char_ne_one (R := R) hp.ne_one
    rw [← CharP.cast_eq_zero_iff (R := R)]
    exact h.ne_zero

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
⊢ r ≠ 0

Tactic:
have q_zero :=
        congr_arg (Ideal.Quotient.factor h_IM) (CharP.cast_eq_zero (R ⧸ I) q)

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
I : Ideal R
hI_ne_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) q
M : Ideal R
hM_max : M.IsMaximal
h_IM : I ≤ M
r : ℕ := ringChar (R ⧸ M)
q_zero : (Ideal.Quotient.factor h_IM) ↑q = (Ideal.Quotient.factor h_IM) 0
⊢ r ≠ 0
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k, k • p = z • r) → ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r

pp: case mpr
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k k_1, (z * k_1 + ↑↑k) • p = z • r) → ∃ k, k • p = z • r

Tactic:
· rintro ⟨k, h⟩
    simp_rw [← h]
    refine ⟨⟨(k % z).toNat, ?_⟩, k / z, ?_⟩
    · rw [← Int.ofNat_lt, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
      exact (Int.emod_lt_abs _ hz).trans_eq (Int.abs_eq_natAbs _)
    rw [Fin.val_mk, Int.toNat_of_nonneg (Int.emod_nonneg _ hz)]
    nth_rewrite 3 [← Int.mul_ediv_add_emod k z]
    rfl

Goal state after:
case mpr
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
⊢ (∃ k k_1, (z * k_1 + ↑↑k) • p = z • r) → ∃ k, k • p = z • r
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.destruct = none → s = nil

Tactic:
by
  dsimp [destruct]
  rcases f0 : get? s 0 <;> intro h
  · exact get?_zero_eq_none.mp f0
  · contradiction

Goal state after: