mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ (algebraMap R B) (x ^ d.natAbs) * mk' B 1 (Submonoid.pow x (-d).natAbs) = 1

pp: case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ -d ≤ 0

Tactic:
Int.natAbs_neg,

Goal state after:
case neg
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ (algebraMap R B) (x ^ d.natAbs) * mk' B 1 (Submonoid.pow x d.natAbs) = 1

case neg.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : 0 < d
⊢ -d ≤ 0
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : DecidableEq R
s : Finset S
x : S
hx : x ∈ ↑s
⊢ (fun x ↦ ↑(commonDenomOfFinset M s) • x) x ∈ ⇑(algebraMap R S) '' (fun t ↦ integerMultiple M s id t) '' ↑s.attach

Tactic:
exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integerMultiple M s id _⟩

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 O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)) ≫ (f ⊗ₘ g) = (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, one_hom, one_hom]

Goal state after:
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i : ι
⊢ ((ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)

Tactic:
suffices ((b.ofIsLocalizedModule Rₛ S f).repr.toLinearMap.restrictScalars R) ∘ₗ f =
      Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ b.repr.toLinearMap by
    exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
b : Basis ι R M
m : M
i : ι
⊢ ↑R ↑(ofIsLocalizedModule Rₛ S f b).repr ∘ₗ f = Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ) ∘ₗ ↑b.repr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case h₂
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
m : B ⨿ X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ coprod.inr ≫ m = coprod.inr ≫ coprod.desc s.inr (coprod.inr ≫ s.inl)

Tactic:
simp [← h₁]

Goal state after:
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₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
⊢ i₁ ≫ t₁.inl ≫ s.inl = (f₁ ≫ f₂) ≫ s.inr

Tactic:
rw [reassoc_of% t₁.condition, ← hi₂, s.condition, Category.assoc]

Goal state after:
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₁.pasteHoriz t₂ hi₂)
⊢ IsColimit t₂

Tactic:
by
  apply PushoutCocone.isColimitAux'
  intro s
  -- Obtain the induced morphism from the universal property of the big square
  obtain ⟨l, hl, hl'⟩ := PushoutCocone.IsColimit.desc' H' (g₁ ≫ s.inl) s.inr
    (by rw [reassoc_of% t₁.condition, ← hi₂, s.condition, Category.assoc])
  refine ⟨l, ?_, hl', ?_⟩
  -- To check that `l` is compatible with the projections, we use the universal property of `t₁`
  · simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hl hl'
    apply PushoutCocone.IsColimit.hom_ext H hl
    rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']
  -- Uniqueness of the lift follows from the universal property of the big square
  · intro m hm₁ hm₂
    apply PushoutCocone.IsColimit.hom_ext H'
    · simpa [← hm₁] using hl.symm
    · simpa [← hm₂] using hl'.symm

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑↑i).IsSupported s
⊢ (↑↑i + 1).IsSupported s

Tactic:
exact isSupported_add hi isSupported_one

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ F.map ((T.η ≫ i.hom).app X) ≫ ((i.inv ◫ i.inv) ≫ T.μ ≫ i.hom).app X = 𝟙 (F.obj ((𝟭 C).obj X))

Tactic:
simp only [NatTrans.comp_app, Functor.map_comp, comp_obj, NatTrans.hcomp_app,
      Category.assoc, NatTrans.naturality_assoc]
    slice_lhs 2 4 =>
      simp only [← T.map_comp]
    simp

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
N : Type u_6
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ m, m * ↑x ∈ S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule S f
x₁ x₂ : M
e : f x₁ = f x₂
⊢ ∃ c, c • x₁ = c • x₂

Tactic:
obtain ⟨c, hc⟩ := IsLocalizedModule.exists_of_eq (S := S) (f := f) e
    exact ⟨⟨c, h c.2⟩, hc⟩

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
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f m s = 0 ↔ f m = 0

Tactic:
mk'_eq_iff,

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
m : M
s : ↥S
⊢ f m = s • 0 ↔ f m = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ mk' (LocalizedModule.mkLinearMap S M) m s = LocalizedModule.mk m s

Tactic:
mk'_eq_iff,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ (LocalizedModule.mkLinearMap S M) m = s • LocalizedModule.mk m s
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom ≫
    G.map (F.map f) ◁ (G.mapComp (F.map g) (F.map h) ≫ G.map₂ (F.mapComp g h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h))

pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.mapComp f (g ≫ h))

Tactic:
rw [Bicategory.whiskerLeft_comp, assoc, ← mapComp_naturality_right, ← map₂_associator_assoc]

Goal state after:
case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
    G.mapComp (F.map f ≫ F.map g) (F.map h) ≫
      G.map₂ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ G.map₂ (F.map f ◁ F.mapComp g h)

case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.mapComp f (g ≫ h))
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : Q.FullSubcategory
Y : D
hY : Q Y
⊢ P ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })

Tactic:
by
    rw [← h]
    exact Q.prop_of_iso (e.counitIso.app Y).symm hY

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
obtain ⟨P', _, hP'⟩ := EssentiallySmall.exists_small_le' P

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inl
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 : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) ((MvPolynomial.map (algebraMap R A)) x) = 0

Tactic:
rw [MvPolynomial.aeval_map_algebraMap (R := R) (A := A), ← aeval_unique]
        have := Ideal.subset_span hx
        rwa [hs] at this

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
    prelaxfunctor.map₂ (Bicategory.associator f g h).hom =
      (Cat.Hom.isoMk (mapComp (f ≫ g).toFunctor h.toFunctor)).hom ≫
        Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f.toFunctor g.toFunctor)).hom (prelaxfunctor.map h) ≫
          (Bicategory.associator (prelaxfunctor.map f) (prelaxfunctor.map g) (prelaxfunctor.map h)).hom ≫
            Bicategory.whiskerLeft (prelaxfunctor.map f) (Cat.Hom.isoMk (mapComp g.toFunctor h.toFunctor)).inv ≫
              (Cat.Hom.isoMk (mapComp f.toFunctor (g ≫ h).toFunctor)).inv

Tactic:
intros
    dsimp
    ext X
    cases X
    · simp
    · rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom ⋯
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map (f ≫ g)).toFunctor ⋙ fib c₃

Tactic:
simp only [Functor.map_comp]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
fib : (c : C) → ↑(F.obj c) ⥤ E
hom : {c c' : C} → (f : c ⟶ c') → fib c ⟶ (F.map f).toFunctor ⋙ fib c'
hom_id : ∀ (c : C), hom (𝟙 c) = eqToHom (@_proof_145 C inst✝² F E inst✝ fib c)
c₁ c₂ c₃ : C
f : c₁ ⟶ c₂
g : c₂ ⟶ c₃
⊢ (F.map f).toFunctor ⋙ (F.map g).toFunctor ⋙ fib c₃ = (F.map (f ≫ g)).toFunctor ⋙ fib c₃

Tactic:
simp only [Functor.map_comp]; rfl

Goal state after:
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)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ ((prod.functor.obj X).mapCone c).π.app j = s.π.app j
⊢ m ≫ prod.snd = prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫ prod.snd

Tactic:
· rw [limit.lift_π]
              apply l.uniq (forgetCone s)
              intro j
              simp [← L j]

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ G.Final

Tactic:
rw [final_iff_comp_equivalence G s₃.functor, final_iff_equivalence_comp s₂.inverse,
    final_iff_isIso_colimit_pre]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
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
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}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = p

Tactic:
intro m w

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
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.ι
⊢ m = p
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk g
h : RegularEpi f
⊢ h.left ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom

Tactic:
reassoc_of% h.w

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk g
h : RegularEpi f
⊢ h.right ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom
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
⊢ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = p

Tactic:
intro m w

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
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
⊢ m = p
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄ =
    pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄

Tactic:
rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_snd]

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

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P.retractClosure ≤ P

Tactic:
intro X ⟨Y, hY, ⟨e⟩⟩

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsStableUnderRetracts
X Y : C
hY : P Y
e : Retract X Y
⊢ P X
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (lift (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁)
          (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ⋯ ≫
        lift (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) ⋯) ≫
      snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    𝟙 (pullback (fst (fst f' g') i₁) (fst (snd f' g') i₂)) ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂)

Tactic:
· apply pullback.hom_ext
      · apply pullback.hom_ext
        · simp only [Category.assoc, lift_snd_assoc, lift_fst_assoc, lift_fst, Category.id_comp]
          rw [← condition_assoc, condition]
        · simp only [Category.assoc, lift_snd, lift_fst_assoc, lift_snd_assoc, Category.id_comp]
          rw [condition]
      · simp only [Category.assoc, lift_snd, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
⊢ P.universally g

Tactic:
by
  introv X' h
  have := h.hasPullback
  rw [← h.isoPullback_hom_fst, P.cancel_left_of_respectsIso]
  exact H ..

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ counit ((antipode R) a) = ∑ x ∈ (ℛ R a).index, counit ((ℛ R a).left x * (antipode R) ((ℛ R a).right x))

Tactic:
counit_mul,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
⊢ counit ((antipode R) a) = ∑ x ∈ (ℛ R a).index, counit ((ℛ R a).left x) * counit ((antipode R) ((ℛ R a).right x))
Module: Mathlib.RingTheory.HopfAlgebra.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
⊢ LinearMap.mul' S (B ⊗[R] A) ∘ₗ
      LinearMap.lTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul =
    Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit

Tactic:
ext x y
    convert! congr($(mul_antipode_lTensor_comul_apply (R := S) x) ⊗ₜ[R]
      $(mul_antipode_lTensor_comul_apply (R := R) y)) using 1
    · dsimp [Algebra.TensorProduct.one_def]
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := R) y with y₁ y₂
      simp
    · dsimp [Algebra.TensorProduct.one_def]
      simp [Algebra.algebraMap_eq_smul_one, smul_tmul']

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z = (ρ_ ((ihom X).obj Y)).hom ≫ (ihom X).map f

Tactic:
← cancel_epi (ρ_ _).inv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : Y ⟶ Z
⊢ (ρ_ ((ihom X).obj Y)).inv ≫ (ihom X).obj Y ◁ curry' f ≫ comp X Y Z =
    (ρ_ ((ihom X).obj Y)).inv ≫ (ρ_ ((ihom X).obj Y)).hom ≫ (ihom X).map f
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < t.depth

Tactic:
cases t
  apply Nat.succ_pos

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s t : Submodule K V
inst✝ : FiniteDimensional K ↥t
hst : s < t
⊢ comap t.subtype s ≠ ⊤

Tactic:
by simp [not_le_of_gt hst]

Goal state after: