mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
t : ↑Γ(M, V)
hs : (ConcreteCategory.hom (M.presheaf.map (homOfLE hf).op)) t = 0
n : ι → ℕ
hn : ∀ (i : ι), (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (f ^ n i • t) = 0
i : ι
⊢ basicOpen (g i) ≤ ⨆ i, basicOpen (g i)

Tactic:
exact le_iSup_of_le _ le_rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M✝ : ModuleCat ↑R
M : (Spec R).Modules
inst✝ : SheafOfModules.IsQuasicoherent M
ι : Type u
U : ι → (Spec R).Opens
pres : (i : ι) → SheafOfModules.Presentation (M.restrict (U i).ι)
hU : IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
s : Finset ι
hs : IsOpenCover fun i ↦ U ↑i
κ : ↥s → Type u
hκ : ∀ (i : ↥s), Finite (κ i)
a : (i : ↥s) → κ i → ↑R
ha : ∀ (i : ↥s), U ↑i = ⨆ k, PrimeSpectrum.basicOpen (a i k)
i : Sigma κ
⊢ PrimeSpectrum.basicOpen (a i.fst i.snd) ≤ ⨆ k, PrimeSpectrum.basicOpen (a i.fst k)

Tactic:
exact le_iSup_of_le _ le_rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf

Goal state before:
pp: C : Type u
A : Type u₁
K✝ : Type u₂
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} K✝
J : GrothendieckTopology C
inst✝¹ : HasSheafify J A
inst✝ : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A
K : Type u₂
⊢ ∀ [inst : Category.{v₂, u₂} K] [IsFiltered K], HasColimitsOfShape K (Sheaf J A)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf

Goal state before:
pp: C : Type u
A : Type u₁
K✝ : Type u₂
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} K✝
J : GrothendieckTopology C
inst✝³ : HasFiniteLimits A
inst✝² : HasSheafify J A
inst✝¹ : HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A
inst✝ : AB5OfSize.{v₂, u₂, v₁, u₁} A
K : Type u₂
x✝¹ : Category.{v₂, u₂} K
x✝ : IsFiltered K
⊢ HasExactColimitsOfShape K (Sheaf J A)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map a ≫ F.map g ≫ f = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀

Tactic:
h₂.fac

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map a ≫ F.map g ≫ f = F.map a ≫ F.map g ≫ f
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type u'
inst✝² : Category.{v', u'} J✝
inst✝¹ : HasFilteredColimitsOfSize.{v', u', v, u} C
inst✝ : AB5OfSize.{v', u', v, u} C
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
⊢ (monomorphisms C).IsStableUnderColimitsOfShape J

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app (op X')))
      (J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map f)) =
    (ConcreteCategory.hom (F.obj.map f.op)) x

Tactic:
rw [uliftYonedaEquiv_uliftYoneda_map]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj.obj (op X)
⊢ (ConcreteCategory.hom ((J.uliftYonedaEquiv.symm x).hom.app (op X'))) { down := f } =
    (ConcreteCategory.hom (F.obj.map f.op)) x
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Preorder J
inst✝ : OrderBot J
x✝ : J ⥤ C
⊢ HasLimit x✝

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Preorder J
inst✝ : OrderTop J
x✝ : J ⥤ C
⊢ HasColimit x✝

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    c.cofan₁.ι.app { as := i } ≫
      c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun x ↦
                match x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι }

Tactic:
by rw [IsColimit.fac]; exact c.hm i

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u'
inst✝⁷ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁶ : LinearOrder J
inst✝⁵ : SuccOrder J
inst✝⁴ : OrderBot J
inst✝³ : WellFoundedLT J
inst✝² : W.IsMultiplicative
inst✝¹ : W.RespectsIso
inst✝ : IsStableUnderFilteredColimits.{w, w, v, u} W
x✝⁴ : Type w
x✝³ : LinearOrder x✝⁴
x✝² : SuccOrder x✝⁴
x✝¹ : OrderBot x✝⁴
x✝ : WellFoundedLT x✝⁴
⊢ W.IsStableUnderColimitsOfShape x✝⁴

Tactic:
by infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f

Tactic:
exact ⟨_, _, _, _, _, hf⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
⊢ functorObjLeft f πX ≫ functorMapTgt f τ = functorMapSrc f τ ≫ functorObjLeft f πY

Tactic:
ext ⟨i, t, b, w⟩
  simp [ι_functorMapTgt f τ i t b w _ rfl, ι_functorMapSrc_assoc f τ i t b w _ rfl]

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

Goal state before:
pp: case mp.mp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ W f → ∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom

pp: case mp.mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ (∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom) → W f

Tactic:
· intro hf
      exact ⟨equivShrink _ ⟨f, hf⟩, by simp⟩

Goal state after:
case mp.mpr
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
a✝ : IsSmall.{w, v, u} W
A B : C
f : A ⟶ B
⊢ (∃ i, Arrow.mk f = Arrow.mk (↑((equivShrink ↑W.toSet).symm i)).hom) → W f
Module: Mathlib.CategoryTheory.Adjunction.Additive

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (G ⋙ preadditiveYoneda ⋙ (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).map f ≫
      (NatIso.ofComponents
          (fun X ↦
            (AddEquiv.ulift.trans ((adj.homAddEquiv (unop X) Y✝).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso)
          ⋯).hom =
    (NatIso.ofComponents
          (fun X ↦
            (AddEquiv.ulift.trans ((adj.homAddEquiv (unop X) X✝).symm.trans AddEquiv.ulift.symm)).toAddCommGrpIso)
          ⋯).hom ≫
      (preadditiveYoneda ⋙
            (whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op ⋙
              (whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj AddCommGrpCat.uliftFunctor).map
        f

Tactic:
ext _ ⟨x⟩
      exact AddEquiv.ulift.injective ((adj.homEquiv_naturality_right_symm x f))

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
hG : IsSeparator G
X : C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
by
  let κ := Order.succ (Cardinal.mk (Shrink.{w} (Subobject X)))
  have : Nonempty κ.ord.ToType := by simp [κ]
  have := WellFoundedLT.toOrderBot κ.ord.ToType
  exact ⟨κ.ord, top_mem_range hG A₀ (lt_of_lt_of_le (Order.lt_succ _) (by simp [κ]))⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case e'_5
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k : ↑(Set.Iic j)
hk : ¬IsMax k
⊢ transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀ =
    largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀)

Tactic:
Set.Iic.succ_eq_of_not_isMax hk,

Goal state after:
case e'_5
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k : ↑(Set.Iic j)
hk : ¬IsMax k
⊢ transfiniteIterate (largerSubobject hG) (↑⟨Order.succ ↑k, ⋯⟩) A₀ =
    largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case e'_6
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k : ↑(Set.Iic j)
hk : ¬IsMax k
e_5✝ :
  Subobject.underlying.obj (transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀) =
    Subobject.underlying.obj (largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀))
⊢ transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀ =
    largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀)

Tactic:
Set.Iic.succ_eq_of_not_isMax hk,

Goal state after:
case e'_6
C : Type u
inst✝⁶ : Category.{v, u} C
G : C
inst✝⁵ : Abelian C
hG : IsSeparator G
X : C
inst✝⁴ : IsGrothendieckAbelian.{w, v, u} C
A₀ : Subobject X
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
j : J
k : ↑(Set.Iic j)
hk : ¬IsMax k
e_5✝ :
  Subobject.underlying.obj (transfiniteIterate (largerSubobject hG) (↑(Order.succ k)) A₀) =
    Subobject.underlying.obj (largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀))
⊢ transfiniteIterate (largerSubobject hG) (↑⟨Order.succ ↑k, ⋯⟩) A₀ =
    largerSubobject hG (transfiniteIterate (largerSubobject hG) (↑k) A₀)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) x ≤ 1 ↔ ¬p ∣ x.den

Tactic:
nth_rw 1 [← x.num_div_den, map_div₀, ← Int.natCast_dvd_natCast, ← Int.padicValuation_eq_one_iff,
    Rat.padicValuation_cast, ← Int.cast_natCast, Rat.padicValuation_cast, div_le_one₀]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (Int.padicValuation p) x.num ≤ (Int.padicValuation p) ↑x.den ↔ (Int.padicValuation p) ↑x.den = 1

p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ 0 < (Int.padicValuation p) ↑x.den
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
rw [padicValNat.div_of_dvd <| factorial_mul_factorial_dvd_factorial h, Nat.mul_sub_left_distrib,
      padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _), Nat.mul_add]

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (k + n - ((p.digits n).sum + (p.digits k).sum)) - (p.digits (n + k)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
Nat.sub_sub,

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (k + n - ((p.digits n).sum + (p.digits k).sum) + (p.digits (n + k)).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ 0 + ((p.digits n).sum + (p.digits k).sum) - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum

Tactic:
zero_add,

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p.digits n).sum + (p.digits k).sum - (p.digits (k + n)).sum =
    (p.digits k).sum + (p.digits n).sum - (p.digits (k + n)).sum
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p : ℕ
a : ℤ
hp : p = 1
⊢ 1 ∣ a

Tactic:
exact one_dvd _

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝² : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → C ⥤ D i
inst✝¹ : HasEqualizers C
inst✝ : ∀ (i : I), PreservesLimitsOfShape WalkingParallelPair (F i)
hF : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [Mono f], (∀ (i : I), IsIso ((F i).map f)) → IsIso f
X Y : C
f g : X ⟶ Y
hfg : ∀ (i : I), (F i).map f = (F i).map g
i : I
⊢ IsIso ((F i).map (equalizer.ι f g))

Tactic:
by
        let hc := isLimitForkMapOfIsLimit (F i) _ (equalizerIsEqualizer f g)
        obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hc (𝟙 _) (by simpa using hfg i)
        exact ⟨l, Fork.IsLimit.hom_ext hc (by cat_disch), by cat_disch⟩

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case hb
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm ⋯ r

Tactic:
· induction r using Quotient.inductionOn; apply PadicSeq.norm_nonneg

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q (q + 1) = Q q - P q ≫ Hσ q

Tactic:
simp only [Q, P_succ, comp_add, comp_id]
  abel

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min ⊤ (if y = 0 then ⊤ else ↑y.valuation) ≤ if 0 + y = 0 then ⊤ else ↑(0 + y).valuation

Tactic:
min_eq_right,

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑y.valuation) ≤ if 0 + y = 0 then ⊤ else ↑(0 + y).valuation

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑y.valuation) ≤ ⊤
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

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
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ Epi (𝟙 (unop Δ))

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ A.fst = Δ

Tactic:
by
  constructor
  · intro h
    dsimp at h
    rw [h]
    rfl
  · intro h
    rcases A with ⟨_, ⟨f, hf⟩⟩
    simp only at h
    subst h
    refine ext _ _ rfl ?_
    simp only [eqToHom_refl, comp_id]
    exact eq_id_of_epi f

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')

Tactic:
by {rw [hu, hv]}

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun i ↦ ↑(f i)) j

Tactic:
simp [piIsoPi]
  rfl

Goal state after:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (F.trans G).symm (t, snd✝) = (G.symm.trans F.symm) (t, snd✝)

Tactic:
rw [trans_apply, symm_apply, trans_apply]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
⊢ (if h : ↑(σ (t, snd✝).1, (t, snd✝).2).1 ≤ 1 / 2 then
      F (⟨2 * ↑(σ (t, snd✝).1, (t, snd✝).2).1, ⋯⟩, (σ (t, snd✝).1, (t, snd✝).2).2)
    else G (⟨2 * ↑(σ (t, snd✝).1, (t, snd✝).2).1 - 1, ⋯⟩, (σ (t, snd✝).1, (t, snd✝).2).2)) =
    if h : ↑(t, snd✝).1 ≤ 1 / 2 then G.symm (⟨2 * ↑(t, snd✝).1, ⋯⟩, (t, snd✝).2)
    else F.symm (⟨2 * ↑(t, snd✝).1 - 1, ⋯⟩, (t, snd✝).2)
Module: Mathlib.Topology.Homotopy.Product

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i ↦ Quotient.mk (γ i)) = Quotient.mk (Path.pi γ)

Tactic:
by
  simp_rw [← Quotient.mk'_eq_mk, Quotient.mk', pi, Quotient.choice_eq, Quotient.map_mk]

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
Z : Type u_1
inst✝ : TopologicalSpace Z
p : Homotopic.Quotient x₀ x₁
f : C(X, Y)
g : C(Y, Z)
⊢ p.map (g.comp f) = (p.map f).map g

Tactic:
rcases p

Goal state after:
case mk
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x₀ x₁ : X
Z : Type u_1
inst✝ : TopologicalSpace Z
p : Homotopic.Quotient x₀ x₁
f : C(X, Y)
g : C(Y, Z)
a✝ : Path x₀ x₁
⊢ map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) (g.comp f) = (map (Quot.mk (⇑(Homotopic.setoid x₀ x₁)) a✝) f).map g
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
p : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
f : C(X, Y)
⊢ (p.cast hx hy).map f = (p.map f).cast ⋯ ⋯

Tactic:
rcases p

Goal state after:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
p : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
f : C(X, Y)
a✝ : Path x y
⊢ (cast (Quot.mk (⇑(Homotopic.setoid x y)) a✝) hx hy).map f = (map (Quot.mk (⇑(Homotopic.setoid x y)) a✝) f).cast ⋯ ⋯
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
⊢ sq.HasLift

Tactic:
have : WeakEquivalence (h.p ≫ pullback.snd p g) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_precomp _ _ _ h.hi.2 h₁

Goal state after:
C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
this : WeakEquivalence (h.p ≫ pullback.snd p g)
⊢ sq.HasLift
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊓ A₃.obj n = A₁.obj n

Tactic:
by
              rw [← sq.inf_eq]
              rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
S : Finset (Fin (n + 1 + 1))
hS : S.card = d + 1
hx : stdSimplex.face S ≤ A
hd : n < d
⊢ S = Finset.univ

Tactic:
rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
          exact le_antisymm (card_finset_fin_le S) (by lia)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.range (stdSimplex.map (SimplexCategory.δ i)) ≤ ∂Δ[n + 1]

Tactic:
by
    simp only [Subcomplex.range_eq_ofSimplex]
    refine le_trans ?_ (face_singleton_compl_le_boundary i)
    rw [stdSimplex.face_singleton_compl, yonedaEquiv_map]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
⊢ ∃ φ, (∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj) ∧ φ ≫ p = b

Tactic:
have sq : CommSq hf.desc Λ[n + 1, i].ι p b :=
    ⟨horn.hom_ext' (fun j hj ↦ by simpa using comm j hj)⟩
  exact ⟨sq.lift, fun j hj ↦ by simp [← ι_ι_assoc i j hj], by simp⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ Λ[2, 0] ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}

Tactic:
rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

Goal state after: