mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
⊢ ∀ ⦃I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve f, ⋯⟩⦄ (r : I₁.Relation I₂),
    (match I₁ with
        | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op) ≫
        F.obj.map r.g₁.op =
      (match I₂ with
        | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op) ≫
        F.obj.map r.g₂.op

Tactic:
by
      rintro ⟨W₀, a, ha⟩ ⟨W₀', a', ha'⟩ ⟨T₀, p₁, p₂, fac⟩
      rw [← Functor.map_comp, ← Functor.map_comp, ← op_comp, ← op_comp]
      apply map_eq_of_eq K G
      rw [Functor.map_comp, Functor.map_comp, ha.choose_spec, ha'.choose_spec,
        ← Functor.map_comp_assoc, ← Functor.map_comp_assoc, fac]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ K (F.obj X)
⊢ S.arrows ∈ (Precoverage.comap F K.toPrecoverage).coverings X

Tactic:
simpa [GrothendieckTopology.mem_toPrecoverage_iff, Sieve.generate_map_eq_functorPushforward]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ (G.restrictedTopology K) U✝
⊢ Sieve.functorPushforward G S✝ ∈ K (G.obj U✝)

Tactic:
rw [Functor.restrictedTopology] at hS
    induction hS with
    | of X S hS => rwa [← Sieve.generate_map_eq_functorPushforward]
    | top X => simp
    | pullback X S _ Y f ih =>
      apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem
        ⟨_, K.pullback_stable (G.map f) ih⟩)
      rintro Z _ ⟨U, iUY, iZU, ⟨W, iWX, iUW, hiWX, e₁⟩, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable
      clear iZU Z
      apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)
      rintro Z _ ⟨U₁, iU₁U, iZU₁, ⟨iU₁W, e₂⟩, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable
      clear iZU₁ Z
      apply K.superset_covering ?_ (G.functorPushforward_equalizer_mem _
        (iU₁U ≫ iUY ≫ f) (iU₁W ≫ iWX) (by simp [e₁, e₂]))
      rintro Z _ ⟨U₂, iU₂U₁, iZU₂, e₃ : _ = _, rfl⟩
      refine ⟨_, iU₂U₁ ≫ iU₁U ≫ iUY, iZU₂, ?_, by simp⟩
      simpa [e₃] using S.downward_closed hiWX (iU₂U₁ ≫ iU₁W)
    | transitive X S R _ _ hS H' =>
      apply K.transitive hS
      rintro Y _ ⟨Z, g, i, hg, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable i
      refine K.superset_covering ?_ (H' hg)
      rintro W _ ⟨Z', g', i', hg, rfl⟩
      refine ⟨Z', g' ≫ g, i', hg, ?_⟩
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
⊢ equalizerSieve a b ∈ K (Opposite.unop X)

Tactic:
apply K.transitive (H.is_cover_of_isCoverDense K X.unop)

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ Opposite.unop X⦄,
    (Sieve.coverByImage H (Opposite.unop X)).arrows f → Sieve.pullback f (equalizerSieve a b) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
i : E.multicospanShape.R
⊢ (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.right i) ≅
    ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.right i)

Tactic:
exact G.mapIso (asIso (f.hom.h₁ i.2)).symm.op

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
⊢ ∀ (m : c.pt ⟶ (E.multifork F.obj).pt),
    (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i) → m = multiforkLift c

Tactic:
m

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
m : c.pt ⟶ (E.multifork F.obj).pt
⊢ (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i) → m = multiforkLift c
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y.left
⊢ (overEquiv Y).symm (generate R) = generate (Presieve.functorPullback (Over.forget X) R)

Tactic:
by
  refine le_antisymm (fun Z g hg ↦ ?_) ?_
  · rw [overEquiv_symm_iff] at hg
    obtain ⟨W, p, q, hq, hpq⟩ := hg
    refine ⟨.mk (q ≫ Y.hom), Over.homMk p (by simp [reassoc_of% hpq]), Over.homMk q rfl, hq, ?_⟩
    ext
    exact hpq
  · rw [generate_le_iff]
    exact fun Z g hg ↦ le_generate _ _ _ hg

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ ⋯.functor.obj ⊤ = U

Tactic:
by
  ext1
  exact Set.image_univ.trans Subtype.range_coe

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U) → x✝ ∈ ↑(hf.functor.obj ((map f).obj U))

Tactic:
· rintro ⟨⟨x, -, rfl⟩, hx⟩
    exact ⟨x, hx, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology ≤ pretopology T

Tactic:
intro X R hR x hx
    rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩
    exact ⟨V, g₂, hg₂, g₁.le hU⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
⊢ (pretopology T).toGrothendieck = grothendieckTopology T

Tactic:
by
  rw [← toPretopology_grothendieckTopology]
  apply (Pretopology.gi (Opens T)).l_u_eq

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : Type u_1
inst✝ : CompleteLattice X
v : ℕ → X
w x y z : X
e : v 0 = v 1
x✝¹ : v 1 = v 2
h₀ : v 1 ≤ x
x✝ : x ≤ z ⊓ w
h₂ : x ≤ y ⊓ z
⊢ v 0 ≤ y

Tactic:
restrict_tac

Goal state after:
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
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
⊢ Epi
    ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv.symm
      ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv
        (kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯)))

Tactic:
let h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit _)).symm

Goal state after:
C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0))).symm
⊢ Epi
    ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv.symm
      ((kernel (generatorsOfIsCokernelFree f g H H').π).freeHomEquiv
        (kernel.lift (generatorsOfIsCokernelFree f g H H').π f ⋯)))
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : ContinuousAdd M₁
inst✝ : ContinuousAdd M₂
f : M × M₁ →L[R] M₂
⊢ (f ∘SL inl R M M₁).coprod (f ∘SL inr R M M₁) = f

Tactic:
rw [← ContinuousLinearMap.comp_coprod, coprod_inl_inr, comp_id]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Ring R
inst✝⁷ : Ring S
A : Type u_3
inst✝⁶ : AddCommGroup A
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsModuleTopology R A
B' : Type u_5
inst✝² : AddCommGroup B'
inst✝¹ : Module S B'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
have := IsModuleTopology.toContinuousAdd R A

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Ring R
inst✝⁷ : Ring S
A : Type u_3
inst✝⁶ : AddCommGroup A
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsModuleTopology R A
B' : Type u_5
inst✝² : AddCommGroup B'
inst✝¹ : Module S B'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this : ContinuousAdd A
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable X κ J

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
⊢ IsCardinalPresentable X κ ↔ (uliftCoyoneda.{t, v₁, u₁}.obj (op X)).IsCardinalAccessible κ

Tactic:
change _ ↔ (coyoneda.obj (op X) ⋙ uliftFunctor.{t}).IsCardinalAccessible κ
  refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun J _ _ ↦ ?_⟩⟩
  have := Functor.preservesColimitsOfShape_of_isCardinalAccessible
    (coyoneda.obj (op X) ⋙ uliftFunctor.{t}) κ J
  exact preservesColimitsOfShape_of_reflects_of_preserves _ uliftFunctor.{t, v₁}

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
A : Type v'
inst✝ : Category.{u', v'} A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Cocone F

Tactic:
have := hA.small

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
A : Type v'
inst✝ : Category.{u', v'} A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
this : Small.{w, max u' v'} (Arrow A)
⊢ Cocone F
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
K : Type u'
S : K → J
hS : HasCardinalLT K κ
⊢ HasCardinalLT (Arrow (Discrete K)) κ

Tactic:
simpa using hS

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
K : Type u'
S : K → J
hS : HasCardinalLT K κ
k : K
⊢ HasCardinalLT (Arrow (Discrete K)) κ

Tactic:
simpa using hS

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

Goal state before:
pp: R A : CommRingCat
inst✝ : TopologicalSpace ↑R
x✝¹ x✝ : A ⟶ R
e : ⇑(Hom.hom x✝¹) = ⇑(Hom.hom x✝)
⊢ x✝¹ = x✝

Tactic:
ext; rw [e]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x y : N
⊢ (x + y) ⊗ₜ[R] Pi.single i 1 = x ⊗ₜ[R] Pi.single i 1 + y ⊗ₜ[R] Pi.single i 1

Tactic:
simp [add_tmul]

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

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
x : ↑C
⊢ (Hom.hom fC) (MvPolynomial.X x) = x

Tactic:
by simp [PC, fC]

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
x : ↑S
hx : x ∈ hf.finset
⊢ (CommRingCat.Hom.hom
        (a ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.fst ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x =
    (CommRingCat.Hom.hom
        (b ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.snd ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x

Tactic:
have (x : _) : F.map (f₁ x) (a x) = F.map (f₂ x) (b x) := h x

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
x : ↑S
hx : x ∈ hf.finset
this :
  ∀ (x : ↑S),
    (ConcreteCategory.hom (F.map (f₁ x))) ((ConcreteCategory.hom a) x) =
      (ConcreteCategory.hom (F.map (f₂ x))) ((ConcreteCategory.hom b) x)
⊢ (CommRingCat.Hom.hom
        (a ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.fst ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x =
    (CommRingCat.Hom.hom
        (b ≫
          F.map (D.multicospan.map (WalkingMulticospan.Hom.snd ⟨x, hx⟩) ≫ c'.ι.app (WalkingMulticospan.right ⟨x, hx⟩))))
      x
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
x y : M
x✝ : ↥(f.eqLocus g)
⊢ ↑({ toFun := fun a ↦ ⟨(x + y) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x✝) =
    ↑(({ toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := fun a ↦ ⟨y ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ })
        x✝)

Tactic:
simp [add_tmul]

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
x y : M
x✝ : ↥f.ker
⊢ ↑({ toFun := fun a ↦ ⟨(x + y) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x✝) =
    ↑(({ toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
          { toFun := fun a ↦ ⟨y ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ })
        x✝)

Tactic:
simp [add_tmul]

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
hA : P (CommRingCat.Hom.hom A.hom)
hB : P (CommRingCat.Hom.hom B.hom)
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S)

Tactic:
by
  rw [CommRingCat.preservesLimit_parallelPair_tensorProd_iff_tensorEqualizer_bijective]
  exact hPse _ _ hA hB

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ¬ringChar R ∣ t

Tactic:
rw [← ringChar.spec, ← Ne]
  exact Invertible.ne_zero (t : R)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a * b).num * (↑b.den * ↑a.den) = ↑((a * b).num * ↑a.den * ↑b.den)

Tactic:
simp_rw [Int.cast_mul, Int.cast_natCast]
        ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a + b).num * (↑b.den * ↑a.den) = ↑((a + b).num * ↑a.den * ↑b.den)

Tactic:
simp_rw [Int.cast_mul, Int.cast_natCast]
        ring

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
⊢ p > 0 → ¬MixedCharZero R p

Tactic:
p_pos

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
⊢ ¬MixedCharZero R p
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Algebra ℚ R

Tactic:
exact algebraRat h

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
⊢ p ≠ 0 → CharP R p → P

Tactic:
p_pos

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
⊢ CharP R p → P
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
⊢ p ≠ 0 → CharP R p → P

Tactic:
p_pos

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
⊢ CharP R p → P
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ ↑(z • a✝¹) = ↑(z • a✝) ↔ ∃ k, ⟦a✝¹⟧ = ⟦a✝⟧ + ↑(↑k • (p / ↑z))

Tactic:
← QuotientAddGroup.mk_add,

Goal state after:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ ↑(z • a✝¹) = ↑(z • a✝) ↔ ∃ k, ⟦a✝¹⟧ = ↑(a✝ + ↑k • (p / ↑z))
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = some a :: f.tail

Tactic:
rw [← f0]

Goal state after:
case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = get? ⟨f, al⟩ 0 :: f.tail