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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (a b : ℤ_[p]), a ∈ nonunits ℤ_[p] → b ∈ nonunits ℤ_[p] → a + b ∈ nonunits ℤ_[p]

Tactic:
simp only [mem_nonunits]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ ∀ (a b : ℤ_[p]), ‖a‖ < 1 → ‖b‖ < 1 → ‖a + b‖ < 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
apply stationaryPoint_spec hf
  · apply le_trans
    · apply le_max_right v2
    · apply le_max_right
  · exact le_rfl

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

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

pp: case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

pp: case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

Tactic:
lift_index_left hf,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (max (stationaryPoint hfg) (max ?v2 ?v3✝))) =
    padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) * padicNorm p (↑g (stationaryPoint ⋯))

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
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
⊢ padicNorm p (↑(f + g) (max (stationaryPoint hfg) (max ?v2 ?v3))) ≤
    max (padicNorm p (↑f (stationaryPoint hf))) (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
⊢ ℕ

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

Tactic:
lift_index_left hf,

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

case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ

case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝¹ : (f + g - 0).LimZero
this✝ : f ≈ -g
this : f.norm = (-g).norm
⊢ f.norm = g.norm

Tactic:
simpa only [norm_neg] using this

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))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))

Tactic:
lift_index_left hf,

Goal state after:
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))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))

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))
⊢ ℕ

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))
⊢ ℕ
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst✝ : F.Full
⊢ F.map (hf.lift i h hi) ≫ hf.fst g = i

Tactic:
by
  simpa [lift] using! PullbackCone.IsLimit.lift_fst _ _ _ _

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
P : MorphismProperty C
inst✝⁴ : F.Faithful
inst✝³ : F.Full
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
⊢ ∀ ⦃a_1 : C⦄ (g : F.obj a_1 ⟶ F.obj b), ∃ b_1 fst snd, ∃ (_ : IsPullback fst (F.map snd) (F.map f) g), P snd

Tactic:
intro Y' g

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
P : MorphismProperty C
inst✝⁴ : F.Faithful
inst✝³ : F.Full
inst✝² : HasPullbacks C
inst✝¹ : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst✝ : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
Y' : C
g : F.obj Y' ⟶ F.obj b
⊢ ∃ b_1 fst snd, ∃ (_ : IsPullback fst (F.map snd) (F.map f) g), P snd
Module: Mathlib.AlgebraicTopology.DoldKan.Compatibility

Goal state before:
pp: A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{v_1, u_1} A
inst✝² : Category.{v_2, u_2} A'
inst✝¹ : Category.{v_3, u_3} B
inst✝ : Category.{v_4, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso = equivalenceCounitIso η

Tactic:
by
  ext1; apply NatTrans.ext; ext Y
  dsimp [equivalence]
  simp only [comp_id, id_comp, Functor.map_comp, equivalence₂CounitIso_eq,
    equivalence₂CounitIso_hom_app, assoc, equivalenceCounitIso_hom_app]
  simp only [equivalence₂_inverse, comp_obj, ← τ₀_hom_app, hη, τ₁_hom_app, ←
    eB.inverse.map_comp_assoc]
  rw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]
  congr 2
  simp only [← e'.functor.map_comp_assoc]
  simp only [Functor.comp_map, Equivalence.fun_inv_map, comp_obj, id_obj, map_comp, assoc]
  simp only [← e'.functor.map_comp_assoc]
  simp only [Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app, comp_obj, comp_id,
    Equivalence.functor_unit_comp, map_id, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = K[X].X m

Tactic:
congr

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : c.Rel m n
⊢ X _⦋n + 1⦌ = K[X].X m

Tactic:
congr

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (nullHomotopicMap' fun i j hij ↦ ((alternatingFaceMapComplex C).map f).f i ≫ hσ' q i j hij) =
    nullHomotopicMap' fun i j hij ↦ hσ' q i j hij ≫ ((alternatingFaceMapComplex C).map f).f j

Tactic:
congr

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (fun i j hij ↦ ((alternatingFaceMapComplex C).map f).f i ≫ hσ' q i j hij) = fun i j hij ↦
    hσ' q i j hij ≫ ((alternatingFaceMapComplex C).map f).f j
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij ↦ hσ' q i j hij).f n
h : ((whiskering C D).obj G ⋙ alternatingFaceMapComplex D).obj X =
  (alternatingFaceMapComplex C ⋙ G.mapHomologicalComplex (ComplexShape.down ℕ)).obj X :=
  Eq.symm (Functor.congr_obj (map_alternatingFaceMapComplex G) X)
⊢ (nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij ↦ hσ' q i j hij).f n

Tactic:
congr

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
| ∑ 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))

Tactic:
congr

Goal state after:
case a
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, ⋯⟩

case a
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) ^ ↑(Fin.cast ⋯ (Fin.castAdd q x)) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castAdd q x))
Module: Mathlib.AlgebraicTopology.DoldKan.Decomposition

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev +
      ∑ x ∈ {i | ↑i < q + 1}.erase q', (P ↑x).f (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev =
    -(P q).f (n + 1) ≫ (Hσ q).f (n + 1) + ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev

Tactic:
congr

Goal state after:
case neg.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ (P ↑q').f (n + 1) ≫ X.δ q'.rev.succ ≫ X.σ q'.rev = -(P q).f (n + 1) ≫ (Hσ q).f (n + 1)

case neg.e_a.e_s
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : (Q q).f (n + 1) = ∑ i with ↑i < q, (P ↑i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ i.rev
hqn : q ≤ n
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := ⟨q, ⋯⟩
⊢ {i | ↑i < q + 1}.erase q' = {i | ↑i < q}
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : Δ = Δ'
⊢ K.X Δ.len = K.X Δ'.len

Tactic:
congr

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

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

Tactic:
exact 0

Goal state after:
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 Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Termwise.mapMono K (image.ι (θ.unop ≫ A.e)) ≫ Sigma.ι (summand K Δ') (A.pull θ) =
    Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e)

Tactic:
congr

Goal state after:
case e_a
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ image.ι (θ.unop ≫ A.e) = i

case e_a.e_6
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ A.pull θ = Splitting.IndexSet.mk e
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
x : Fin (⦋0⦌.len + 1)
⊢ ∀ ⦃a₂ : Fin (⦋0⦌.len + 1)⦄, (SimplexCategory.Hom.toOrderHom θ) x = (SimplexCategory.Hom.toOrderHom θ) a₂ → x = a₂

Tactic:
y

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
x y : Fin (⦋0⦌.len + 1)
⊢ (SimplexCategory.Hom.toOrderHom θ) x = (SimplexCategory.Hom.toOrderHom θ) y → x = y
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case e_a.e_6
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Splitting.IndexSet.mk (factorThruImage (θ.unop ≫ A.e)) = Splitting.IndexSet.mk e

Tactic:
congr

Goal state after:
case e_a.e_6
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
K : ChainComplex C ℕ
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop A.fst
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ factorThruImage (θ.unop ≫ A.e) = e
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ x✝¹.f n ≫ (NormalizedMooreComplex.objX X n).arrow = x✝.f n ≫ (NormalizedMooreComplex.objX X n).arrow

Tactic:
exact HomologicalComplex.congr_hom hf n

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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : ¬B = A
⊢ s.N (unop B.fst).len ⟶ s.N (unop A.fst).len

Tactic:
exact 0

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.τ₀ = Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀

Tactic:
ext K : 3

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ Compatibility.τ₀.hom.app K = (Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀).hom.app K
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case neg.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
this : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ False

Tactic:
exact hj₁ (by simp only [Fin.ext_iff, Fin.val_zero]; lia)

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

Goal state before:
pp: V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝, map_id := map_id✝ }.map f))
⊢ { obj := F_obj, map := map✝¹, map_id := map_id✝¹ } = { obj := F_obj, map := map✝, map_id := map_id✝ }

Tactic:
congr

Goal state after:
V : Type u
inst✝¹ : ReflQuiver V
W : Type u₂
inst✝ : ReflQuiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : V), { obj := F_obj, map := map✝¹ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝¹ }.obj X)
map✝ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : V), { obj := F_obj, map := map✝ }.map (𝟙rq X) = 𝟙rq ({ obj := F_obj, map := map✝ }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.obj X = { obj := F_obj, map := map✝, map_id := map_id✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹ }.map f =
      Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := F_obj, map := map✝, map_id := map_id✝ }.map f))
⊢ map✝¹ = map✝
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₁ : C(X, Y)
toFun✝¹ : ↑I × X → Y
continuous_toFun✝¹ : Continuous toFun✝¹
map_zero_left✝¹ : ∀ (x : X), { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun (0, x) = f₀ x
map_one_left✝¹ : ∀ (x : X), { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹ }.toFun (1, x) = f₁ x
toFun✝ : ↑I × X → Y
continuous_toFun✝ : Continuous toFun✝
map_zero_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (0, x) = f₀ x
map_one_left✝ : ∀ (x : X), { toFun := toFun✝, continuous_toFun := continuous_toFun✝ }.toFun (1, x) = f₁ x
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_zero_left := map_zero_left✝¹,
        map_one_left := map_one_left✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
        map_one_left := map_one_left✝ }
⊢ { toFun := toFun✝¹, continuous_toFun := continuous_toFun✝¹, map_zero_left := map_zero_left✝¹,
      map_one_left := map_one_left✝¹ } =
    { toFun := toFun✝, continuous_toFun := continuous_toFun✝, map_zero_left := map_zero_left✝,
      map_one_left := map_one_left✝ }

Tactic:
congr

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

Goal state before:
pp: case h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
i : ι
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (Quotient.mk (Path.pi a✝)).map { toFun := fun p ↦ p i, continuous_toFun := ⋯ } = Quotient.mk (a✝ i)

Tactic:
congr

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

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

Tactic:
congr

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ Quotient.mk ((a✝.prod b✝).map ⋯) = Quotient.mk a✝

Tactic:
congr

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ Quotient.mk ((a✝.prod b✝).map ⋯) = Quotient.mk b✝

Tactic:
congr

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

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
a✝ : Path (a₁, b₁) (a₂, b₂)
⊢ prod (Quotient.mk (a✝.map ⋯)) (Quotient.mk (a✝.map ⋯)) = Quotient.mk a✝

Tactic:
congr

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

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ ≍ (π.map (TopCat.ofHom g)).map ⟦q⟧

Tactic:
exact heq_path_of_eq_image hfg

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ ⟦p₁⟧ = ⟦p₂⟧

Tactic:
congr

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ p₁ = p₂
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ { obj := fun x ↦ { as := (ContinuousMap.id X) x.as },
      map := fun {X_1 Y} p ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X), map_id := ⋯, map_comp := ⋯ } =
    𝟭 (FundamentalGroupoid X)

Tactic:
congr

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (fun {X_1 Y} p ↦ Path.Homotopic.Quotient.map p (ContinuousMap.id X)) = fun {X_1 Y} f ↦ f
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ { obj := fun x ↦ { as := (g.comp f) x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p (g.comp f),
      map_id := ⋯, map_comp := ⋯ } =
    { obj := fun x ↦ { as := f x.as }, map := fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
        map_comp := ⋯ } ⋙
      { obj := fun x ↦ { as := g x.as }, map := fun {X Y_1} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
        map_comp := ⋯ }

Tactic:
congr

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
Z : Type u_3
inst✝ : TopologicalSpace Z
g : C(Y, Z)
f : C(X, Y)
⊢ (fun {X_1 Y_1} p ↦ Path.Homotopic.Quotient.map p (g.comp f)) = fun {X_1 Y_1} f_1 ↦
    { obj := fun x ↦ { as := g x.as }, map := fun {X Y_2} p ↦ Path.Homotopic.Quotient.map p g, map_id := ⋯,
          map_comp := ⋯ }.map
      ({ obj := fun x ↦ { as := f x.as }, map := fun {X_2 Y_2} p ↦ Path.Homotopic.Quotient.map p f, map_id := ⋯,
            map_comp := ⋯ }.map
        f_1)