mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
κ : Cardinal.{w}
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 : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
⊢ ∃ m a b, ∀ (i : ι), f i ≫ a i = b

Tactic:
obtain ⟨l, hl⟩ := h₁ k hι

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
κ : Cardinal.{w}
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 : (i : ι) → j ⟶ k i
hι : HasCardinalLT ι κ
l : J
hl : ∀ (i : ι), Nonempty (k i ⟶ l)
⊢ ∃ m a b, ∀ (i : ι), f i ≫ a i = b
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 : ι → 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:
refine ⟨fun ι j hι ↦ ?_, fun ι j k f hι ↦ ?_⟩

Goal state after:
case refine_1
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 : ι → J₂
hι : HasCardinalLT ι κ
⊢ ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)

case refine_2
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 ι κ
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b
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})
⊢ (Set.range fun x ↦ f ≫ x) = ⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0}

Tactic:
ext x

Goal state after:
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
⊢ (x ∈ Set.range fun x ↦ f ≫ x) ↔ x ∈ ⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0}
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A : CommRingCat
inst✝² : TopologicalSpace ↑R
inst✝¹ : IsTopologicalRing ↑R
inst✝ : T1Space ↑R
f : of (MvPolynomial ↑A ↑(⊥_ CommRingCat)) ⟶ A := ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
this : Function.Surjective ⇑(ConcreteCategory.hom f)
g : A ⟶ R
⊢ ⇑(Hom.hom g) =
    (⇑((mvPolynomialHomeomorph (↑A) R (of ↑(colimit.cocone (Functor.empty CommRingCat)).1)).trans
            (Homeomorph.uniqueProd (⊥_ CommRingCat ⟶ R) (↑A → ↑R))) ∘
        fun x ↦ f ≫ x)
      g

Tactic:
ext x

Goal state after:
R A : CommRingCat
inst✝² : TopologicalSpace ↑R
inst✝¹ : IsTopologicalRing ↑R
inst✝ : T1Space ↑R
f : of (MvPolynomial ↑A ↑(⊥_ CommRingCat)) ⟶ A := ofHom (MvPolynomial.eval₂Hom (Hom.hom (initial.to A)) id)
this : Function.Surjective ⇑(ConcreteCategory.hom f)
g : A ⟶ R
x : ↑A
⊢ (Hom.hom g) x =
    (⇑((mvPolynomialHomeomorph (↑A) R (of ↑(colimit.cocone (Functor.empty CommRingCat)).1)).trans
            (Homeomorph.uniqueProd (⊥_ CommRingCat ⟶ R) (↑A → ↑R))) ∘
        fun x ↦ f ≫ x)
      g x
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
i : J
hi : (a : Fin n) → j a ⟶ i
⊢ iP ≫
      CommRingCat.ofHom
        (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (α.app i)) fun x_1 ↦
          (ConcreteCategory.hom (F.map (hi x_1))) (x x_1)) =
    α.app i

Tactic:
ext x

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x✝ : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x✝ i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
i : J
hi : (a : Fin n) → j a ⟶ i
x : ↑R
⊢ (CommRingCat.Hom.hom
        (iP ≫
          CommRingCat.ofHom
            (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (α.app i)) fun x ↦
              (ConcreteCategory.hom (F.map (hi x))) (x✝ x))))
      x =
    (CommRingCat.Hom.hom (α.app i)) x
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ (iP ≫ π) ≫
      CommRingCat.ofHom
        (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩) =
    α.app c'.pt

Tactic:
ext x

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑R
⊢ (CommRingCat.Hom.hom
        ((iP ≫ π) ≫
          CommRingCat.ofHom
            (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩)))
      x =
    (CommRingCat.Hom.hom (α.app c'.pt)) x
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_3
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
⊢ g =
    CommRingCat.ofHom
        (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩) ≫
      c.ι.app c'.pt

Tactic:
ext x

Goal state after:
case refine_3
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
i : J
g' : P ⟶ F.obj i
hg' : π ≫ g = g' ≫ c.ι.app i
hg'' : iP ≫ g' = α.app i
i' : ↥s → J
hi' : (r : ↥s) → i ⟶ i' r
hi'' : ∀ (r : ↥s), (ConcreteCategory.hom (F.map (hi' r))) ((ConcreteCategory.hom g') ↑r) = 0
c' : Cocone (WidePushoutShape.wideSpan i i' hi')
x : ↑S
⊢ (CommRingCat.Hom.hom g) x =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (((CommRingCat.Hom.hom π).liftOfSurjective hπ) ⟨CommRingCat.Hom.hom (g' ≫ F.map (c'.ι.app none)), ⋯⟩) ≫
          c.ι.app c'.pt))
      x
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
⊢ ∀ {c : Cocone F} (hc : IsColimit c), Nonempty (IsColimit ((coyoneda.obj (Opposite.op S)).mapCocone c))

Tactic:
intro c hc

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
⊢ Nonempty (IsColimit ((coyoneda.obj (Opposite.op S)).mapCocone c))
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
⊢ CharP A p

Tactic:
have := f.domain_nontrivial
  have H := (CharP.char_is_prime_or_zero R p).resolve_right hp
  obtain ⟨q, hq⟩ := CharP.exists A
  obtain ⟨k, e⟩ := dvd_of_ringHom f p q
  have := Nat.isUnit_iff.mp ((H.2 e).resolve_left (Nat.isUnit_iff.not.mpr (char_ne_one A q)))
  rw [this, mul_one] at e
  exact e ▸ hq

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

Goal state before:
pp: 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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
inst✝ : Q.RespectsIso
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) mapComp._auto_1
⊢ P fg

Tactic:
subst hfg

Goal state after:
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
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
inst✝ : Q.RespectsIso
⊢ P (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pullbackComp._auto_1
⊢ P.HasPullbacksAlong fg

Tactic:
subst hfg

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
⊢ P.HasPullbacksAlong (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pullbackComp._auto_1
this : P.HasPullbacksAlong fg
⊢ P.IsStableUnderBaseChangeAlong fg

Tactic:
subst hfg

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
this : P.HasPullbacksAlong (f ≫ g)
⊢ P.IsStableUnderBaseChangeAlong (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
fg : X ⟶ Z
hfg : fg = f ≫ g
⊢ P.HasPullbacksAlong fg

Tactic:
subst hfg

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderBaseChangeAlong f
inst✝⁴ : P.IsStableUnderBaseChangeAlong g
inst✝³ : P.HasPullbacksAlong f
inst✝² : P.HasPullbacksAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderBaseChange
⊢ P.HasPullbacksAlong (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: 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
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (f ≫ g = fg) pullbackMapHomPullback._auto_1
⊢ P.IsStableUnderBaseChangeAlong fg

Tactic:
subst hfg

Goal state after:
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
X Y Z : T
f : X ⟶ Y
hPf : P f
hQf : Q f
g : Y ⟶ Z
inst✝³ : P.IsStableUnderBaseChangeAlong f
inst✝² : P.IsStableUnderBaseChangeAlong g
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : HasPullbacks T
⊢ P.IsStableUnderBaseChangeAlong (f ≫ g)
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
inst✝ : Module.Flat R M
⊢ tensorKer S M f ∘ₗ tensorKerInv S M f = id

Tactic:
ext x

Goal state after:
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
inst✝ : Module.Flat R M
x : ↥((AlgebraTensorModule.lTensor S M) f).ker
⊢ ↑((tensorKer S M f ∘ₗ tensorKerInv S M f) x) = ↑(id x)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
⊢ P.HasPushoutsAlong fg

Tactic:
subst hfg

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.HasPushoutsAlong (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
fg : optParam (X ⟶ Z) (f ≫ g)
hfg : autoParam (fg = f ≫ g) pushoutComp._auto_1
this : P.HasPushoutsAlong fg
⊢ P.IsStableUnderCobaseChangeAlong fg

Tactic:
subst hfg

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
this : P.HasPushoutsAlong (f ≫ g)
⊢ P.IsStableUnderCobaseChangeAlong (f ≫ g)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
fg : X ⟶ Z
hfg : fg = f ≫ g
⊢ P.HasPushoutsAlong fg

Tactic:
subst hfg

Goal state after:
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁶ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
inst✝⁵ : P.IsStableUnderCobaseChangeAlong f
inst✝⁴ : P.IsStableUnderCobaseChangeAlong g
inst✝³ : P.HasPushoutsAlong f
inst✝² : P.HasPushoutsAlong g
inst✝¹ : Q.RespectsIso
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.HasPushoutsAlong (f ≫ g)
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ n ∣ x

Tactic:
← CharP.cast_eq_zero_iff (R ⧸ I) n _

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
x✝ : CharP (R ⧸ I) n
x : ℕ
hx : ↑x ∈ I
⊢ ↑x = 0
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ Function.Injective Nat.cast

Tactic:
intro a b h_ab

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
a b : ℕ
h_ab : ↑a = ↑b
⊢ a = b
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: 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
⊢ lift (restrict h) = F

Tactic:
ext x

Goal state after:
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
⊢ x ∈ lift (restrict h) ↔ x ∈ F
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case nil
α : Type u
a : Stream' α
n : ℕ
h : n < [].length
⊢ ([] ++ₛ a).get n = [][n]

Tactic:
simp at h

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), take n s ++ₛ drop n s = s
s : Stream' α
⊢ take (n + 1) s ++ₛ drop (n + 1) s = s

Tactic:
rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a <+: take n a

Tactic:
(by simp [h] : a.take m = (a.take n).take m)

Goal state after:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Tactic:
terminatedAt_iff_s_none

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
terminatedAt_n : g.s.get? n = none
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux m = g.contsAux (n + 1)

Tactic:
refine Nat.le_induction rfl (fun k hnk hk => ?_) _ n_lt_m
  rcases Nat.exists_eq_add_of_lt hnk with ⟨k, rfl⟩
  refine (contsAux_stable_step_of_terminated ?_).trans hk
  exact terminated_stable (Nat.le_add_right _ _) terminatedAt_n

Goal state after: