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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
p q : LocalizedModule S M
⊢ x • (p + q) = x • p + x • q

Tactic:
induction p with | _ m s
  induction q with | _ n t
  rw [smul_def, smul_def, mk_add_mk, mk_add_mk]
  rw [show x • _ = IsLocalization.mk' T _ _ • _ by rw [IsLocalization.mk'_sec (M := S) T]]
  rw [← IsLocalization.mk'_cancel _ _ (IsLocalization.sec S x).2, mk'_smul_mk]
  congr 1
  · simp only [Submonoid.smul_def, smul_add, ← mul_smul, Submonoid.coe_mul]; ring_nf
  · rw [mul_mul_mul_comm]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
s : ↥S
r : R
x : LocalizedModule S M
⊢ (r • x).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ = (RingHom.id R) r • x.liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
refine x.induction_on (fun _ _ ↦ ?_)
    simp_rw [smul'_mk, liftOn_mk, smul'_mk]
    congr!

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
⊢ T.map (T.η.app X) = T.η.app (T.obj X)

Tactic:
simp [← cancel_mono (T.μ.app _)]

Goal state after:
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
M'' : Type u_4
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid M''
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module A M'
inst✝⁵ : IsLocalization S A
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ ↑⋯.unit⁻¹ (f a) = ↑⋯.unit⁻¹ (f a')

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, ← map_smul,
        Module.End.algebraMap_isUnit_inv_apply_eq_iff', ← map_smul]

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : AddCommMonoid M''
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module A M'
inst✝⁵ : IsLocalization S A
inst✝⁴ : Module R M
inst✝³ : Module R M'
inst✝² : Module R M''
inst✝¹ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
p : LocalizedModule S M
a : M
b : ↥S
a' : M
b' c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ f (↑(a, b).2 • a') = f (↑(a', b').2 • a)
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
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm = l

Tactic:
LocalizedModule.lift_unique S g h (l.comp (iso S f).toLinearMap),

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ (l ∘ₗ ↑(iso S f)) ∘ₗ ↑(iso S f).symm = l

R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ (l ∘ₗ ↑(iso S f)) ∘ₗ LocalizedModule.mkLinearMap S M = g
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ (𝟙 f) = 𝟙 (F.map f)

Tactic:
F.map₂_id

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ 𝟙 (F.map f) = 𝟙 (F.map f)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ (𝟙 g) = 𝟙 (F.map g)

Tactic:
F.map₂_id

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ 𝟙 (F.map g) = 𝟙 (F.map g)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂ (eqToHom hfg) = eqToHom ⋯

Tactic:
subst hfg
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂Iso (eqToIso hfg) = eqToIso ⋯

Tactic:
subst hfg
  simp

Goal state after:
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)
⊢ ∃ k f g,
    IsLocalHom (Hom.hom (F.map f)) ∧
      (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
        (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)

Tactic:
refine ⟨one, 𝟙 _, left, inferInstance, ?_⟩

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 (F.map (𝟙 one))) ((ConcreteCategory.hom ((limit.cone F).π.app one)) x) =
    (ConcreteCategory.hom (F.map left)) ((ConcreteCategory.hom ((limit.cone F).π.app zero)) x)
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J → α
h : ∀ (j₁ j₂ : J) (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' X✝ Y✝ : J
f : X✝ ⟶ Y✝
⊢ (Discrete.mk ∘ F) X✝ = (Discrete.mk ∘ F) Y✝

Tactic:
by ext; exact h _ _ f

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
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))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
⊢ Ideal.span s₀ = I

Tactic:
apply leI.antisymm

Goal state after:
case refine_2
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
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := ⋯
s₀ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
⊢ RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) ≤
    Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
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 : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
⊢ G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y → G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y

Tactic:
h₂

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 : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
h₂ : G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y
⊢ G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
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 : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
⊢ G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y → G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y

Tactic:
h₂

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 : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
h₂ : G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
⊢ G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.fst =
    s.π.app j ≫ prod.fst

pp: case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.snd =
    s.π.app j ≫ prod.snd

Tactic:
· erw [assoc, limMap_π, comp_id, limit.lift_π]
              exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm

Goal state after:
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.snd =
    s.π.app j ≫ prod.snd
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
⊢ Ideal.span (Set.range g' ∪ ⇑aeval_h '' ↑s) = RingHom.ker f.toRingHom

Tactic:
apply leI.antisymm

Goal state after:
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) := ⋯
RXm : Type (max w₁ 0) := ⋯
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 := ⋯
g' : Fin n → RXn := ⋯
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := ⋯
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
⊢ RingHom.ker f.toRingHom ≤ Ideal.span s'
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
Z : D
F : C ⥤ D
M : (x : C) → Z ⟶ F.obj x
hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y
x : C
⊢ (liftStar F M hM).hom ≫ (lift F M hM).map (starInitial.to (incl.obj x)) = M x ≫ (inclLift F M hM).hom.app x

Tactic:
by
  simp [incl]

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.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
⊢ c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f → c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f

Tactic:
h₂

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 : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
h₂ : c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f
⊢ c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f
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 : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
⊢ c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f → c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f

Tactic:
h₂

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 : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
h₂ : c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f
⊢ c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_3
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
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x✝ y✝ : RXn
hx✝ : x✝ ∈ adjoin R (Set.range MvPolynomial.X)
hy✝ : y✝ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : x✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ y✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
    x✝ + y✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
h₂

Goal state after:
case refine_3
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
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x✝ y✝ : RXn
hx✝ : x✝ ∈ adjoin R (Set.range MvPolynomial.X)
hy✝ : y✝ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : x✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
h₂ : y✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ x✝ + y✝ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_4
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
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
p₁ p₂ : RXn
hx✝ : p₁ ∈ adjoin R (Set.range MvPolynomial.X)
hy✝ : p₂ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : p₁ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid →
    p₁ * p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid

Tactic:
h₂

Goal state after:
case refine_4
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
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
p₁ p₂ : RXn
hx✝ : p₁ ∈ adjoin R (Set.range MvPolynomial.X)
hy✝ : p₂ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : p₁ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
h₂ : p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ p₁ * p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
⊢ ∀ (d : Grothendieck F), IsConnected (StructuredArrow d (pre F G))

Tactic:
rintro ⟨d, f⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
⊢ IsConnected (StructuredArrow { base := d, fiber := f } (pre F G))
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
  let F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}
  let G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}
  let α' : F' ⟶ G' := whiskerLeft _ (whiskerRight α _)
  have : ∀ X, Final (α'.app X).toFunctor := fun X =>
    inferInstanceAs (AsSmall.equiv.inverse ⋙ _ ⋙ AsSmall.equiv.functor).Final
  have hα' : (map α').Final := final_map_small _
  dsimp only [α', ← Equivalence.symm_functor] at hα'
  have i := mapWhiskerLeftIsoConjPreMap sC.symm (whiskerRight α Cat.asSmallFunctor)
    ≪≫ isoWhiskerLeft _ (isoWhiskerRight (mapWhiskerRightAsSmallFunctor α) _)
  have := final_of_natIso i
  rwa [← final_iff_equivalence_comp, ← final_iff_comp_equivalence,
    ← final_iff_equivalence_comp, ← final_iff_comp_equivalence] at this

Goal state after: