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
J : GrothendieckTopology C
K : GrothendieckTopology D
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 Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ ⋯.amalgamate ⟨G.imageSieve f, ⋯⟩
        (fun x ↦
          match x with
          | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op)
        ⋯ ≫
      F.obj.map (a ≫ p).op =
    F.obj.map g.op ≫ F.obj.map a.op

Tactic:
F.2.amalgamate_map ⟨_, imageSieve_mem J K G f⟩
        (fun ⟨W₀, a, ha⟩ ↦ F.obj.map ha.choose.op) _ ⟨W₀, a ≫ p, ha⟩,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
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 Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ (match { Y := W₀, f := a ≫ p, hf := ha } with
    | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op) =
    F.obj.map g.op ≫ F.obj.map a.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
⊢ (comap F K).toGrothendieck = F.restrictedTopology K.toGrothendieck

Tactic:
refine le_antisymm ?_ fun X T hT ↦ ?_

Goal state after:
case refine_1
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
⊢ (comap F K).toGrothendieck ≤ F.restrictedTopology K.toGrothendieck

case refine_2
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
hT : T ∈ (F.restrictedTopology K.toGrothendieck) X
⊢ T ∈ (comap F K).toGrothendieck X
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1

Tactic:
let d : T ⟶ W := Over.homMk b

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsIso biprod.inl ↔ IsZero Y

Tactic:
by
  rw [biprod.isIso_inl_iff_id_eq_fst_comp_inl, ← biprod.total, add_eq_left]
  constructor
  · intro h
    replace h := h =≫ biprod.snd
    simpa [← IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h
  · intro h
    rw [IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] at h
    rw [h, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
F : Discrete WalkingPair ⥤ C
this : HasLimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
⊢ HasLimit F

Tactic:
apply hasLimit_of_iso (diagramIsoPair F).symm

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_2
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
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
shAdj : F.sheafPushforwardContinuous RingCat J K ⊣ F.rightAdjoint.sheafPushforwardContinuous RingCat K J :=
  adj.sheafPushforwardContinuous J K
ψ : R ⟶ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).obj S :=
  shAdj.unit.app R ≫ (F.rightAdjoint.sheafPushforwardContinuous RingCat K J).map (CategoryTheory.inv φ)
U : Cᵒᵖ
this :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y), φ.hom.app X ≫ R.obj.map (F.map f.unop).op ≫ CategoryTheory.inv (φ.hom.app Y) = S.obj.map f
⊢ (φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj).app U = (𝟙 S.obj).app U

Tactic:
simp [ψ, shAdj, ← this, ← Functor.map_comp_assoc, ← op_comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesLimitsOfSize.{v, v, v, max v v', max u (v + 1), (max v v') + 1}
    (uliftFunctor.{v', v, u} R ⋙ forget (ModuleCat R))

Tactic:
by
    change Limits.PreservesLimitsOfSize.{v, v} (forget (ModuleCat R) ⋙
      CategoryTheory.uliftFunctor.{v'})
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
this :
  Limits.PreservesFiniteLimits (uliftFunctor.{v', v, u} R) ∧ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)
⊢ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)

Tactic:
exact this.2

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : M ≃L[R] M
⊢ ↑f * ↑f.symm = 1

Tactic:
by
    ext
    simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : M ≃L[R] M
⊢ ↑f.symm * ↑f = 1

Tactic:
by
    ext
    simp

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map δ ≫ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map γ ≫ F.map (minToRight i₀ j)

Tactic:
← F.map_comp_assoc,

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map (δ ≫ α) ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map γ ≫ F.map (minToRight i₀ j)
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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ s.π.app i₀ ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = s.π.app j

Tactic:
← s.w (IsCofiltered.minToLeft i₀ 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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
j : J
⊢ (s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToLeft i₀ j)) ≫
      (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) =
    s.π.app j
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ'
⊢ PreservesColimitsOfShape J F

Tactic:
have := IsCardinalFiltered.of_le J h

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ'
this : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : F.IsCardinalAccessible κ
J : Type w
x✝ : SmallCategory J
hκ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J G

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ J
    exact preservesColimitsOfShape_of_natIso e

Goal state after:
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'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
X✝ Y✝ : C'
f : X✝ ⟶ Y✝
g : (coyoneda.obj (op (e.functor.obj X))).obj X✝
⊢ (ConcreteCategory.hom
          ((coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}).map f ≫
            (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Y✝).trans Equiv.ulift.symm)).toIso.hom)).toFun
      { down := g } =
    (ConcreteCategory.hom
          ((Equiv.ulift.trans ((e.toAdjunction.homEquiv X X✝).trans Equiv.ulift.symm)).toIso.hom ≫
            (e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)).toFun
      { down := g }

Tactic:
simp [Adjunction.homEquiv_unit]

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

Goal state before:
pp: κ : Cardinal.{w}
hκ : Fact κ.IsRegular
ι : Type w
f : ι → κ.ord.ToType
h : Function.Surjective fun i ↦ ⟨f i, ⋯⟩
hs : ∀ (j : κ.ord.ToType), ∃ k, j < f k
j : κ.ord.ToType
k : ι
hk : j < f k
⊢ ∃ y ∈ Set.range f, j ≤ y

Tactic:
exact ⟨_, Set.mem_range_self k, hk.le⟩

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
ι : Type w
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
i : ι
l : J
a : k ⟶ l
b : j i ⟶ l
hl : ∀ (i_1 : PUnit.{w + 1} ⊕ PUnit.{w + 1}), Sum.elim (fun x ↦ f₁ i) (fun x ↦ f₂ i) i_1 ≫ a = b
⊢ ∃ l p, f₁ i ≫ p = f₂ i ≫ p

Tactic:
exact ⟨l, a, (hl (Sum.inl .unit)).trans (hl (Sum.inr .unit)).symm⟩

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

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
⊢ IsCardinalFiltered J κ ↔
    (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
      ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b

Tactic:
by
  refine ⟨fun _ ↦ ⟨fun ι j hι ↦ ⟨_, fun i ↦ ⟨toMax j hι i⟩⟩,
    fun ι j k f hι ↦ ⟨_, _, _, coeq_condition f hι⟩⟩,
    fun ⟨h₁, h₂⟩ ↦ ⟨fun {A _} F hA ↦ ?_⟩⟩
  obtain ⟨j, hj⟩ := h₁ F.obj (hasCardinalLT_of_hasCardinalLT_arrow hA)
  let a (i : A) : F.obj i ⟶ j := (hj i).some
  obtain ⟨l, b, hb⟩ := isCardinalFiltered_iff_aux₂ h₁ h₂
    (fun (f : Arrow A) ↦ F.map f.hom ≫ a f.right)
    (fun (f : Arrow A) ↦ a f.left) hA
  exact ⟨{
    pt := l
    ι.app i := a i ≫ b
    ι.naturality _ _ f := by simpa using hb (Arrow.mk f) }⟩

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
⊢ ∃ l a, ∀ (i : ι), f₁ i ≫ a = f₂ i ≫ a

Tactic:
exact ⟨l, b, fun i ↦ by rw [← h i, IsFiltered.coeq_condition_assoc]⟩

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
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
x✝¹ x✝ : N
⊢ (pi fun i ↦ (mk R N (M i)) (x✝¹ + x✝) ∘ₗ proj i) =
    (pi fun i ↦ (mk R N (M i)) x✝¹ ∘ₗ proj i) + pi fun i ↦ (mk R N (M i)) x✝ ∘ₗ proj i

Tactic:
by
    ext
    simp

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

Goal state before:
pp: case pos
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 a b, ∀ (i : ι), f i ≫ a = b

Tactic:
obtain ⟨l, ⟨a⟩⟩ := h₁ k
      choose m b hb using fun (i : ι × ι) ↦ h₂ (f i.1 ≫ a) (f i.2 ≫ a)
      simp only [Category.assoc, Prod.forall] at hb
      obtain ⟨n, c, d, hn⟩ := wideSpan b
        (hasCardinalLT_prod (Cardinal.IsRegular.aleph0_le Fact.out) hι hι)
      let i₀ : ι := Classical.arbitrary _
      exact ⟨F.obj n, a ≫ F.map d, f i₀ ≫ a ≫ F.map d,
        fun i ↦ by rw [← hn (i₀, i), Functor.map_comp, reassoc_of% (hb i₀ i)]⟩

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

Goal state before:
pp: case neg
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 a b, ∀ (i : ι), f i ≫ a = b

Tactic:
simp only [not_nonempty_iff] at h

Goal state after:
case neg
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 : IsEmpty ι
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b
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)
⊢ IsEmbedding fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)

Tactic:
have hfB : Function.Surjective fB.hom := fun x ↦ ⟨.X x, by simp [PB, fB]⟩

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)
⊢ IsEmbedding fun f ↦ (pushout.inl φ ψ ≫ f, pushout.inr φ ψ ≫ f)
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)
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj A

Tactic:
let e : A ≅ CommRingCat.mkUnder R (Π i, pres.diag.obj ⟨i⟩) :=
    (limit.isoLimitCone ⟨_, pres.isLimit⟩).symm ≪≫
      HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso <| by simp) ≪≫
      limit.isoLimitCone ⟨CommRingCat.Under.piFan <| fun i ↦ (pres.diag.obj ⟨i⟩),
        CommRingCat.Under.piFanIsLimit <| fun i ↦ (pres.diag.obj ⟨i⟩)⟩

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 } }
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).underObj A
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 A p
⊢ CharP R p

Tactic:
obtain ⟨q, h⟩ := CharP.exists R

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
inst✝ : CharP A p
q : ℕ
h : CharP R q
⊢ CharP R p
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
⊢ x ∈ lift (restrict h)

Tactic:
let y : E := ⟨x, h hx⟩

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ F
y : ↥E := ⟨x, ⋯⟩
⊢ x ∈ lift (restrict h)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
o : Option β
⊢ (Corec.f f o).fst = none → (Corec.f f (Corec.f f o).snd).fst = none

Tactic:
rcases o with - | b

Goal state after:
case zero.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ (Corec.f f none).fst = none → (Corec.f f (Corec.f f none).snd).fst = none

case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
⊢ (Corec.f f (some b)).fst = none → (Corec.f f (Corec.f f (some b)).snd).fst = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ : Stream' (Option α)
⊢ ∀ ⦃s₂ : Stream' (Option α)⦄,
    (∃ s s', ↑s = t₁ ∧ ↑s' = s₂ ∧ R s s') → t₁.head = s₂.head ∧ ∃ s s', ↑s = t₁.tail ∧ ↑s' = s₂.tail ∧ R s s'

Tactic:
t₂

Goal state after:
case bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
⊢ (∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s') → t₁.head = t₂.head ∧ ∃ s s', ↑s = t₁.tail ∧ ↑s' = t₂.tail ∧ R s s'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
n : ℕ
⊢ (const a).get n = (a :: const a).get n

Tactic:
cases n <;> rfl

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

Goal state before:
pp: α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1) + 1) = s₂.get (n + 1)

Tactic:
by
    change get (s₁ ⋈ s₂) (succ (succ (2 * n + 1))) = get s₂ (succ n)
    rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons,
      get_interleave_right n (tail s₁) (tail s₂)]
    rfl

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

Goal state before:
pp: case bisim
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ : Stream' (Option α)
⊢ ∀ ⦃s₂ : Stream' (Option α)⦄,
    (∃ s s', s.val = t₁ ∧ s'.val = s₂ ∧ R s s') →
      t₁.head = s₂.head ∧ ∃ s s', s.val = t₁.tail ∧ s'.val = s₂.tail ∧ R s s'

Tactic:
t₂

Goal state after:
case bisim
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
⊢ (∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s') → t₁.head = t₂.head ∧ ∃ s s', s.val = t₁.tail ∧ s'.val = t₂.tail ∧ R s s'
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : x ∈ s
⊢ ∃ i, some x = s.get? i

Tactic:
by
    change (some x ∈ s.1) at h
    rwa [Stream'.mem_iff_exists_get_eq] at h

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

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ s.length = n

Tactic:
h2.length

Goal state after:
α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ n = n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ s.TerminatedAt n

Tactic:
rw [← length_le_iff']; simp [h]

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

Goal state before:
pp: α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ (map id ⟨f, al⟩).val = ⟨f, al⟩.val

Tactic:
simp only [map, comp_apply, id_eq]

Goal state after:
α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ Stream'.map (fun o ↦ Option.rec none (fun val ↦ some val) o) f = f