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

Goal state before:
pp: case degree_f_lt
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ n < (Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

Tactic:
Finset.card_image_of_injOn (strictAntiOn_node n).injOn,

Goal state after:
case degree_f_lt
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ n < (Finset.range (n + 1)).card
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case degree_g_lt
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ n < (Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

Tactic:
Finset.card_image_of_injOn (strictAntiOn_node n).injOn,

Goal state after:
case degree_g_lt
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ n < (Finset.range (n + 1)).card
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ∑ i ≤ n, eval (node n i) P * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ = P.coeff n

Tactic:
have : P.degree < (Finset.range (n + 1)).card := by
    rw [Finset.card_range]
    grw [hP]
    norm_cast
    simp

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
this : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n, eval (node n i) P * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ = P.coeff n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup

Tactic:
refine (Finset.range n).nodup_map_iff_injOn.mpr ?_

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) ↑(Finset.range n)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ L.sumInvPow 0 = L.G

Tactic:
ext; simp [sumInvPow, G]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
⊢ (Multiset.map (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Multiset.range n)).Nodup

Tactic:
refine (Finset.range n).nodup_map_iff_injOn.mpr ?_

Goal state after:
n : ℕ
⊢ Set.InjOn (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) ↑(Finset.range n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic

Goal state before:
pp: x : ℂ
a✝ : x ∈ Set.univ
⊢ cos x ≠ 0 ∨ sin x ≠ 0

Tactic:
grind [sin_sq_add_cos_sq]

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

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

Tactic:
dsimp
    rw [← Nat.cast_ofNat, ← Nat.cast_add, ← Nat.cast_add_one, fib_natCast, fib_natCast,
      Nat.fib_add_two, Nat.cast_add]

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin (↑π * x) ≠ 0

Tactic:
apply Complex.sin_ne_zero_iff.2

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ∀ (k : ℤ), ↑π * x ≠ ↑k * ↑π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
⊢ EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℂ_ℤ)
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) ℂ_ℤ

Tactic:
by
  apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen Complex.isOpen_compl_range_intCast)
  exact eqOn_iteratedDeriv_cotTerm ..

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ Summable fun n ↦ (x - (↑n + 1)) ^ (-1 - ↑k)

Tactic:
apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp
        (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by lia))).2).congr

Goal state after:
k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ ∀ (b : ℕ), ((↑1 * x + ↑(-↑(b + 1))) ^ (↑k + 1))⁻¹ = (x - (↑b + 1)) ^ (-1 - ↑k)
Module: Mathlib.CategoryTheory.Generator.Preadditive

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

Tactic:
by
  rw [isSeparator_iff_faithful_preadditiveCoyoneda, preadditiveCoyoneda_obj]
  exact ⟨fun h => Functor.Faithful.of_comp _ (forget₂ _ AddCommGrpCat.{v}),
    fun h => Functor.Faithful.comp _ _⟩

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hbc
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ ↑n * l - ε * (1 + l) * ↑n ≤ u n

Tactic:
linarith only [hn]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hab
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
ε : ℝ
hε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
npos : 0 < n
⊢ u n ≤ ↑n * l + ε * (1 + ε + l) * ↑n

Tactic:
linarith only [hn]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.IndObject

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow yoneda A) ↔ PreservesFiniteLimits A

Tactic:
by
    refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
    · apply preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda
    · exact isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits A
    · have := essentiallySmallSelf (CostructuredArrow yoneda A)
      apply finallySmall_of_essentiallySmall

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
this : (yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j) = i.hom.app (limit K) ≫ A.map (limit.π K j)
x✝ : Opposite.unop (limit K) ⟶ i.left
⊢ (ConcreteCategory.hom ((yoneda.obj i.left).map (limit.π K j) ≫ i.hom.app (K.obj j))).toFun x✝ =
    (ConcreteCategory.hom
          (((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
            (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
              ((coyoneda ⋙
                          (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj
                            (CostructuredArrow.proj yoneda A)).map
                      (limit.π K j)).app
                  i ≫
                ((functorToInterchangeIso A K).inv.app j).app i ≫
                  ((flipFunctorToInterchange A K).hom.app i).app j ≫
                    (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j)).toFun
      x✝

Tactic:
simp [flipFunctorToInterchange, functorToInterchangeIso, functorToInterchange]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ ExactAt I.cocomplex (n + 1)

Tactic:
rw [← quasiIsoAt_iff_exactAt I.ι (n + 1) (exactAt_succ_single_obj _ _)]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: case mpr.refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ Ψ : Preradical C
X : C
h : IsZero (Ψ.r.obj (Φ.quotient.obj X))
inv : (Φ.colon Ψ).r.obj X ⟶ (KernelFork.ofι (Φ.ι.app X) ⋯).pt
hinv : inv ≫ Φ.ι.app X = (Φ.colon Ψ).ι.app X
⊢ (Over.Hom.left (Φ.toColon Ψ).hom).app X ≫ inv = 𝟙 (Φ.obj.left.obj X)

Tactic:
simp [← cancel_mono (Φ.ι.app X), hinv]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map
      (InjectiveResolution.desc (𝟙 X) (injectiveResolution X) (injectiveResolution X)) =
    𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex)

Tactic:
rw [← (HomotopyCategory.quotient _ _).map_id]
    apply HomotopyCategory.eq_of_homotopy
    apply InjectiveResolution.descIdHomotopy

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 : ℕ
⊢ (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:
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.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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ rightDerived (𝟙 F) n = 𝟙 (F.rightDerived n)

Tactic:
dsimp only [rightDerived]

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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ Functor.whiskerRight (rightDerivedToHomotopyCategory (𝟙 F))
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (F.rightDerived n)
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
J : Type u_3
inst✝ : Category.{v_2, u_3} J
F : J ⥤ Action V G
c✝ : Cone F
h : IsLimit ((forget V G).mapCone c✝)
⊢ IsLimit ((functorCategoryEquivalence V G).functor.mapCone c✝)

Tactic:
exact evaluationJointlyReflectsLimits _ (fun _ => h)

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ { hom := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.hom, ⋯⟩, comm := ⋯ } = x✝

Tactic:
by ext; simp [ConcreteCategory.ofHom_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
⊢ { g // F.map (adj₁.unit.app (L.obj Y) ≫ U.map g) = g ≫ F.map (adj₁.unit.app X) } ≃
    { z // z ≫ U.map (F.map (adj₁.unit.app X)) = z ≫ adj₁.unit.app (U.obj (F.obj X)) }

Tactic:
apply (adj₁.homEquiv _ _).subtypeEquiv
      intro g
      rw [← (adj₁.homEquiv _ _).injective.eq_iff, adj₁.homEquiv_unit,
        adj₁.homEquiv_unit, adj₁.homEquiv_unit, eq_comm]
      simp

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s t✝ : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
⊢ ∀ (s : LeftExtension f g) (τ : t.ofCompId ⟶ s), τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
intro s τ

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : a ⟶ c
s✝ t✝ : LeftExtension f g
t : LeftExtension f (g ≫ 𝟙 c)
P : t.IsKan
s : LeftExtension f g
τ : t.ofCompId ⟶ s
⊢ τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t✝ : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
⊢ ∀ (s : LeftLift f g) (τ : t.ofIdComp ⟶ s), τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))

Tactic:
intro s τ

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : LeftLift f g
t : LeftLift f (𝟙 c ≫ g)
P : t.IsKan
s : LeftLift f g
τ : t.ofIdComp ⟶ s
⊢ τ = t.whiskerIdCancel (Limits.IsInitial.to P (s.whisker (𝟙 c)))
Module: Mathlib.CategoryTheory.Bicategory.Kan.IsKan

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t✝ : RightLift f g
t : RightLift f (𝟙 c ≫ g)
P : t.IsKan
⊢ ∀ (s : RightLift f g) (τ : s ⟶ t.ofIdComp), τ = t.whiskerIdCancel (Limits.IsTerminal.from P (s.whisker (𝟙 c)))

Tactic:
intro s τ

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s✝ t✝ : RightLift f g
t : RightLift f (𝟙 c ≫ g)
P : t.IsKan
s : RightLift f g
τ : s ⟶ t.ofIdComp
⊢ τ = t.whiskerIdCancel (Limits.IsTerminal.from P (s.whisker (𝟙 c)))
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
⊢ PFun.toSubtype (fun x ↦ x ≠ Z.point) (f ≫ g).toFun ∘ Subtype.val =
    PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val ≫
      PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val

Tactic:
refine PFun.ext fun ⟨a, ha⟩ ⟨c, hc⟩ =>
      (PFun.mem_toSubtype_iff.trans ?_).trans Part.mem_bind_iff.symm

Goal state after:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
⊢ ↑⟨c, hc⟩ = (f ≫ g).toFun ↑⟨a, ha⟩ ↔
    ∃ a_1 ∈ (PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val) ⟨a, ha⟩,
      ⟨c, hc⟩ ∈ (PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val) a_1
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β
x : α
⊢ x ∈ f.Dom ↔ ∃ y, y ∈ f x

Tactic:
by simp [Dom, Part.dom_iff_mem]

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
⊢ ∃ f, graphFunctor.map f.hom = r

Tactic:
obtain ⟨g, hg⟩ := Classical.axiomOfChoice (fun a => (h2 a a).mpr rfl)

Goal state after:
case mp
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
⊢ ∃ f, graphFunctor.map f.hom = r
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y Z : RelCat
⊢ unopFunctor.IsEquivalence

Tactic:
change opEquivalence.inverse.IsEquivalence

Goal state after:
X Y Z : RelCat
⊢ opEquivalence.inverse.IsEquivalence
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 φ
a' : 𝒳
φ' : a' ≅ a
inst✝ : p.IsHomLift (𝟙 R) φ'.hom
⊢ ∀ {a'_1 : 𝒳} (φ'_1 : a'_1 ⟶ b) [p.IsHomLift f φ'_1], ∃! χ, p.IsHomLift (𝟙 R) χ ∧ χ ≫ φ'.hom ≫ φ = φ'_1

Tactic:
by
    intro c ψ hψ
    use IsCartesian.map p f φ ψ ≫ φ'.inv
    refine ⟨⟨inferInstance, by simp⟩, ?_⟩
    rintro τ ⟨hτ₁, hτ₂⟩
    rw [Iso.eq_comp_inv]
    apply map_uniq
    simp only [assoc, hτ₂]

Goal state after:
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⟩

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ ∃ Z h, { base := u, fiber := x } ≫ h = { base := v, fiber := y } ≫ h
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
X Y : C
f g : X ⟶ Y
x : (F.obj X).obj
h : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x
⊢ (ConcreteCategory.hom (F.map (equalizer.ι f g))) ((fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x

Tactic:
simp only [fiberEqualizerEquiv, Functor.comp_map]
  change ((Types.equalizerIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g)) _ = _
  erw [PreservesEqualizer.iso_inv_ι, Types.equalizerIso_inv_comp_ι]
  rfl

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

Goal state before:
pp: case ind
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
⊢ ∀ (X : C), n = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
intro X hn

Goal state after:
case ind
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
n : ℕ
hi : ∀ m < n, ∀ (X : C), m = Nat.card (F.obj X).obj → ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
X : C
hn : n = Nat.card (F.obj X).obj
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι
Module: Mathlib.CategoryTheory.Galois.GaloisObjects

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
A B : C
inst✝¹ : IsConnected A
inst✝ : IsGalois B
f : A ⟶ B
σ : Aut A
a : (F.obj A).obj
⊢ (ConcreteCategory.hom (F.map (autMap f σ).hom)) ((ConcreteCategory.hom (F.map f)) a) =
    (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (F.map σ.hom)) a)

Tactic:
simpa [-comp_autMap] using ConcreteCategory.congr_hom (F.congr_map (comp_autMap f σ)) a

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X A : C
a : (F.obj A).obj
isGalois✝² : IsGalois A
B : C
b : (F.obj B).obj
isGalois✝¹ : IsGalois B
u : A ⟶ X
v : B ⟶ X
h : (ConcreteCategory.hom (F.map u)) a = (ConcreteCategory.hom (F.map v)) b
Z : C
z : (F.obj Z).obj
isGalois✝ : IsGalois Z
f :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).obj
hf :
  (ConcreteCategory.hom (F.map f)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := ⋯ })).pt
h✝ : True
g :
  (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).obj ⟶
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).obj
hg :
  (ConcreteCategory.hom (F.map g)) (Opposite.unop (Opposite.op { obj := Z, pt := z, isGalois := isGalois✝ })).pt =
    (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := ⋯ })).pt
⊢ (ConcreteCategory.hom (F.map (f ≫ u))) z = (ConcreteCategory.hom (F.map (g ≫ v))) z

Tactic:
rw [map_comp, FintypeCat.comp_apply, hf, map_comp, FintypeCat.comp_apply, hg, h]

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

Goal state before:
pp: case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
A : C
f : A ⟶ X
hgal : IsGalois A
hs : Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
x y : (F.obj X).obj
a : (F.obj A).obj
ha : (ConcreteCategory.hom (F.map f)) a = x
b : (F.obj A).obj
hb : (ConcreteCategory.hom (F.map f)) b = y
this : MulAction.IsPretransitive (Aut F) (F.obj A).obj
σ : Aut F
hσ : (ConcreteCategory.hom (σ.hom.app A)) a = b
⊢ (ConcreteCategory.hom (F.map f ≫ σ.hom.app X)) a = (ConcreteCategory.hom (F.map f)) b

Tactic:
rw [σ.hom.naturality, FintypeCat.comp_apply, hσ]

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

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
⊢ ∃ a, (toAut F G) a = t

Tactic:
choose gi hgi using (fun X : PointedGaloisObject F ↦ toAut_surjective_isGalois F G t X)

Goal state after:
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
⊢ ∃ a, (toAut F G) a = t
Module: Mathlib.CategoryTheory.Groupoid.FreeGroupoid

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ ∀ (x y : Paths (Symmetrify V)) (f₁ f₂ : x ⟶ y),
    redStep f₁ f₂ → (Paths.lift (Symmetrify.lift φ)).map f₁ = (Paths.lift (Symmetrify.lift φ)).map f₂

Tactic:
by
    rintro _ _ _ _ ⟨X, Y, f⟩
    -- Porting note: `simp` does not work, so manually `rewrite`
    erw [Paths.lift_nil, Paths.lift_cons, Quiver.Path.comp_nil, Paths.lift_toPath,
      Quiver.Symmetrify.lift_reverse]
    symm
    apply Groupoid.comp_inv

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Subgroupoid

Goal state before:
pp: C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ discrete.arrows c✝ c✝
⊢ Groupoid.inv f ≫ γ ≫ f ∈ discrete.arrows d✝ d✝

Tactic:
by
      cases hγ
      simp only [inv_eq_inv, Category.id_comp, IsIso.inv_hom_id]; constructor

Goal state after: