mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ max (↑p ^ (-padicValRat p q)) (↑p ^ (-padicValRat p r))

Tactic:
apply le_max_iff.2

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
h : padicValRat p q ≤ padicValRat p r
hnqp : padicNorm p q ≥ 0
hnrp : padicNorm p r ≥ 0
hq : ¬q = 0
hr : ¬r = 0
hqr : ¬q + r = 0
⊢ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p q) ∨ ↑p ^ (-padicValRat p (q + r)) ≤ ↑p ^ (-padicValRat p r)
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p ((p * m + n + 1) * (p * m + n)!) = padicValNat p (p * m)!

Tactic:
padicValNat.mul (succ_ne_zero (p * m + n)) <| factorial_ne_zero (p * m + _),

Goal state after:
case succ
p m : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n < p → padicValNat p (p * m + n)! = padicValNat p (p * m)!
h : n + 1 < p
⊢ padicValNat p (p * m + n).succ + padicValNat p (p * m + n)! = padicValNat p (p * m)!
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ max (stationaryPoint hf) v3 ≤ max v1 (max (stationaryPoint hf) v3)

Tactic:
· apply le_max_right

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

Goal state before:
pp: case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ max v2 (stationaryPoint hf) ≤ max v1 (max v2 (stationaryPoint hf))

Tactic:
· apply le_max_right

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

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint ?hf ≤ i

pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint ?hf ≤ stationaryPoint hg

pp: case hf
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ ¬g ≈ 0

Tactic:
· apply le_max_right

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := ⋯
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint hg ≤ stationaryPoint hg
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : S.Etale
R : Sieve X
hR : R ∈ S.smallEtaleTopology X
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj X
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f)) y = φ

Tactic:
cases X with | _ X f
    obtain ⟨φ : Spec (.of Ω) ⟶ X, rfl : φ ≫ f = s, rfl⟩ := Over.homMk_surjective φ
    obtain ⟨𝒰, h, _, le⟩ := (mem_smallGrothendieckTopology _ _).1 hR
    obtain ⟨i, y, hy⟩ := 𝒰.exists_eq (φ default)
    obtain ⟨l, hl₁, hl₂⟩ := exists_fac_of_etale_of_isSepClosed (𝒰.f i) φ _ hy
    have : 𝒰.f i ≫ f = 𝒰.X i ↘ S := HomIsOver.comp_over (f := 𝒰.f i) (S := S)
    exact ⟨(𝒰.X i).asOverProp S inferInstance,
      MorphismProperty.Over.homMk (𝒰.f i), le _ _ ⟨i⟩, Over.homMk l, by cat_disch⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))

pp: case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

pp: case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (max ?v1✝ (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

pp: case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

pp: case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ

Tactic:
· rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
        exact padicNorm.add_eq_max_of_ne hfgne

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

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ↑(PadicSeq.norm f) = ↑p ^ (-PadicSeq.valuation f)

Tactic:
rw [PadicSeq.norm_eq_zpow_neg_valuation]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ↑(↑p ^ (-PadicSeq.valuation f)) = ↑p ^ (-PadicSeq.valuation f)

case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ¬f ≈ 0
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
have h₄₃ : P₄.f n = P₃.f n := by
    have h := Functor.congr_obj (toKaroubi_comp_karoubiFunctorCategoryEmbedding _ _) Y₂
    simp only [P₃, P₄, ← natTransPInfty_f_app]
    congr 1

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : Karoubi (SimplicialObject C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y
Y₂ : SimplicialObject C := Y.X
Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)
P₁ : K[Y₁] ⟶ K[Y₁] := PInfty
P₂ : K[Y₂] ⟶ K[Y₂] := PInfty
P₃ : K[Y₃] ⟶ K[Y₃] := PInfty
P₄ : K[Y₄] ⟶ K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : ⟨Δ₁, ⟨α₁, hα₁⟩⟩.fst = ⟨Δ₂, ⟨α₂, hα₂⟩⟩.fst
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₂, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₂, ⟨α₂, hα₂⟩⟩

Tactic:
simp only at h₁

Goal state after:
Δ Δ₁ : SimplexCategoryᵒᵖ
α₁ : unop Δ ⟶ unop Δ₁
hα₁ : Epi α₁
Δ₂ : SimplexCategoryᵒᵖ
α₂ : unop Δ ⟶ unop Δ₂
hα₂ : Epi α₂
h₁ : Δ₁ = Δ₂
h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₂, ⟨α₂, hα₂⟩⟩
⊢ ⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₂, ⟨α₂, hα₂⟩⟩
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ PInfty.f (n + 1) ≫ { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun i ↦ g.app (op ⦋n⦌) ≫ f.b i }.a +
      ∑ i,
        (P ↑i).f (n + 1) ≫
          X'.δ i.rev.succ ≫ { a := g.app (op ⦋n + 1⦌) ≫ f.a, b := fun i ↦ g.app (op ⦋n⦌) ≫ f.b i }.b i.rev =
    g.app (op ⦋n + 1⦌) ≫ (PInfty.f (n + 1) ≫ f.a + ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev)

Tactic:
simp only [PInfty_f, comp_add]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z : C
f : MorphComponents X n Z
g : X' ⟶ X
⊢ (P (n + 1)).f (n + 1) ≫ g.app (op ⦋n + 1⦌) ≫ f.a +
      ∑ x, (P ↑x).f (n + 1) ≫ X'.δ x.rev.succ ≫ g.app (op ⦋n⦌) ≫ f.b x.rev =
    g.app (op ⦋n + 1⦌) ≫ (P (n + 1)).f (n + 1) ≫ f.a +
      g.app (op ⦋n + 1⦌) ≫ ∑ i, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ f.b i.rev
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
inst✝ : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ ((splitting K).cofan Δ).inj A ≫ (obj K).map θ =
    Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ ((splitting K).cofan Δ').inj (A.pull θ)

Tactic:
by
  apply Obj.map_on_summand
  apply image.fac

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso ((karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ F₂ ⋙ F₃ ⋙ F₄).map f)

Tactic:
← compatibility_N₂_N₁_karoubi,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
A✝ B✝ : Karoubi (SimplicialObject C)
f : A✝ ⟶ B✝
inst✝ : IsIso (N₂.map f)
F₁ : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ SimplexCategoryᵒᵖ ⥤ Karoubi C :=
  karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C
F₂ : SimplicialObject (Karoubi C) ⥤ Karoubi (ChainComplex (Karoubi C) ℕ) := N₁
F₃ : Karoubi (ChainComplex (Karoubi C) ℕ) ⥤ ChainComplex (Karoubi (Karoubi C)) ℕ :=
  (karoubiChainComplexEquivalence (Karoubi C) ℕ).functor
F₄ : HomologicalComplex (Karoubi (Karoubi C)) (ComplexShape.down ℕ) ⥤
  HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) :=
  (KaroubiKaroubi.equivalence C).inverse.mapHomologicalComplex (ComplexShape.down ℕ)
F : Karoubi (SimplexCategoryᵒᵖ ⥤ C) ⥤ HomologicalComplex (Karoubi C) (ComplexShape.down ℕ) := F₁ ⋙ F₂ ⋙ F₃ ⋙ F₄
⊢ IsIso ((N₂ ⋙ (karoubiChainComplexEquivalence C ℕ).functor).map f)
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
w : ∀ (j : J), m ≫ (piLimitFan F).proj j = s.proj j
j : J
⊢ m ⋙ Pi.eval (fun i ↦ ↑(F i)) j = (Functor.pi' fun j ↦ s.proj j) ⋙ Pi.eval (fun i ↦ ↑(F i)) j

Tactic:
specialize w j

Goal state after:
J : Type u
F : J → Grpd
s : Limits.Fan F
m : s.pt ⟶ (piLimitFan F).pt
j : J
w : m ≫ (piLimitFan F).proj j = s.proj j
⊢ m ⋙ Pi.eval (fun i ↦ ↑(F i)) j = (Functor.pi' fun j ↦ s.proj j) ⋙ Pi.eval (fun i ↦ ↑(F i)) j
Module: Mathlib.CategoryTheory.Groupoid.Grpd.Basic

Goal state before:
pp: ⊢ {J : Type u} → (f : J → Grpd) → Limits.Fan f

Tactic:
apply piLimitFan

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

Goal state before:
pp: case neg
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
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ¬↑t ≤ 1 / 2
⊢ G (⟨2 * (1 - ↑t) - 1, ⋯⟩, snd✝) = F (σ ⟨2 * ↑t - 1, ⋯⟩, snd✝)

Tactic:
exfalso
    linarith

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

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
S : Set X
F : f₀.HomotopyRel f₁ S
G : f₁.HomotopyRel f₂ S
t : ↑I
x : X
hx : x ∈ S
⊢ { toFun := fun x ↦ (F.trans G.toHomotopy).toFun (t, x), continuous_toFun := ⋯ } x = f₀ x

Tactic:
simp only [Homotopy.trans]
    split_ifs
    · simp [HomotopyWith.extendProp F (2 * t) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]
    · simp [HomotopyWith.extendProp G (2 * t - 1) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ piToPiTop X ≫ CategoryTheory.Functor.pi' (proj X) = 𝟙 (CategoryTheory.Grpd.of ((i : I) → ↑(π.obj (X i))))

Tactic:
change piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 _
    apply CategoryTheory.Functor.ext ?_ ?_
    · intros; rfl
    · intros; ext; simp

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y x' y' : X
hx : x' = x
hy : y' = y
γ : Homotopic.Quotient x y
⊢ γ.cast hx hy ≍ γ

Tactic:
by
  cases hx; cases hy; exact heq_of_eq γ.cast_rfl_rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: t : ↑I
⊢ transAssocReparamAux t ∈ I

Tactic:
by
  unfold transAssocReparamAux
  split_ifs <;> constructor <;> linarith [unitInterval.le_one t, unitInterval.nonneg t]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y : C
inst✝³ : IsCofibrant X
inst✝² : IsCofibrant Y
inst✝¹ : IsFibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : (toHoCat.obj (mk X)).as ⟶ (toHoCat.obj (mk Y)).as
h : HomRel.CompClosure (homRel C) x✝¹ x✝
⊢ RightHomotopyClass.mk x✝¹.hom = RightHomotopyClass.mk x✝.hom

Tactic:
simpa [RightHomotopyClass.mk_eq_mk_iff] using! h

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
X Y : Over S
f : X ⟶ Y
inst✝ : Fibration f
⊢ Fibration (Over.Hom.left f)

Tactic:
rwa [← fibrations_over_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
have (x : d.multispan.ColimitType) :
      ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (.right i) a = x := by
    obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x
    · exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z, by rw [ιColimitType_map]⟩
    · exact ⟨r, z, by simp⟩
  constructor
  · intro hc
    refine ⟨fun i₁ i₂ x₁ x₂ h ↦ ?_, ?_⟩
    · simp only [← descColimitType_ιColimitType_apply] at h
      exact hc.bijective.1 h
    · intro x
      obtain ⟨y, rfl⟩ := hc.bijective.2 x
      obtain ⟨i, z, rfl⟩ := this y
      exact ⟨i, z, by simp⟩
  · rintro ⟨h₁, h₂⟩
    refine ⟨fun x₁ x₂ h ↦ ?_, fun x ↦ ?_⟩
    · obtain ⟨i₁, a₁, rfl⟩ := this x₁
      obtain ⟨i₂, a₂, rfl⟩ := this x₂
      exact h₁ _ _ _ _ h
    · obtain ⟨i, y, rfl⟩ := h₂ x
      exact ⟨d.multispan.ιColimitType (.right i) y, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : X₂
⊢ (∃ s, x₁ = (ConcreteCategory.hom f) s ∧ x₂ = (ConcreteCategory.hom g) s) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)

Tactic:
rintro ⟨s, rfl, rfl⟩

Goal state after:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr ((ConcreteCategory.hom g) s))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ (∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)

Tactic:
rintro ⟨s, rfl, rfl⟩

Goal state after:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr ((ConcreteCategory.hom g) s))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case e'_3
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h : (ConcreteCategory.hom c.inl) x₁ = (ConcreteCategory.hom c.inr) x₂
⊢ (ConcreteCategory.hom c'.inr) x₂ = (ConcreteCategory.hom e.hom.hom) ((ConcreteCategory.hom c.inr) x₂)

Tactic:
exact ConcreteCategory.congr_hom (e.hom.w WalkingSpan.right).symm x₂

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

Goal state before:
pp: case «2»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
· dsimp
        simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 0 1 (by simp)).hom,
          ← Category.assoc]
        convert! h₂₃ <;> decide

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

Goal state before:
pp: case succ.refine_1
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (p.arrow 0) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ 0).op)) ↑(hn (p.interval 1 n ⋯))

Tactic:
rw [p.arrow_tgt 0]
      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0

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

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
⊢ ∀ {a b c d : CatEnriched C} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    hComp (𝟙 (f ≫ g)) η = (eqToIso ⋯).hom ≫ hComp (𝟙 f) (hComp (𝟙 g) η) ≫ (eqToIso ⋯).inv

Tactic:
by simp [← id_hComp_id, hComp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : (C ⥤ Type w)ᵒᵖ
f : A ⟶ A'
x : F.HomObj G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ F.map φ ≫ x.app Y ((ConcreteCategory.hom (f.unop.app Y)) ((ConcreteCategory.hom ((Opposite.unop A').map φ)) a)) =
    x.app X ((ConcreteCategory.hom (f.unop.app X)) a) ≫ G.map φ

Tactic:
rw [← HomObj.naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A A' : (C ⥤ Type w)ᵒᵖ
f : A ⟶ A'
x : F.HomObj G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ F.map φ ≫ x.app Y ((ConcreteCategory.hom (f.unop.app Y)) ((ConcreteCategory.hom ((Opposite.unop A').map φ)) a)) =
    F.map φ ≫ x.app Y ((ConcreteCategory.hom ((Opposite.unop A).map φ)) ((ConcreteCategory.hom (f.unop.app X)) a))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
motive : V.HomotopyCategory → Prop
h : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), motive (mk x)
x' : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ motive (mk x')

Tactic:
exact h x'

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case cast
n : ℕ
i : Fin (n + 1)
⊢ mk (n + 1) ⟶ mk n

Tactic:
exact σ i

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case last
n : ℕ
⊢ δ (Fin.last (n + 1)) ≫ σ (Fin.last n) = 𝟙 (mk n)

Tactic:
exact δ_comp_σ_succ

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case «0».«1»
⊢ δ ((fun i ↦ i) ⟨1, ⋯⟩) ≫ σ ((fun i ↦ i) ⟨0, ⋯⟩) = 𝟙 (mk 0)

Tactic:
exact δ_comp_σ_succ

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (toMk₁ i.castSucc)) (j.succAbove k) = 0 ↔ (ConcreteCategory.hom (toMk₁ i)) k = 0

Tactic:
toMk₁_apply_eq_zero_iff,

Goal state after:
n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.castSucc ↔ (ConcreteCategory.hom (toMk₁ i)) k = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (toMk₁ i.succ)) (j.succAbove k) = 0 ↔ (ConcreteCategory.hom (toMk₁ i)) k = 0

Tactic:
toMk₁_apply_eq_zero_iff,

Goal state after:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.succ ↔ (ConcreteCategory.hom (toMk₁ i)) k = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.castSucc)) k

Tactic:
· dsimp
    rw [toMk₁_of_le_castSucc, toMk₁_of_le_castSucc _ _ (by simpa)]
    by_cases hk' : k ≤ j.castSucc
    · rwa [Fin.predAbove_of_le_castSucc _ _ hk', Fin.castSucc_castPred]
    · grind [Fin.predAbove]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = (x.cast ⋯).simplex
⊢ x ≤ y

Tactic:
simp only [cast_simplex_rfl] at this

Goal state after:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this : (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index ⋯))) (y.cast ⋯).simplex = x.simplex
⊢ x ≤ y
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
⊢ WellFounded (P.ofIso e hA).AncestralRel

Tactic:
by
    have hP := P.wf
    rw [wellFounded_iff_isEmpty_descending_chain] at hP ⊢
    by_contra!
    obtain ⟨f, hf⟩ := this
    refine hP.false ⟨fun n ↦ ⟨_, (f n).2⟩, fun n ↦ ?_⟩
    simpa [← P.ofIso_ancestralRel_iff e hA] using hf n

Goal state after: