mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : f (c • x₁) = f (c • x₂)
⊢ f x₁ = f x₂

Tactic:
simp_rw [f.map_smul_of_tower, Submonoid.smul_def, ← Module.algebraMap_end_apply R R] at h

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
x✝ : ∃ c, c • x₁ = c • x₂
c : ↥S
h : ((algebraMap R (End R M')) ↑c) (f x₁) = ((algebraMap R (End R M')) ↑c) (f x₂)
⊢ f x₁ = f x₂
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom) =
    pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
      Under.Hom.right
        ((tensorProdObjIsoPushoutObj S A).inv ≫
          (tensorProdObjIsoPushoutObj S A).hom ≫
            Under.homMk
              (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
              ⋯)

Tactic:
rw [← cancel_mono (tensorProdObjIsoPushoutObj S B).inv.right]
      ext x
      simp [mkUnder_right]

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

Goal state before:
pp: R : CommRingCat
x✝ : of (ULift.{u, 0} ℤ) ⟶ R
⊢ Hom.hom x✝ = Hom.hom default

Tactic:
← RingHom.cancel_right (f := (ULift.ringEquiv.{0, u} (R := ℤ)).symm.toRingHom)
        (hf := ULift.ringEquiv.symm.surjective)

Goal state after:
R : CommRingCat
x✝ : of (ULift.{u, 0} ℤ) ⟶ R
⊢ (Hom.hom x✝).comp ULift.ringEquiv.symm.toRingHom = (Hom.hom default).comp ULift.ringEquiv.symm.toRingHom
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : ↑s.pt
eq1 : (ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
eq2 : (ConcreteCategory.hom (m ≫ (A.prodFan B).snd)) x = (ConcreteCategory.hom (BinaryFan.snd s)) x
⊢ (ConcreteCategory.hom m) x =
    ((ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x, (ConcreteCategory.hom (BinaryFan.snd s)) x)

Tactic:
← eq2

Goal state after:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : ↑s.pt
eq1 : (ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x = (ConcreteCategory.hom (BinaryFan.fst s)) x
eq2 : (ConcreteCategory.hom (m ≫ (A.prodFan B).snd)) x = (ConcreteCategory.hom (BinaryFan.snd s)) x
⊢ (ConcreteCategory.hom m) x =
    ((ConcreteCategory.hom (m ≫ (A.prodFan B).fst)) x, (ConcreteCategory.hom (m ≫ (A.prodFan B).snd)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ (ConcreteCategory.hom (F.map (𝟙 one))) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
    (ConcreteCategory.hom (F.map left)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
simp only [CategoryTheory.Functor.map_id, hom_id, limit.cone_x, limit.cone_π, RingHom.id_apply]

Goal state after:
case one
A B : CommRingCat
f g : A ⟶ B
F : WalkingParallelPair ⥤ CommRingCat
x : ↑(limit.cone F).pt
hx : IsUnit ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
⊢ (ConcreteCategory.hom (limit.π F one)) x =
    (ConcreteCategory.hom (F.map left)) ((ConcreteCategory.hom (limit.π F zero)) x)
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
eq2 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x
⊢ ↑((ConcreteCategory.hom m) x) =
    ((Hom.hom
          (m ≫
            ofHom
              ((RingHom.fst ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x,
      (Hom.hom s.snd) x)

Tactic:
← eq2

Goal state after:
case uniq
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
m : s.pt ⟶ of ↥(((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B)))
e₁ :
  m ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst
e₂ :
  m ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd
x : ↑s.pt
eq1 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
eq2 :
  (Hom.hom
        (m ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x
⊢ ↑((ConcreteCategory.hom m) x) =
    ((Hom.hom
          (m ≫
            ofHom
              ((RingHom.fst ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x,
      (Hom.hom
          (m ≫
            ofHom
              ((RingHom.snd ↑A ↑B).comp
                (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
        x)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝⁴ : Bicategory B
C : Type u₂
inst✝³ : Bicategory C
D : Type u₃
inst✝² : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
g h : b✝ ⟶ c✝
η : g ⟶ h
⊢ F.map₂ (f ◁ η) = (asIso (F.mapComp f g)).hom ≫ F.map f ◁ F.map₂ η ≫ (asIso (F.mapComp f h)).inv

Tactic:
dsimp
    rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_right]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: case sup
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁✝ : I₁.FG
hN₂✝ : I₂.FG
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J

Tactic:
obtain ⟨n₂, hn₂⟩ := h₂ (le_sup_right.trans h')

Goal state after:
case sup
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
I₁ I₂ : Submodule R R
hN₁✝ : I₁.FG
hN₂✝ : I₂.FG
h₁ : I₁ ≤ J.radical → ∃ n, I₁ ^ n ≤ J
h₂ : I₂ ≤ J.radical → ∃ n, I₂ ^ n ≤ J
h' : I₁ ⊔ I₂ ≤ J.radical
n₁ : ℕ
hn₁ : I₁ ^ n₁ ≤ J
n₂ : ℕ
hn₂ : I₂ ^ n₂ ≤ J
⊢ ∃ n, (I₁ ⊔ I₂) ^ n ≤ J
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
j₀ : J
h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : J), j ∈ p
this : Nonempty J
α : Type u₁
F : J → α
a : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ j₁ ∈ {j | F j = F j₀} ↔ j₂ ∈ {j | F j = F j₀}

Tactic:
change F j₁ = F j₀ ↔ F j₂ = F j₀
      simp [a f]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE ⋯).IsEquivalence

Tactic:
isEquivalence_ιOfLE_iff

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ P.isoClosure ≤ P.isoClosure
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
hfp : FinitePresentation R A
⊢ FinitePresentation R (MvPolynomial ι A)

Tactic:
rw [iff_quotient_mvPolynomial'] at hfp ⊢

Goal state after:
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
hfp : ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ ι_1 x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
⊢ adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) (Set.range MvPolynomial.X) = ⊤

Tactic:
apply Subalgebra.restrictScalars_injective R

Goal state after:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := ⋯
AX : Type (max w₂ 0) := ⋯
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) (Set.range MvPolynomial.X)) =
    Subalgebra.restrictScalars R ⊤
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inr
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ (algebraMap A B) x - (algebraMap A B) x = 0

Tactic:
sub_self

Goal state after:
case inr
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
⊢ yonedaEquiv.symm ((map α).obj (unop X)).snd = yonedaEquiv.symm (unop X).snd ≫ α

Tactic:
ext _ f

Goal state after:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
x✝ : Cᵒᵖ
f : (yoneda.obj (unop ((map α).obj (unop X)).1)).obj x✝
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm ((map α).obj (unop X)).snd).app x✝)).toFun f =
    (ConcreteCategory.hom ((yonedaEquiv.symm (unop X).snd ≫ α).app x✝)).toFun f
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α

Tactic:
by
  fapply Functor.ext
  · intro X
    simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,
      Functor.comp_obj]
    congr
    ext _ f
    exact (α.naturality_apply f.op (unop X).snd).symm
  · simp

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

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
⊢ k₁ ≫ F.map g = k₂ →
    G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂

Tactic:
a

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁ →
    G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
⊢ k₁ ≫ F.map g = k₂ →
    G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁

Tactic:
a

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : X ⟶ F.obj Z₁
k₂ : X ⟶ F.obj Z₂
g : Z₁ ⟶ Z₂
a : k₁ ≫ F.map g = k₂
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app Z₂ →
    G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app Z₁
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
m : s.pt ⟶ (constCone J X).pt
hm : ∀ (j : J), m ≫ (constCone J X).π.app j = s.π.app j
⊢ m = s.π.app (Classical.arbitrary J)

Tactic:
by simpa using hm (Classical.arbitrary _)

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
m : (constCocone J X).pt ⟶ s.pt
hm : ∀ (j : J), (constCocone J X).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app (Classical.arbitrary J)

Tactic:
by simpa using hm (Classical.arbitrary _)

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
⊢ Z j₁.left j₁.hom → Z j₂.left j₂.hom

Tactic:
a

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
⊢ Z j₂.left j₂.hom
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
⊢ Z j₂.left j₂.hom → Z j₁.left j₁.hom

Tactic:
a

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₂.left j₂.hom
⊢ Z j₁.left j₁.hom
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
⊢ F.map g ≫ k₂ = k₁ →
    c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
      c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f

Tactic:
a

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
⊢ c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
    c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inl
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
i : Fin n
⊢ f' (g i) - f' (g i) = 0

Tactic:
sub_self

Goal state after:
case inl
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
i : Fin n
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
⊢ F.map g ≫ k₂ = k₁ →
    c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
      c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f

Tactic:
a

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
⊢ c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
    c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.op.unop.ι = c.ι

Tactic:
by
  simp [Cofork.unop_ι, Fork.op_π]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B

Tactic:
toAlgebra_algebraMap

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
⊢ (map α).Final

Tactic:
let sC : C ≌ AsSmall.{max u₁ u₂ v₁ v₂} C := AsSmall.equiv

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
⊢ (map α).Final