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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
X : C
S : Sieve X
H : ∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ S ∈ (finestTopology Ps) X

Tactic:
rintro _ ⟨⟨_, _, ⟨P, hP, rfl⟩, rfl⟩, rfl⟩ Y f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
X : C
S : Sieve X
H : ∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
P : Cᵒᵖ ⥤ Type w
hP : P ∈ Ps
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : F.IsContinuous J K
⊢ J ≤ F.inducedTopology K

Tactic:
apply Sheaf.le_finestTopology
    rintro _ ⟨P, rfl⟩
    exact Functor.op_comp_isSheaf_of_types F J K P

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

Goal state before:
pp: case mp
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.Full
inst✝ : G.Faithful
X : C
S : Sieve X
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
⊢ ∃ T, Sieve.functorPullback G ↑T = S

Tactic:
exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩

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

Goal state before:
pp: case refine_1.refine_1
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.L
⊢ (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.left i) ≅
    ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.left i)

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

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y.left
hS : S ∈ J Y.left
⊢ (Sieve.overEquiv Y).symm S ∈ (J.over X) Y

Tactic:
simpa only [mem_over_iff, OrderIso.apply_symm_apply] using hS

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ (Sieve.overEquiv ((Over.post F).obj U)) (Sieve.functorPushforward (Over.post F) S) ∈ K ((Over.post F).obj U).left

Tactic:
rw [Sieve.overEquiv_functorPushforward_post]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ Sieve.functorPushforward F ((Sieve.overEquiv U) S) ∈ K ((Over.post F).obj U).left
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

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✝¹
C✝ : Type u₁
inst✝⁵ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J✝ : GrothendieckTopology C✝
K : GrothendieckTopology D
F : C✝ ⥤ D
G : D ⥤ C✝
S : Sheaf J✝ RingCat
R✝ : Sheaf K RingCat
inst✝³ : F.IsContinuous J✝ K
inst✝² : G.IsContinuous K J✝
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R✝
ψ : R✝ ⟶ (G.sheafPushforwardContinuous RingCat K J✝).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R✝.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
C : Type u'
inst✝¹ : Category.{v', u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
x : C
U V : Cᵒᵖ
f : U ⟶ V
⊢ R.obj.map f ≫ R.obj.map prod.snd.op =
    R.obj.map prod.snd.op ≫ (((Over.star x).sheafPushforwardContinuous RingCat J (J.over x)).obj (R.over x)).obj.map f

Tactic:
by simp [← Functor.map_comp, ← op_comp]; rfl

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ U
V : Opens ↑X
iVU : V ⟶ U
hxV : x ∈ V
W : Opens ↑X
iVW : V ⟶ W
iWU : W ⟶ U
hiWU : R iWU
⊢ ∃ i, x ∈ coveringOfPresieve U R i

Tactic:
exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case pair
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.pair i j)))) s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Tactic:
rw [← (F.mapCone (Pairwise.cocone U).op).w (op <| Pairwise.Hom.left i j)]

Goal state after:
case pair
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ (ConcreteCategory.hom
        ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.single i)) ≫
          ((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.left i j))))
      s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
⊢ F.IsSheaf ↔ F.IsSheafUniqueGluing

Tactic:
simp_rw [isSheaf_iff_isSheafPairwiseIntersections, IsSheafPairwiseIntersections,
    Types.isLimit_iff, IsSheafUniqueGluing, isGluing_iff_pairwise]

Goal state after:
X : TopCat
F : Presheaf (Type u_4) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X),
      ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
        ∃! x,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X) (sf : (i : ι) → ToType (F.obj (op (U i)))),
      F.IsCompatible U sf →
        ∃! s,
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U : Opens ↑Y
hU : (ConcreteCategory.hom f) x ∈ U
⊢ F.germ U ((ConcreteCategory.hom f) x) hU ≫ stalkPullbackHom C f F x =
    ((pullbackPushforwardAdjunction C f).unit.app F).app (op U) ≫ ((pullback C f).obj F).germ ((Opens.map f).obj U) x hU

Tactic:
by
  simp [stalkPullbackHom, germ, stalkFunctor, stalkPushforward]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

Tactic:
rw [← cocone_naturality F f]

Goal state after:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (F.map f ≫ coconeMorphism F j')) x
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0

Tactic:
rintro ⟨hM, hM₂⟩
    let e : M ≃L[R] M₂ :=
    { toFun := 0
      invFun := 0
      left_inv x := Subsingleton.elim _ _
      right_inv x := Subsingleton.elim _ _
      map_add' x y := Subsingleton.elim _ _
      map_smul' c x := Subsingleton.elim _ _ }
    refine ⟨e, ?_⟩
    ext x
    exact Subsingleton.elim _ _

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 w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ HasCardinalLT (Arrow A) Cardinal.aleph0

Tactic:
simp only [hasCardinalLT_aleph0_iff]

Goal state after:
J : Type u
inst✝³ : Category.{v, u} J
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝² : IsCardinalFiltered J κ
A : Type w
inst✝¹ : SmallCategory A
inst✝ : FinCategory A
F : A ⥤ J
⊢ Finite (Arrow A)
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: ι : Type u'
J : ι → Type u
inst✝³ : (i : ι) → Category.{v, u} (J i)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : ∀ (i : ι), IsCardinalFiltered (J i) κ
A✝ : Type w
inst✝ : SmallCategory A✝
F : A✝ ⥤ ((i : ι) → J i)
hC : HasCardinalLT (Arrow A✝) κ
⊢ Cocone F

Tactic:
by
    let c (i : ι) := cocone (F ⋙ Pi.eval J i) hC
    exact
      { pt i := (c i).pt
        ι.app X i := (c i).ι.app X
        ι.naturality {X Y} f := by
          ext i
          simpa using! (c i).ι.naturality f }

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

Goal state before:
pp: R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
x : A ⟶ R
H : ∀ (a : ↑A), (Hom.hom f) a = 0 → (ConcreteCategory.hom x) a = 0
x✝ : ↑A
⊢ (Hom.hom (f ≫ ofHom (((Hom.hom f).liftOfSurjective hf) ⟨Hom.hom x, H⟩))) x✝ = (Hom.hom x) x✝

Tactic:
simp [RingHom.liftOfRightInverse_comp_apply]

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)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
⊢ IsEmbedding fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)

Tactic:
← IsEmbedding.of_comp_iff this

Goal state after:
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)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
⊢ IsEmbedding ((Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x) ∘ fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f))
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
N₃ : Type u_7
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₂
inst✝⁹ : AddCommGroup N₃
inst✝⁸ : Module R N₃
i₁ : M₁ →ₗ[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₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁷ : AddCommGroup K₂
inst✝⁶ : Module R K₂
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x y : K₃
⊢ π₁ (ρ (i₂ (σ (ι₃ (x + y))))) = π₁ (ρ (i₂ (σ (ι₃ x)))) + π₁ (ρ (i₂ (σ (ι₃ y))))

Tactic:
rw [← map_add]

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
N₃ : Type u_7
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₂
inst✝⁹ : AddCommGroup N₃
inst✝⁸ : Module R N₃
i₁ : M₁ →ₗ[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₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁷ : AddCommGroup K₂
inst✝⁶ : Module R K₂
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x y : K₃
⊢ π₁ (ρ (i₂ (σ (ι₃ (x + y))))) = π₁ (ρ (i₂ (σ (ι₃ x))) + ρ (i₂ (σ (ι₃ y))))
Module: Mathlib.Algebra.Category.Ring.Under.Limits

Goal state before:
pp: R : CommRingCat
A B : Under R
f g : A ⟶ B
⊢ ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ f = ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ g

Tactic:
ext (a : AlgHom.equalizer (toAlgHom f) (toAlgHom g))
  exact a.property

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

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝³ : HasPushouts T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.HasOfPrecompProperty P
⊢ P.underObj.IsClosedUnderColimitsOfShape WalkingSpan

Tactic:
rw [ObjectProperty.isClosedUnderColimitsOfShape_iff_op, ←
    ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff _ _ (Over.opEquivOpUnder _),
    MorphismProperty.inverseImage_op_underObj,
    ObjectProperty.isClosedUnderLimitsOfShape_iff_of_equivalence _ walkingSpanOpEquiv]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ Hom.left (Y✝.π.app { as := j }) = Hom.left (X✝.π.app { as := j })

Tactic:
rw [← f.w ⟨j⟩]

Goal state after:
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ Hom.left (Y✝.π.app { as := j }) = Hom.left (f.hom ≫ Y✝.π.app { as := 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
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
⊢ PreservesFiniteProducts
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ f)

Tactic:
refine ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩

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
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this :
  CreatesFiniteProducts (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
⊢ PreservesLimit K (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ f)
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
r : S
x : M
x✝ : ↥(f.eqLocus g)
⊢ ↑({ toFun := fun a ↦ ⟨(r • x) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } x✝) =
    ↑(((RingHom.id S) r • { toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }) x✝)

Tactic:
simp [smul_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
r : S
x : M
y : ↥f.ker
⊢ ↑({ toFun := fun a ↦ ⟨(r • x) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } y) =
    ↑(((RingHom.id S) r • { toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }) y)

Tactic:
simp [smul_tmul']

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_pos : p ≠ 0
⊢ CharP R p → P

Tactic:
p_char

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
p_char : 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_pos : p ≠ 0
⊢ CharP R p → P

Tactic:
p_char

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
p_char : CharP R p
⊢ P
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
h : (some a :: ↑s) 0 = none
⊢ (some a :: ↑s) (0 + 1) = none

pp: case succ
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n✝ : ℕ
h : (some a :: ↑s) (n✝ + 1) = none
⊢ (some a :: ↑s) (n✝ + 1 + 1) = none

Tactic:
· contradiction

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
n✝ : ℕ
h : (some a :: ↑s) (n✝ + 1) = none
⊢ (some a :: ↑s) (n✝ + 1 + 1) = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mp
α : Type u
x x' : α
s s' : Seq α
⊢ cons x s = cons x' s' → x = x' ∧ s = s'

pp: case mpr
α : Type u
x x' : α
s s' : Seq α
⊢ x = x' ∧ s = s' → cons x s = cons x' s'

Tactic:
· apply cons_injective2

Goal state after:
case mpr
α : Type u
x x' : α
s s' : Seq α
⊢ x = x' ∧ s = s' → cons x s = cons x' s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
h : (fun a' ↦ (a', s.tail)) <$> some val✝ = none
⊢ s = nil

Tactic:
· contradiction

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
h : (fun a' ↦ (a', s.tail)) <$> none = some (a, s')
⊢ s = cons a s'

pp: case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'

Tactic:
· contradiction

Goal state after:
case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s

Tactic:
left

Goal state after:
case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
h : Stream'.cons none c.val 0 = some a
⊢ Stream'.cons none c.val (0 + 1) = some a

pp: case succ
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h : Stream'.cons none c.val (n + 1) = some a
⊢ Stream'.cons none c.val (n + 1 + 1) = some a

Tactic:
· contradiction

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h : Stream'.cons none c.val (n + 1) = some a
⊢ Stream'.cons none c.val (n + 1 + 1) = some a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

Tactic:
· contradiction

Goal state after:
case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
· contradiction

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.even.get n.succ = s.get (2 * n.succ)

Tactic:
by
    change get (even s) (succ n) = get s (succ (succ (2 * n)))
    rw [get_succ, get_succ, tail_even, get_even n]; rfl

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e✝ : α
e : s n = some e✝
a✝ : Option.map f (some e✝) = none
⊢ Option.map f (s (n + 1)) = none

Tactic:
· contradiction

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
s : Computation α
a : α
h : some a = s.think.val.get 0
⊢ a ∈ s

pp: case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = s.think.val.get (n' + 1)
⊢ a ∈ s

Tactic:
· contradiction

Goal state after:
case succ
α : Type u
s : Computation α
a : α
n' : ℕ
h : some a = s.think.val.get (n' + 1)
⊢ a ∈ s