mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b = ↑(count (normalize a) (normalizedFactors b))

Tactic:
apply le_antisymm
  · apply Order.le_of_lt_add_one
    rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge,
      le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
    simp
  rw [le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
⊢ a ∣ b ↔ ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b

Tactic:
refine ⟨fun h _ _ ↦ emultiplicity_le_emultiplicity_of_dvd_right h, fun h ↦ ?_⟩

Goal state after:
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b : R
ha : a ≠ 0
h : ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b
⊢ a ∣ b
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
⊢ x * y ∈ closure s

Tactic:
have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
this : (AddMonoidHom.mulLeft x) y ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
⊢ x * y ∈ closure s
Module: Mathlib.RingTheory.Jacobson.Radical

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ jacobson R M
⊢ comap f (map f (jacobson R M)) = jacobson R M

Tactic:
comap_map_eq_self le

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
surj : Function.Surjective ⇑f
le : f.ker ≤ jacobson R M
⊢ jacobson R M = jacobson R M
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
r : R
h : r ∈ I.jacobson
⊢ ∃ s, s * (r + 1) - 1 ∈ I

Tactic:
obtain ⟨s, hs⟩ := mem_jacobson_iff.1 h 1
  use s
  rw [mul_add, mul_one]
  simpa using hs

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasStrictTerminalObjects C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal (F.obj j)
inst✝ : Subsingleton (i ⟶ i)
⊢ IsIso (limit.π F i)

Tactic:
refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
    · exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _
    · intro j k f
      split_ifs with h h_1 h_1
      · cases h
        cases h_1
        obtain rfl : f = 𝟙 _ := Subsingleton.elim _ _
        simp
      · cases h
        have : IsIso (F.map f) := (H _ h_1).isIso_from _
        rw [← IsIso.comp_inv_eq]
        apply (H _ h_1).hom_ext
      · cases h_1
        apply (H _ h).hom_ext
      · apply (H _ h).hom_ext
    · ext
      rw [assoc, limit.lift_π]
      dsimp only
      split_ifs with h
      · cases h
        rw [id_comp, eqToHom_refl]
        exact comp_id _
      · apply (H _ h).hom_ext
    · simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| η ⊗ₘ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
rw [← Category.id_comp η, ← tensorHom_comp_tensorHom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N P : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj P
| (𝟙 (𝟙_ C) ⊗ₘ (λ_ (𝟙_ C)).inv) ≫ (η ⊗ₘ η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Mon

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ M (𝟙_ C) M (𝟙_ C) ≫ (μ ⊗ₘ (λ_ (𝟙_ C)).hom)) ≫ (ρ_ M).hom = ((ρ_ M).hom ⊗ₘ (ρ_ M).hom) ≫ μ

Tactic:
by
  rw [← Category.id_comp μ, ← Category.comp_id (λ_ (𝟙_ C)).hom, ← tensorHom_comp_tensorHom]
  simp only [tensorHom_id, id_tensorHom]
  slice_lhs 3 4 => rw [rightUnitor_naturality]
  slice_lhs 1 3 => rw [← rightUnitor_monoidal]
  simp only [Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Mono g
⊢ ∀ {Z : C} (g h : Z ⟶ P), g ≫ fst = h ≫ fst → g = h

Tactic:
intro W fst' snd' heq

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Mono g
W : C
fst' snd' : W ⟶ P
heq : fst' ≫ fst = snd' ≫ fst
⊢ fst' = snd'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
this : HasPullback f g
⊢ IsIso fst

Tactic:
← h.isoPullback_hom_fst

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.fst f g)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit t₂
s : PushoutCocone i₁ (f₁ ≫ f₂)
⊢ i₁ ≫ s.inl = f₁ ≫ f₂ ≫ s.inr

Tactic:
rw [s.condition, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
⊢ ∀ {Z : C} (g h : P ⟶ Z), inl ≫ g = inl ≫ h → g = h

Tactic:
intro W fst' snd' heq

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst : Epi g
W : C
fst' snd' : P ⟶ W
heq : inl ≫ fst' = inl ≫ snd'
⊢ fst' = snd'
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst✝¹ : HasBinaryCoproduct A X
inst✝ : HasBinaryCoproduct B X
s : PushoutCocone coprod.inl f
⊢ { l //
    (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ l = s.inl ∧
      (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).pt ⟶ s.pt},
          (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inl ≫ m = s.inl →
            (PushoutCocone.mk (coprod.map f (𝟙 X)) coprod.inl ⋯).inr ≫ m = s.inr → m = l }

Tactic:
by
    refine ⟨coprod.desc s.inr (coprod.inr ≫ s.inl), ?_, ?_, ?_⟩
    · ext
      · simp [PushoutCocone.condition]
      · simp
    · simp
    · intro m h₁ h₂
      dsimp at m h₁ h₂ ⊢
      ext
      · simpa using h₂
      · simp [← h₁]

Goal state after:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (bicompl F G H)

Tactic:
constructor <;> intros

Goal state after:
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α✝ : Type u_1
β✝ : Type u_2
x✝ : bicompl F G H α✝ β✝
⊢ bimap id id x✝ = x✝

case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝⁵ : Bifunctor F
G : Type u_1 → Type u₀
H : Type u_2 → Type u₁
inst✝⁴ : Functor G
inst✝³ : Functor H
inst✝² : LawfulFunctor G
inst✝¹ : LawfulFunctor H
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u_1
β₀✝ β₁✝ β₂✝ : Type u_2
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompl F G H α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
⊢ LawfulBifunctor (bicompr G F)

Tactic:
constructor <;> intros

Goal state after:
case id_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α✝ : Type u₀
β✝ : Type u₁
x✝ : bicompr G F α✝ β✝
⊢ bimap id id x✝ = x✝

case bimap_bimap
F : Type u₀ → Type u₁ → Type u₂
inst✝³ : Bifunctor F
G : Type u₂ → Type u_1
inst✝² : Functor G
inst✝¹ : LawfulFunctor G
inst✝ : LawfulBifunctor F
α₀✝ α₁✝ α₂✝ : Type u₀
β₀✝ β₁✝ β₂✝ : Type u₁
f✝ : α₀✝ → α₁✝
f'✝ : α₁✝ → α₂✝
g✝ : β₀✝ → β₁✝
g'✝ : β₁✝ → β₂✝
x✝ : bicompr G F α₀✝ β₀✝
⊢ bimap f'✝ g'✝ (bimap f✝ g✝ x✝) = bimap (f'✝ ∘ f✝) (g'✝ ∘ g✝) x✝
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type u_3
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Submonoid R
t : Finset ι
a : ι → A
s : ι → ↥S
⊢ ∏ i ∈ t, mk (a i) (s i) = mk (∏ i ∈ t, a i) (∏ i ∈ t, s i)

Tactic:
by
  induction t using Finset.cons_induction <;> simp [OreLocalization.one_def, *, mk_mul_mk]

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

Goal state before:

Tactic:
_ = a.2 • a.1 • s • p'.2 • p.1 := by
            simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]; ring_nf
          _ = a.2 • a.1 • s • p.2 • p'.1 := by rw [h]
          _ = s • (a.2 * p.2) • a.1 • p'.1 := by
            simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]; ring_nf

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x

Tactic:
by
  induction x with
  | neg_one => use -1; rfl
  | of b => exact ⟨FreeRing.of b, rfl⟩
  | add _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
  | mul _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩

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''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x : M'
⊢ ∃ x_1, x_1.2 • x = (f ∘ₗ ↑e) x_1.1

Tactic:
by
    obtain ⟨⟨p, s⟩, h⟩ := hf.surj x
    exact ⟨⟨e.symm p, s⟩, by simpa using h⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : Comonad C
A B : G.Coalgebra
f : A ⟶ B
inst✝ : IsIso f.f
⊢ B.a ≫ G.map (inv f.f) = inv f.f ≫ A.a

Tactic:
by
          rw [IsIso.eq_inv_comp f.f, ← f.h_assoc]
          simp

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ ↑⋯.unit⁻¹ (g (↑(b * b') • a)) = g (b' • a)

Tactic:
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff]
        simp only [Submonoid.coe_mul, LinearMap.map_smul_of_tower]
        rw [mul_smul, Submonoid.smul_def]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₁ : Type u_7
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
S₁ S₂ : Submonoid R
h : S₁ ≤ S₂
f₁ : M →ₗ[R] M₁
f₂ : M →ₗ[R] M₂
inst✝¹ : IsLocalizedModule S₁ f₁
inst✝ : IsLocalizedModule S₂ f₂
m : M
s : ↥S₁
⊢ (liftOfLE S₁ S₂ h f₁ f₂) (mk' f₁ m s) = mk' f₂ m ⟨↑s, ⋯⟩

Tactic:
by
  apply ((Module.End.isUnit_iff _).mp (map_units f₂ ⟨s, h s.2⟩)).1
  simp only [Module.algebraMap_end_apply, ← map_smul, ← Submonoid.smul_def, mk'_cancel']
  rw [liftOfLE, lift_apply]
  exact (mk'_cancel' (S := S₂) f₂ m ⟨s.1, h s.2⟩).symm

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
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.inv = inv (F.map₂ η.hom)

Tactic:
by
  rw [← F.map₂_inv, IsIso.Iso.inv_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: X Y : Type u
x✝¹ : Cone (pair X Y)
x✝ : x✝¹.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone X Y).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun x ↦ ((ConcreteCategory.hom (BinaryFan.fst x✝¹)) x, (ConcreteCategory.hom (BinaryFan.snd x✝¹)) x)

Tactic:
ext x
    apply Prod.ext
    exacts [ConcreteCategory.congr_hom (w ⟨left⟩) x, ConcreteCategory.congr_hom (w ⟨right⟩) x]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ uliftYoneda.{w, v, u}.map (↑(unop f)).unop ≫ (CostructuredArrow.mk (uliftYonedaEquiv.symm (unop Y✝).snd)).hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm (unop X✝).snd)).hom

Tactic:
by
        dsimp
        rw [← uliftYonedaEquiv_symm_map, map_snd]

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
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂

Tactic:
intro Z₁ Z₂ k₁ k₂ g a z

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₂
z : 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
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁

Tactic:
intro Z₁ Z₂ k₁ k₂ g a z

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

Tactic:
intro Z₁ Z₂ k₁ k₂ g a z

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₁
z : 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.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
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f

Tactic:
intro Z₁ Z₂ k₁ k₂ g a z

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₁
z : 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.RegularMono

Goal state before:
pp: case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
⊢ m ≫ (PullbackCone.mk f g comm).snd = p ≫ (PullbackCone.mk f g comm).snd

Tactic:
exact z

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 : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
⊢ (StructuredArrow.mk { base := X✝.hom, fiber := _root_.id (𝟙 ((F.map X✝.hom).toFunctor.obj f)) }).right.base ⟶
    (StructuredArrow.mk { base := Y✝.hom, fiber := _root_.id (𝟙 ((F.map Y✝.hom).toFunctor.obj f)) }).right.base

Tactic:
by exact g.right

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
⊢ { l // (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }

Tactic:
refine ⟨p, hp₁, ?_⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
⊢ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = p
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: case h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right✝ : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (PushoutCocone.mk h k comm).inl ≫ m = (PushoutCocone.mk h k comm).inl ≫ p

Tactic:
exact z

Goal state after: