mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n ↦ u n / ↑n) '' Ici 1) ≤ u n / ↑n

Tactic:
exact csInf_le (hbdd.mono <| image_subset_range _ _) ⟨n, hn.bot_lt, rfl⟩

Goal state after:
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ ↑S.commutant ↔ ∀ g ∈ S, g * z = z * g

Tactic:
coe_commutant

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ (↑S).centralizer ↔ ∀ g ∈ S, g * z = z * g
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
h : ∀ x ∈ S.commutant, e * (x * e) = x * e
x : H →L[ℂ] H
hx : x ∈ S.commutant
⊢ e * (x * e) = e * x

Tactic:
simpa [he.isSelfAdjoint.star_eq] using! congr(star $(h _ (star_mem hx)))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ φ f g ≫ π f g = 0

Tactic:
dsimp [φ, π]
  ext
  · rw [biprod.inl_desc_assoc, assoc, biprod.inl_desc, comp_zero,
      ← assoc, cokernel.condition]
  · simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : InjectiveResolution X
X' : C
R' : InjectiveResolution X'
f : X ⟶ X'
φ : R.Hom R' f
n : ℤ
m : ℕ
h : ↑m = n
⊢ φ.hom'.f n = (R.cochainComplexXIso n m h).hom ≫ φ.hom.f m ≫ (R'.cochainComplexXIso n m h).inv

Tactic:
simp [hom',
    HomologicalComplex.extendMap_f _ ComplexShape.embeddingUpNat (i := m) (i' := n) (by simpa),
    cochainComplexXIso]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
⊢ pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
      (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) ≫ d f =
    0

Tactic:
refine (Preadditive.isSeparator_iff G).1 hG _ (fun h => ?_)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
h : G ⟶ pullback (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g))
⊢ h ≫
      pullback.fst (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) (kernel.ι (d g)) ≫
        (∑ a ∈ F.attach, Sigma.π (fun a ↦ G) a ≫ Sigma.ι (fun x ↦ G) (↑a).as) ≫ d f =
    0
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
inst✝ : HasDerivedCategory C
x : Cocycle ((singleFunctor C 0).obj X) R.cochainComplex ↑n
⊢ (R.extEquivCohomologyClass.symm (CohomologyClass.mk x)).hom =
    (ShiftedHom.mk₀ 0 ⋯ ((DerivedCategory.singleFunctorIsoCompQ C 0).hom.app X)).comp
      ((ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q).comp
        (ShiftedHom.mk₀ 0 ⋯ (inv (DerivedCategory.Q.map R.ι') ≫ (DerivedCategory.singleFunctorIsoCompQ C 0).inv.app Y))
        ⋯)
      ⋯

Tactic:
by
  change SmallShiftedHom.equiv _ _ ((CohomologyClass.mk x).toSmallShiftedHom.comp _ _) = _
  simp only [SmallShiftedHom.equiv_comp, CohomologyClass.equiv_toSmallShiftedHom_mk,
    SmallShiftedHom.equiv_mk₀Inv, isoOfHom, asIso_inv,
    DerivedCategory.singleFunctorIsoCompQ, Iso.refl_hom, NatTrans.id_app, Iso.refl_inv,
    ShiftedHom.mk₀_id_comp]
  congr
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (F.rightDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (J.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)) ≫
      HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n

Tactic:
rw [assoc, ← Functor.map_comp_assoc,
    InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality f I J φ comm F,
    Functor.map_comp, assoc]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map
          ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) =
    (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫
        HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
x✝ : Epi (L.map f)
⊢ P.epiModSerre f

Tactic:
by
    have hf : L.map (cokernel.π f) = 0 := by
      rw [← cancel_epi (L.map f), comp_zero, ← L.map_comp,
        cokernel.condition, L.map_zero]
    simpa [hf] using! map_comp_eq_zero_iff_of_epi_mono L P (cokernel.π f) (𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : ActionCategory G X
f : a ⟶ b
⊢ P f

Tactic:
by
  refine cast ?_ (hyp b.back f.val)
  rcases a with ⟨⟨⟩, a : X⟩
  rcases b with ⟨⟨⟩, b : X⟩
  rcases f with ⟨g : G, h : g • a = b⟩
  cases inv_smul_eq_iff.mpr h.symm
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
this : ∀ (W : D) (z : L.obj Y ⟶ W), L.map f ≫ z = 0 → ∃ l, L.map (cokernel.π f) ≫ l = z
s : Cofork (L.map f) 0
x✝¹ x✝ : (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L).pt ⟶ s.pt
h₁ : Cofork.π (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L) ≫ x✝¹ = s.π
h₂ : Cofork.π (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) L) ≫ x✝ = s.π
⊢ x✝¹ = x✝

Tactic:
simpa [cancel_epi] using h₁.trans h₂.symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ exactFunctor C E (L ⋙ Localization.lift F.obj hF L)

Tactic:
exact ObjectProperty.prop_of_iso _ (Localization.fac F.obj hF L).symm F.property

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : Quot Rel), Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel (Hom₂.id X)) f = f

Tactic:
rintro f g ⟨η⟩

Goal state after:
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
f✝ : Quot Rel
η : Hom₂ f g
⊢ Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel (Hom₂.id f)) (Quot.mk Rel η) = Quot.mk Rel η
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : Quot Rel), Quot.map₂ Hom₂.vcomp ⋯ ⋯ f (Quot.mk Rel (Hom₂.id Y)) = f

Tactic:
rintro f g ⟨η⟩

Goal state after:
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
f✝ : Quot Rel
η : Hom₂ f g
⊢ Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η) (Quot.mk Rel (Hom₂.id g)) = Quot.mk Rel η
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    Quot.lift (liftHom₂ F) ⋯ (η ▷ h) =
      (Iso.refl (liftHom F (f ≫ h))).hom ≫ Quot.lift (liftHom₂ F) ⋯ η ▷ liftHom F h ≫ (Iso.refl (liftHom F (g ≫ h))).inv

Tactic:
intro _ _ _ _ _ η h; dsimp; induction η using Quot.rec <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
⊢ t ≫ r = φ

Tactic:
hφ

Goal state after:
B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
⊢ φ = φ
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
⊢ ∀ {X Y : (i : I) × C i} (f : X ⟶ Y),
    q.map f ≫
        (match Y with
          | ⟨i, X⟩ => (h i).app X).hom =
      (match X with
          | ⟨i, X⟩ => (h i).app X).hom ≫
        (desc F).map f

Tactic:
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ q.map (SigmaHom.mk f) ≫
      (match ⟨i, Y✝⟩ with
        | ⟨i, X⟩ => (h i).app X).hom =
    (match ⟨i, X⟩ with
        | ⟨i, X⟩ => (h i).app X).hom ≫
      (desc F).map (SigmaHom.mk f)
Module: Mathlib.CategoryTheory.Sigma.Basic

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    (Functor.sigma F).map f ≫ SigmaHom.mk ((α Y.fst).app Y.snd) =
      SigmaHom.mk ((α X.fst).app X.snd) ≫ (Functor.sigma G).map f

Tactic:
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (D i)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ (Functor.sigma F).map (SigmaHom.mk f) ≫ SigmaHom.mk ((α ⟨i, Y✝⟩.fst).app ⟨i, Y✝⟩.snd) =
    SigmaHom.mk ((α ⟨i, X⟩.fst).app ⟨i, X⟩.snd) ≫ (Functor.sigma G).map (SigmaHom.mk f)
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: case none
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
hb : none ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1 ∈ f a, ⟨none, hb⟩ ∈ Part.some ⟨some a_1, ⋯⟩) ↔ ↑⟨none, hb⟩ = (partialFunToPointed.map f).toFun ↑⟨some a, ⋯⟩

Tactic:
exact (hb rfl).elim

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a → b ∈ f.fix a'

pp: case mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a' → b ∈ f.fix a

Tactic:
· intro h
    obtain h' | ⟨a, h', e'⟩ := mem_fix_iff.1 h <;> cases Part.mem_unique ha' h'
    exact e'

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a a' : α
ha' : Sum.inr a' ∈ f a
b : β
⊢ b ∈ f.fix a' → b ∈ f.fix a
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih ↦
      Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
        (fun b' e ↦
          have e := ⋯;
          hbase a' ⋯)
        (fun a'' e ↦
          have e := ⋯;
          hind a' a'' ⋯ e (ih a'' e))
        ⋯) =
    hbase a fa

Tactic:
fixInduction_spec

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a : α
h : b ∈ f.fix a
fa : Sum.inl b ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x ↦ (f a).get ⋯ = x → C a) ((f a).get ⋯)
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hbase a fa
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ (fixInduction h fun a' h ih ↦
      Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
        (fun b' e ↦
          have e := ⋯;
          hbase a' ⋯)
        (fun a'' e ↦
          have e := ⋯;
          hind a' a'' ⋯ e (ih a'' e))
        ⋯) =
    hind a a' h' fa
      (fixInduction h' fun a' h ih ↦
        Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → (fun x ↦ C x) a') ((f a').get ⋯)
          (fun b' e ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun a'' e ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)

Tactic:
fixInduction_spec

Goal state after:
α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ Sum.casesOn (motive := fun x ↦ (f a).get ⋯ = x → C a) ((f a).get ⋯)
      (fun b' e ↦
        have e := ⋯;
        hbase a ⋯)
      (fun a'' e ↦
        have e := ⋯;
        hind a a'' ⋯ e
          ((fun x h' ↦
              fixInduction ⋯ fun a' h ih ↦
                Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → C a') ((f a').get ⋯)
                  (fun b' e ↦
                    have e := ⋯;
                    hbase a' ⋯)
                  (fun a'' e ↦
                    have e := ⋯;
                    hind a' a'' ⋯ e (ih a'' e))
                  ⋯)
            a'' e))
      ⋯ =
    hind a a' h' fa
      (fixInduction h' fun a' h ih ↦
        Sum.casesOn (motive := fun x ↦ (f a').get ⋯ = x → (fun x ↦ C x) a') ((f a').get ⋯)
          (fun b' e ↦
            have e := ⋯;
            hbase a' ⋯)
          (fun a'' e ↦
            have e := ⋯;
            hind a' a'' ⋯ e (ih a'' e))
          ⋯)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
⊢ fst f g ≫ f = snd f g ≫ g

Tactic:
rw [condition]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Algebra F
h : Limits.IsInitial A
⊢ A.str ≫ strInv h = 𝟙 (F.obj A.a)

Tactic:
by
  rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]
  congr
  exact left_inv h

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst✝¹ : p.IsStronglyCartesian f' φ'
inst✝ : p.IsHomLift f'' φ''
⊢ map p f' φ' H' φ'' ≫ map p f φ H φ' = map p f φ ⋯ φ''

Tactic:
apply map_uniq p f φ
  simp only [assoc, fac]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ) ≫ φ = τ

pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)

Tactic:
· apply IsStronglyCartesian.ext p g ψ (h ≫ f) (by simp)

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
K : Type u₄
inst✝² : Category.{v₄, u₄} K
inst✝¹ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝ : HasFunctorEnrichedHom V F₁ F₂
X : J
⊢ precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
      (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂))

Tactic:
ext j
    -- this was produced by `simp?`
    simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π,
      Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
      eHomWhiskerLeft_id, comp_id, id_comp]
    congr 1
    simp [Under.map, Comma.mapLeft]
    rfl

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
A X : C
inst✝ : IsConnected A
⊢ Nat.card (A ⟶ X) ≤ Nat.card (F.obj X).obj

Tactic:
by
  apply Nat.card_le_card_of_injective
  exact evaluation_injective_of_isConnected F A X (Classical.arbitrary _)

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Full

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i

Tactic:
let is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i => (functorToAction F).obj (gZ i) :=
    PreservesCoproduct.iso (functorToAction F) gZ

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
F : C ⥤ FintypeCat
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
X : C
Y : Action FintypeCat (Aut F)
i : Y ⟶ (functorToAction F).obj X
inst✝ : Mono i
ι : Type
hf : Finite ι
f : ι → Action FintypeCat (Aut F)
t : ∐ f ≅ Y
hc : ∀ (i : ι), IsConnected (f i)
i' : (j : ι) → f j ⟶ (functorToAction F).obj X := fun j ↦ Sigma.ι f j ≫ t.hom ≫ i
gZ : ι → C
gf : (i : ι) → gZ i ⟶ X
gu : (i : ι) → f i ≅ (functorToAction F).obj (gZ i)
h✝¹ : ∀ (i : ι), IsConnected (gZ i)
h✝ : ∀ (i : ι), Mono (gf i)
h : ∀ (i : ι), i' i = (gu i).hom ≫ (functorToAction F).map (gf i)
is2 : (functorToAction F).obj (∐ gZ) ≅ ∐ fun i ↦ (functorToAction F).obj (gZ i) :=
  PreservesCoproduct.iso (functorToAction F) gZ
⊢ ∃ Z f u, Mono f ∧ u.hom ≫ (functorToAction F).map f = i
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
h : Nonempty (F.obj X).obj
⊢ ∃ A x, IsGalois A

Tactic:
by
  obtain ⟨x⟩ := h
  obtain ⟨A, f, a, h1, _⟩ := exists_hom_from_galois_of_fiber F X x
  exact ⟨A, f, h1⟩

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Prorepresentability

Goal state before:
pp: C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
⊢ IsIso f

Tactic:
rw [← isUnit_iff_isIso]

Goal state after:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
f : End F
⊢ IsUnit f