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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ max ‖z1‖ ‖z2‖

Tactic:
apply le_max_left

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖↑z‖ = ‖z‖

Tactic:
simp [norm_def]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ‖↑z‖ = ‖↑z‖

Tactic:
simp [norm_def]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inr
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p k = padicValNat p k + padicValNat p b - padicValNat p b

Tactic:
Nat.add_sub_cancel

Goal state after:
case inr
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p k = padicValNat p k
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑(p - 1)‖ = 1

Tactic:
simp [norm_def]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (p ^ n * q ^ m) = m

Tactic:
rw [mul_comm (p ^ n) (q ^ m)]

Goal state after:
p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : q ≠ p
⊢ padicValNat q (q ^ m * p ^ n) = m
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
zify

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hxy : x + y ≠ 0
⊢ min ↑x.valuation ↑y.valuation ≤ ↑(x + y).valuation
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
zify

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).valuation = ↑x.valuation + ↑y.valuation
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ (x ^ n).valuation = n * x.valuation

Tactic:
zify

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ ↑(x ^ n).valuation = ↑n * ↑x.valuation
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖z * w‖ ≤ ‖z‖
⊢ 1 ≤ ‖z‖

Tactic:
← eq,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
h : IsUnit z
w : ℤ_[p]
eq : 1 = z * w
this : ‖1‖ ≤ ‖z‖
⊢ 1 ≤ ‖z‖
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
apply le_max_left

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

Goal state before:
pp: 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
⊢ f.norm = g.norm

Tactic:
simp only [hg, hf, norm, dif_neg, not_false_iff]

Goal state after:
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
⊢ padicNorm p (↑f (stationaryPoint ⋯)) = padicNorm p (↑g (stationaryPoint ⋯))
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 : ℕ := ⋯
⊢ stationaryPoint ?hf ≤ i

Tactic:
apply le_max_left

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
⊢ ∃ i, (s i) default = X.hom x

Tactic:
have := Set.mem_univ (X.hom x)

Goal state after:
ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
this : X.hom x ∈ Set.univ
⊢ ∃ i, (s i) default = X.hom x
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ i ≥ N, padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ j ≥ N2, ∀ k ≥ N2, padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ max N N2 ≥ N

Tactic:
apply le_max_left

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i))) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ i,
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q i)) * (-1) ^ (a + 1)) •
          (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q i)) =
    -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩

Tactic:
simp only [assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a + q
hnaq_shift : ∀ (d : ℕ), n + d = a + d + q
⊢ ∑ x, ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x))) • φ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) ≫ X.σ ⟨a, ⋯⟩ +
      ∑ x,
        ((-1) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x)) * (-1) ^ (a + 1)) •
          φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x)) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ padicNorm p ↑k ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k

Tactic:
← padicNorm.dvd_iff_norm_le

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ↑(p ^ n) ∣ k ↔ ↑(p ^ n) ∣ k
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ≤ max ‖z1‖ ‖z2‖

Tactic:
apply le_max_left

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 x.valuation y.valuation ≤ (x + y).valuation

Tactic:
simpa only [hx, zero_add] using min_le_right _ _

Goal state after:
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
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq : Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌)
⊢ Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌) = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f

Tactic:
← eq,

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
h₁₄ :
  PInfty.f n =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p
eq : Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = (PInfty.f n).f ≫ Y.p.app (op ⦋n⦌)
⊢ Y.p.app (op ⦋n⦌) ≫ Y.p.app (op ⦋n⦌) ≫ (PInfty.f n).f = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ K.d Δ'.len Δ.len ≫ f.f Δ.len = f.f Δ'.len ≫ K'.d Δ'.len Δ.len

Tactic:
HomologicalComplex.Hom.comm

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ K.d Δ'.len Δ.len ≫ f.f Δ.len = K.d Δ'.len Δ.len ≫ f.f Δ.len
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
X✝ Y✝ Z✝ : Split C
Φ₁₂ : X✝.Hom Y✝
Φ₂₃ : Y✝.Hom Z✝
n : ℕ
⊢ X✝.s.ι n ≫ (Φ₁₂.F ≫ Φ₂₃.F).app (op ⦋n⦌) = (Φ₁₂.f n ≫ Φ₂₃.f n) ≫ Z✝.s.ι n

Tactic:
by
        dsimp
        simp only [assoc, Split.Hom.comm_assoc, Split.Hom.comm]

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

Goal state before:
pp: case zero
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ (inclusionOfMooreComplexMap X ≫ PInfty).f 0 = (inclusionOfMooreComplexMap X).f 0

Tactic:
dsimp
    simp only [comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : c.Rel i j
⊢ P.p.f i ≫ ((functor ⋙ inverse).obj P).X.d i j = ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).X.d i j ≫ P.p.f j

Tactic:
by
                dsimp
                simp only [HomologicalComplex.Hom.comm, HomologicalComplex.Hom.comm_assoc,
                  HomologicalComplex.p_idem]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ PInfty.f i ≫ K[X].d i j =
    (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ PInfty.f j

Tactic:
HomologicalComplex.Hom.comm

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ PInfty.f j =
    (s.cofan (op ⦋i⦌)).inj (IndexSet.id (op ⦋i⦌)) ≫ K[X].d i j ≫ PInfty.f j
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ (S₁.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
      ((alternatingFaceMapComplex C).obj S₁.X).d i j ≫
        ((alternatingFaceMapComplex C).map Φ.F).f j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    ((S₁.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
        K[S₁.X].d i j ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) ≫
      Φ.f j

Tactic:
simp only [assoc]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
⊢ (S₁.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
      ((alternatingFaceMapComplex C).obj S₁.X).d i j ≫
        ((alternatingFaceMapComplex C).map Φ.F).f j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋i⦌)).inj (Splitting.IndexSet.id (op ⦋i⦌)) ≫
      K[S₁.X].d i j ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X Y : TopPair
f g : X ⟶ Y
H : Homotopy f g
x : ↑TopPair.snd
t : ↑unitInterval
⊢ H.fst (t, (ConcreteCategory.hom map) x) = (ConcreteCategory.hom map) (H.snd (t, x))

Tactic:
have := w_apply H (x, I.homeomorph.symm t)

Goal state after:
X Y : TopPair
f g : X ⟶ Y
H : Homotopy f g
x : ↑TopPair.snd
t : ↑unitInterval
this :
  H.fst (I.homeomorph (x, I.homeomorph.symm t).2, (ConcreteCategory.hom map) (x, I.homeomorph.symm t).1) =
    (ConcreteCategory.hom map) (H.snd (I.homeomorph (x, I.homeomorph.symm t).2, (x, I.homeomorph.symm t).1))
⊢ H.fst (t, (ConcreteCategory.hom map) x) = (ConcreteCategory.hom map) (H.snd (t, x))
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
hx : 2⁻¹ < ↑x
⊢ p ⟨if ↑x ≤ 1 / 2 then ↑1 * 2 * ↑x else ↑1 * (2 - 2 * ↑x), ⋯⟩ =
    { toFun := (fun t ↦ if t ≤ 1 / 2 then p.extend (2 * t) else p.symm.extend (2 * t - 1)) ∘ Subtype.val,
        continuous_toFun := ⋯ }
      x

Tactic:
have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
      simpa [hx.not_ge, ← extend_apply]

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

Goal state before:
pp: case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ 2 * ↑t

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ 2 * ↑t ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case neg.left
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case neg.right
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case pos.left
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 0 ≤ 2 * ↑t

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case pos.right
t : ↑I
h✝ : ↑t ≤ 1 / 4
⊢ 2 * ↑t ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case pos.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ 0 ≤ ↑t + 1 / 4

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case pos.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ↑t ≤ 1 / 2
⊢ ↑t + 1 / 4 ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case neg.left
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 ≤ 1 / 2 * (↑t + 1)

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

Goal state before:
pp: case neg.right
t : ↑I
h✝¹ : ¬↑t ≤ 1 / 4
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 / 2 * (↑t + 1) ≤ 1

Tactic:
linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

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

Tactic:
rwa [← cofibrations_over_iff]

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

Goal state before:
pp: case mp.refine_1
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
i₁ i₂ : J.R
x₁ : d.right i₁
x₂ : d.right i₂
h : c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂

Tactic:
simp only [← descColimitType_ιColimitType_apply] at h

Goal state after:
case mp.refine_1
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
i₁ i₂ : J.R
x₁ : d.right i₁
x₂ : d.right i₂
h :
  d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁) =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂)
⊢ d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
⊢ ∀ (a b : X₁ ⊕ X₂),
    Rel f g a b →
      (match a with
        | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
        | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂) =
        match b with
        | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
        | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂

Tactic:
rintro _ _ ⟨t⟩

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
t : S
⊢ (match Sum.inl ((ConcreteCategory.hom f) t) with
    | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
    | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂) =
    match Sum.inr ((ConcreteCategory.hom g) t) with
    | Sum.inl x₁ => (ConcreteCategory.hom s.inl) x₁
    | Sum.inr x₂ => (ConcreteCategory.hom s.inr) x₂
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂)
h₁ : (hom (Sigma.ι X₁ i₁ ≫ Limits.Sigma.map f)) x₁ = (hom (f i₁ ≫ Sigma.ι X₂ i₁)) x₁
h₂ : (hom (Sigma.ι X₁ i₂ ≫ Limits.Sigma.map f)) x₂ = (hom (f i₂ ≫ Sigma.ι X₂ i₂)) x₂
⊢ (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)

Tactic:
simp only [comp_apply] at h₁ h₂ hx

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂)
h₁ : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₁)) x₁) = (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁)
h₂ : (hom (Limits.Sigma.map f)) ((hom (Sigma.ι X₁ i₂)) x₂) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)
⊢ (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ : X₄
⊢ ∀ ⦃a₂ : (fun X ↦ X) X₄⦄, (ConcreteCategory.hom k) x₃ = (ConcreteCategory.hom k) a₂ → x₃ = a₂

Tactic:
y₃

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ y₃ : X₄
⊢ (ConcreteCategory.hom k) x₃ = (ConcreteCategory.hom k) y₃ → x₃ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

Tactic:
by
    apply le_antisymm
    · rw [sup_le_iff]
      constructor
      · exact face_le_horn (1 : Fin 3) 2 (by simp)
      · exact face_le_horn (0 : Fin 3) 2 (by simp)
    · rw [horn_eq_iSup, iSup_le_iff]
      rintro i
      fin_cases i
      · exact le_sup_right
      · exact le_sup_left

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    Functor.LaxMonoidal.ε F ≫
      (ρ_ (F.obj (𝟙_ V))).inv ≫
        F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
          (F.map ((eHomEquiv V) f) ⊗ₘ F.map ((eHomEquiv V) g)) ≫
            Functor.LaxMonoidal.μ F (X✝ ⟶[V] Y✝) (Y✝ ⟶[V] Z✝) ≫ F.map (eComp V X✝ Y✝ Z✝)

Tactic:
Functor.LaxMonoidal.μ_natural_assoc,

Goal state after:
V : Type u'
inst✝⁶ : Category.{v', u'} V
inst✝⁵ : MonoidalCategory V
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : EnrichedOrdinaryCategory V C
W : Type u''
inst✝² : Category.{v'', u''} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Functor.LaxMonoidal.ε F ≫ F.map ((eHomEquiv V) (f ≫ g)) =
    Functor.LaxMonoidal.ε F ≫
      (ρ_ (F.obj (𝟙_ V))).inv ≫
        F.obj (𝟙_ V) ◁ Functor.LaxMonoidal.ε F ≫
          Functor.LaxMonoidal.μ F (𝟙_ V) (𝟙_ V) ≫ F.map ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) g) ≫ F.map (eComp V X✝ Y✝ Z✝)