mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x ↔ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
constructor
  · intro h
    apply (abs_eval_T_real_eq_one_iff hn x).mp
    apply eq_of_le_of_ge (abs_eval_T_real_le_one n (by grind))
    refine h.elim (fun h => ?_) (fun h => ?_)
    · refine le_abs.mpr (.inr (le_neg_of_le_neg ?_))
      have := isMinOn_iff.mp h (cos (1 * π / n)) (by grind [abs_cos_le_one])
      rw [(eval_T_real_eq_neg_one_iff hn (cos (1 * π / n))).mpr ⟨1, Nat.one_le_iff_ne_zero.mpr hn,
        by simp⟩] at this
      assumption
    · refine le_abs.mpr (.inl ?_)
      have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)
      rw [(eval_T_real_eq_one_iff hn _).mpr ⟨0, by simp, by simp⟩] at this
      assumption
  · rintro ⟨k, hk, hx⟩
    rw [hx]
    exact isExtrOn_T_real hn hk

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ 1 + sineTerm x n ≠ 0

Tactic:
simp only [sineTerm, ne_eq]

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 + -x ^ 2 / (↑n + 1) ^ 2 = 0
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case ofNat
n : ℕ
⊢ fib (↑n + 2) = ↑(Nat.fib n) + fib (↑n + 1)

Tactic:
← Nat.cast_ofNat,

Goal state after:
case ofNat
n : ℕ
⊢ fib (↑n + ↑2) = ↑(Nat.fib n) + fib (↑n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : -↑(2 * n + 1) + 1 = -↑(2 * n + 1 - 1)
⊢ (-1) ^ (2 * n + 1 + 1) * (↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n + 1 - 1) + Nat.fib (2 * n + 1))) =
    (-1) ^ (2 * n + 1 - 1 + 1) * ↑(Nat.fib (2 * n + 1 - 1))

Tactic:
pow_add

Goal state after:
case inr
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : -↑(2 * n + 1) + 1 = -↑(2 * n + 1 - 1)
⊢ (-1) ^ (2 * n + 1) * (-1) ^ 1 * (↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n + 1 - 1) + Nat.fib (2 * n + 1))) =
    (-1) ^ (2 * n + 1 - 1 + 1) * ↑(Nat.fib (2 * n + 1 - 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun n ↦ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop
    (𝓝 (logDeriv (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) x))

Tactic:
refine logDeriv_tendsto isOpen_compl_range_intCast hx
      HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_
  · filter_upwards with n using by fun_prop
  · simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or]
    exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr.inl
m n : ℕ
⊢ fib (-↑m + ↑n) = fib (-↑m - 1) * fib ↑n + fib (-↑m) * fib (↑n + 1)

pp: case inr.inr
m n : ℕ
⊢ fib (-↑m + -↑n) = fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1)

Tactic:
· exact fib_add_natCast _ _

Goal state after:
case inr.inr
m n : ℕ
⊢ fib (-↑m + -↑n) = fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1)
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ ↑((fib ↑m).gcd (fib n)) = fib ↑m

Tactic:
gcd_fib,

Goal state after:
m : ℕ
n : ℤ
h : ↑m ∣ n
⊢ ↑(Nat.fib ((↑m).gcd n)) = fib ↑m
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ Irrational ψ

Tactic:
by
  have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
  have := this.ratCast_sub 1
  convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
  simp
  ring

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ IsCoseparator G ↔ (preadditiveYoneda.obj G).Faithful

Tactic:
isCoseparator_iff_faithful_yoneda_obj,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (yoneda.obj G).Faithful ↔ (preadditiveYoneda.obj G).Faithful
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
s : Discrete α
⊢ ((Discrete.functor fun s ↦ Pi.eval I s ⋙ G s) ⋙
          (whiskeringRight ((i : α) → I i) C (Ind C)).obj Ind.yoneda ⋙ colim).obj
      s ≅
    F.obj s

Tactic:
refine (Functor.Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda)) ≪≫ ?_

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
s : Discrete α
⊢ colimit (G s.as ⋙ Ind.yoneda) ≅ F.obj s
Module: Mathlib.CategoryTheory.Abelian.Preradical.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
Φ : Preradical C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : D ⥤ C
⊢ Mono (F.whiskerLeft Φ.ι)

Tactic:
rw [NatTrans.mono_iff_mono_app]
  intro
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: case refine_1
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
x✝ : (sq₁.map uliftFunctor.{max u v, v}).X₁
⊢ ((ConcreteCategory.hom
            ((sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫ ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom)).toFun
        x✝).down =
    ((ConcreteCategory.hom
            (((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₂)).toFun
        x✝).down

Tactic:
simpa [types_comp, uliftFunctor_map] using congrFun comm₁₂ _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h

Tactic:
refine ⟨pullback q p', pullback.fst _ _ ≫ p, pullback.snd _ _ ≫ q',
    epi_comp _ _, epi_comp _ _, ?_⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
x✝¹ : PseudoEqual P f g
x✝ : PseudoEqual P g h
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst q p' ≫ p) ≫ f.hom = (pullback.snd q p' ≫ q') ≫ h.hom
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 : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
      (J.isoRightDerivedObj F n).inv

Tactic:
by
  rw [← cancel_mono (J.isoRightDerivedObj F n).hom, assoc, assoc,
    InjectiveResolution.isoRightDerivedObj_hom_naturality f I J φ comm F n,
    Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
this : P.epiModSerre 0
⊢ P (Abelian.image f)

Tactic:
epiModSerre_zero_iff

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
X' : C
s : X' ⟶ X
hs : P.epiModSerre s
eq : s ≫ f = 0
this : P (Abelian.image f)
⊢ P (Abelian.image f)
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 : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
⊢ MorphismProperty.monomorphisms D (L.map f')

Tactic:
simpa using inferInstanceAs (Mono (L.map f'))

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ (F.map f ⊗ₘ inv (F.map f)ᘁ)

Tactic:
← id_tensor_comp_tensor_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ (𝟙 (F.obj X) ⊗ₘ inv (F.map f)ᘁ) ≫ (F.map f ⊗ₘ 𝟙 (F.obj Y)ᘁ)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (inv (F.map f)ᘁ ⊗ₘ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ

Tactic:
← id_tensor_comp_tensor_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ ((𝟙 (F.obj X)ᘁ ⊗ₘ F.map f) ≫ (inv (F.map f)ᘁ ⊗ₘ 𝟙 (F.obj Y))) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing X (G.obj (F.obj X)ᘁ)

Tactic:
letI := exactPairingCongrRight (X := F.obj X) (Y := F.obj (G.obj (F.obj X)ᘁ))
      (Y' := (F.obj X)ᘁ) (adj.toEquivalence.counitIso.app (F.obj X)ᘁ)
    apply ExactPairing.ofFullyFaithful F

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      η_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj Y)
        (F.obj Y) =
    η_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj X)
        (F.obj X) ≫
      ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ } ⊗ F).map f

Tactic:
by
            simp [tensorHom_def, coevaluation_comp_leftAdjointMate_assoc]

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

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = T.η.app (beckAlgebraCofork X).pt.1 ≫ ((beckAlgebraCofork X).π ≫ m).f

Tactic:
apply (X.unit_assoc _).symm

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

Goal state before:
pp: 𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f g : a ⟶ b
hfg : f = g
⊢ f.base = g.base

Tactic:
rw [hfg]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
u : b ⟶ a
t : LeftLift u (𝟙 a)
H : t.IsKan
H' : (t.whisker u).IsKan
ε : u ≫ t.lift ⟶ 𝟙 b := ⋯
Hε : rightZigzag t.unit ε = (ρ_ u).hom ≫ (λ_ u).inv
⊢ t.unit ≫ ((λ_ t.lift).inv ≫ leftZigzag t.unit ε) ▷ u =
    t.unit ≫ ((λ_ t.lift).inv ≫ (λ_ t.lift).hom ≫ (ρ_ t.lift).inv) ▷ u

Tactic:
calc _
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ leftZigzag t.unit ε ▷ u ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ (_ ◁ t.unit ≫ t.unit ▷ _) ⊗≫ t.lift ◁ ε ▷ u ⊗≫ 𝟙 _ := by
          rw [leftZigzag]; bicategory
        _ = 𝟙 _ ⊗≫ t.unit ⊗≫ t.lift ◁ (u ◁ t.unit ⊗≫ ε ▷ u) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]; bicategory
        _ = _ := by
          rw [← rightZigzag, Hε]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Limit

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Cat
X Y : limit (F ⋙ objects)
x✝¹ x✝ Z : J
f : x✝¹ ⟶ x✝
g : x✝ ⟶ Z
⊢ (↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map (f ≫ g)).toFunctor.map g_1 ≫ eqToHom ⋯) =
    (↾fun g ↦ eqToHom ⋯ ≫ (F.map f).toFunctor.map g ≫ eqToHom ⋯) ≫
      ↾fun g_1 ↦ eqToHom ⋯ ≫ (F.map g).toFunctor.map g_1 ≫ eqToHom ⋯

Tactic:
by
    ext h
    let : Category (objects.obj (F.obj Z)) := (inferInstance : Category (F.obj Z))
    simp [Functor.congr_hom congr($(F.map_comp f g).toFunctor) h, eqToHom_map]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Prod

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₃
D₂ : Type u₄
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
inst✝³ : Category.{v₃, u₃} D₁
inst✝² : Category.{v₄, u₄} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : Type u₅
inst✝¹ : Category.{v₅, u₅} E
F : C₁ × C₂ ⥤ E
inst✝ : W₂.ContainsIdentities
hF : (W₁.prod W₂).IsInvertedBy F
x✝¹ x✝ : C₁
f₁ : x✝¹ ⟶ x✝
hf₁ : W₁ f₁
⊢ IsIso ((curry.obj F).map f₁)

Tactic:
by
    have : ∀ (X₂ : C₂), IsIso (((curry.obj F).map f₁).app X₂) :=
      fun X₂ => hF _ ⟨hf₁, MorphismProperty.id_mem _ _⟩
    apply NatIso.isIso_of_isIso_app

Goal state after:
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
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ φ₁' = φ₂'

Tactic:
apply (adj.homEquiv U _).symm.injective

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst✝ : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := ⋯
U : Over Z := ⋯
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := ⋯
⊢ (adj.homEquiv U (Over.mk f)).symm φ₁' = (adj.homEquiv U (Over.mk f)).symm φ₂'
Module: Mathlib.CategoryTheory.DinatTrans

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ C ⥤ D
δ : F ⤞ G
α : G ⟶ H
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ (F.map f.op).app X✝ ≫ (δ.app X✝ ≫ (α.app (op X✝)).app X✝) ≫ (H.obj (op X✝)).map f =
    (F.obj (op Y✝)).map f ≫ (δ.app Y✝ ≫ (α.app (op Y✝)).app Y✝) ≫ (H.map f.op).app Y✝

Tactic:
rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app,
      ← δ.dinaturality_assoc f, NatTrans.naturality]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Q X Y Z : LocalizedMonoidal L W ε
f : Q ⟶ X
g : Y ⟶ Z
⊢ Q ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g

Tactic:
by
  simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.EffectiveEpi.Coproduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
c : Cofan X
hc : IsColimit c
π : (a : α) → X a ⟶ B
inst✝ : EffectiveEpiFamily X π
W✝ : C
e : c.pt ⟶ W✝
x✝¹ : ∀ {Z : C} (g₁ g₂ : Z ⟶ c.pt), g₁ ≫ hc.desc (Cofan.mk B π) = g₂ ≫ hc.desc (Cofan.mk B π) → g₁ ≫ e = g₂ ≫ e
m : (Cofan.mk B π).pt ⟶ W✝
hm : hc.desc (Cofan.mk B π) ≫ m = e
x✝ : α
⊢ π x✝ ≫ m = c.ι.app { as := x✝ } ≫ e

Tactic:
simp [← hm]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (adj.homEquiv A₁.a A₁.a) A₁.str ≫ G.map f.f = f.f ≫ (adj.homEquiv A₂.a A₂.a) A₂.str

Tactic:
← Adjunction.homEquiv_naturality_right,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ C
adj : F ⊣ G
A₁ A₂ : Algebra F
f : A₁ ⟶ A₂
⊢ (adj.homEquiv A₁.a A₂.a) (A₁.str ≫ f.f) = f.f ≫ (adj.homEquiv A₂.a A₂.a) A₂.str
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.IsCartesian f φ
⊢ IsCartesian.map p f φ φ = 𝟙 a

Tactic:
subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [id_comp]

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 φ
⊢ map p f φ ⋯ φ = 𝟙 a

Tactic:
subst_hom_lift p f φ; symm
  apply map_uniq
  simp only [id_comp]

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 : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
⊢ IsIso φ

Tactic:
let φ' := map p (p.map φ) φ (IsIso.inv_hom_id (p.map φ)).symm (𝟙 b)

Goal state after:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
inst✝¹ : p.IsStronglyCartesian (p.map φ) φ
inst✝ : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)
⊢ IsIso φ
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
· rintro ⟨c, f⟩ ⟨d, g⟩ ⟨u, x⟩ ⟨v, y⟩
    refine ⟨⟨coeq u v, coeq (eqToHom ?_ ≫
        (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y)⟩,
          ⟨coeqHom u v, coeqHom _ _⟩, ?_⟩
    · conv_rhs => rw [← Cat.Hom.comp_obj, ← F.map_comp, coeq_condition, F.map_comp,
        Cat.Hom.comp_obj]
    · set_option backward.isDefEq.respectTransparency.types false in
      apply Grothendieck.ext _ _ (coeq_condition u v)
      refine Eq.trans ?_ (eqToHom _ ≫= coeq_condition _ _)
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D₁
inst✝² : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝¹ : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝ : (F' ⋙ G').IsRightDerivedFunctor (whiskerRight β G' ≫ (L₂.associator F' G').hom) W₂
X₂ : C₂
⊢ G'.map (β.app X₂) ≫ (adj.derivedε W₂ α β).app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
simpa using! ((F' ⋙ G').rightDerived_fac_app
    (whiskerRight β G' ≫ (Functor.associator _ _ _).hom) W₂ _
    ((Functor.associator _ _ _).hom ≫ whiskerLeft F α ≫ (Functor.associator _ _ _).inv ≫
      whiskerRight adj.counit _ ≫ L₂.leftUnitor.hom ≫ L₂.rightUnitor.inv)) X₂

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
⊢ Function.Surjective (autMap f)

Tactic:
intro σ

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
A B : C
inst✝¹ : IsGalois A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut B
⊢ ∃ a, autMap f a = σ
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ Function.Injective ⇑(autEmbedding F)

Tactic:
intro σ

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ : Aut F
⊢ ∀ ⦃a₂ : Aut F⦄, (autEmbedding F) σ = (autEmbedding F) a₂ → σ = a₂
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
X : C
x : (F.obj X).obj
⊢ (ConcreteCategory.hom (σ.hom.app X)) x = (ConcreteCategory.hom (τ.hom.app X)) x

Tactic:
have : σ.app X = τ.app X := congr_fun h X

Goal state after:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
σ τ : Aut F
h : (autEmbedding F) σ = (autEmbedding F) τ
X : C
x : (F.obj X).obj
this : Iso.app σ X = Iso.app τ X
⊢ (ConcreteCategory.hom (σ.hom.app X)) x = (ConcreteCategory.hom (τ.hom.app X)) x
Module: Mathlib.CategoryTheory.Galois.Decomposition

Goal state before:
pp: case h.right
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x : (F.obj X).obj
⊢ ∃ a_1, (fun f ↦ (ConcreteCategory.hom (F.map f)) a) a_1 = x

Tactic:
use u ≫ Pi.π _ x

Goal state after:
case h
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
u : A ⟶ selfProd F X
a : (F.obj A).obj
h1 : (ConcreteCategory.hom (F.map u)) a = mkSelfProdFib F X
h2 : IsConnected A
h3 : Mono u
x : (F.obj X).obj
⊢ (fun f ↦ (ConcreteCategory.hom (F.map f)) a) (u ≫ Pi.π (fun x ↦ X) x) = x