mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e : d.Extension val₀ j
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
⊢ (ConcreteCategory.hom (F.map (homOfLE hki).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val) =
    d.lift k hk
      ⟨fun x ↦
        match x with
        | op ⟨k_1, hk⟩ =>
          (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.map (homOfLE hij).op)) e.val),
        ⋯⟩

Tactic:
by
    rw [← comp_apply, ← map_comp, ← op_comp, homOfLE_comp,
      e.map_limit k hk (hki.trans hij)]
    congr
    ext ⟨l, hl⟩
    dsimp
    rw [← comp_apply, ← map_comp]
    rfl

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

Goal state before:
pp: case inl
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this : (e i hij').val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ (ConcreteCategory.hom (F.map (homOfLE hij).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩

Tactic:
d.map_lift _ _ _ _ hij'

Goal state after:
case inl
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this : (e i hij').val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (e i hij').val, ⋯⟩
⊢ ↑⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩ (op ⟨i, hij'⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift j hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: case inr
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
⊢ (ConcreteCategory.hom (F.map (𝟙 (op i)))) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩) =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩

Tactic:
rw [map_id, id_apply]

Goal state after:
case inr
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
⊢ d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩ =
    d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.lift i hj ⟨fun x ↦ (e ↑x.1 ⋯).val, ⋯⟩), ⋯⟩
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f g : Arrow C
φ : f ⟶ g
⊢ objMap I κ φ ≫ πObj I κ g.hom = πObj I κ f.hom ≫ Arrow.Hom.right φ

Tactic:
by
  let e₁ := asIso ((ιIteration I κ).app (Arrow.mk f.hom)).right
  let e₂ := asIso ((ιIteration I κ).app (Arrow.mk g.hom)).right
  change _ ≫ _ ≫ e₂.inv = (_ ≫ e₁.inv) ≫ _
  have h₁ := ((iteration I κ).map φ).w =≫ e₂.inv
  have h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right :=
    ((Functor.whiskerRight (ιIteration I κ) Arrow.rightFunc).naturality φ)
  dsimp at h₁
  rw [assoc] at h₁
  apply h₁.trans
  simp only [← cancel_mono e₂.hom, assoc, e₂.inv_hom_id, h₂, e₁.inv_hom_id_assoc]
  rw [← assoc]
  apply comp_id

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ (if ↑z = 0 then 0 else ↑p ^ (-padicValRat p ↑z)) ≤ 1

Tactic:
if_neg (mod_cast hz)

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ ↑p ^ (-padicValRat p ↑z) ≤ 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ^ (-x.valuation + x.valuation) = 1

pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ≠ 0 ∨ -x.valuation + -↑n ≠ 0 ∨ -x.valuation = 0 ∧ -↑n = 0

Tactic:
neg_add_cancel,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ^ 0 = 1

p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ≠ 0 ∨ -x.valuation + -↑n ≠ 0 ∨ -x.valuation = 0 ∧ -↑n = 0
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ^ 0 = 1

pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ≠ 0 ∨ -x.valuation + -↑n ≠ 0 ∨ -x.valuation = 0 ∧ -↑n = 0

Tactic:
zpow_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ 1 = 1

p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx✝ : ¬‖x‖ ≤ 1
n : ℕ := (-x.valuation).toNat
hn : n = (-x.valuation).toNat
hn_coe : ↑n = -x.valuation
a : ℚ_[p] := x * ↑p ^ n
ha : a = x * ↑p ^ n
hx : x ≠ 0
⊢ ↑p ≠ 0 ∨ -x.valuation + -↑n ≠ 0 ∨ -x.valuation = 0 ∧ -↑n = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
⊢ (f * g).norm = f.norm * g.norm

Tactic:
have hg : f * g ≈ 0 := mul_equiv_zero' _ hf

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
hg : f * g ≈ 0
⊢ (f * g).norm = f.norm * g.norm
Module: Mathlib.CategoryTheory.Limits.EpiMono

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ IsPushout f f (𝟙 Y) (𝟙 Y) → Epi f

Tactic:
intro hf
    exact (epi_iff_inl_eq_inr hf.isColimit).2 rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
this : Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U)) ∈ J U
V : C
g : unop (op V) ⟶ U
⊢ Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm g) ∈ J V

Tactic:
replace this := J.pullback_stable g this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝¹ : LocallySmall.{w, v, u} C
hP :
  ∀ ⦃X : C⦄ (S : Sieve X),
    (∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X),
        ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x) →
      S ∈ J X
F₁ : Cᵒᵖ ⥤ Type w
U : C
f : F₁ ⟶ shrinkYoneda.{w, v, u}.obj U
inst✝ : Mono f
hf : ∀ (Φ : P.FullSubcategory), Function.Surjective ⇑(ConcreteCategory.hom (Φ.obj.presheafFiber.map f))
V : C
g : unop (op V) ⟶ U
this : Sieve.pullback g (Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm (𝟙 U))) ∈ J (unop (op V))
⊢ Presheaf.imageSieve f (shrinkYonedaObjObjEquiv.symm g) ∈ J V
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s₀ : ↥S
X : S.Etale
y : ↥(Hom.fiber X.hom s₀)
t : ↥S
a : S.residueField t ⟶ CommRingCat.of Ω
hs₀ : ((SpecToEquivOfField Ω S).symm ⟨t, a⟩) default = s₀
⊢ t = s₀

Tactic:
simp [SpecToEquivOfField, ← hs₀]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
⊢ { toFun := Quotient.lift PadicSeq.norm ⋯, map_mul' := ⋯ } (Completion.mk q' - ↑(↑q' N)) < ε

Tactic:
convert_to! PadicSeq.norm (q' - const _ (q' N)) < ε

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
⊢ (q' - const (padicNorm p) (↑q' N)).norm < ε
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ (ConcreteCategory.hom
        ({ hom := yonedaEquiv.symm ((glueData hf).sheafValGluedMk (fun i ↦ yonedaEquiv (f i)) ⋯) }.hom.app (op (X i))))
      ((ConcreteCategory.hom (↾fun g ↦ g ≫ toGlued hf i)) (𝟙 (X i))) =
    (ConcreteCategory.hom ((f i).app (op (X i)))) (𝟙 (X i))

Tactic:
simpa using! GlueData.sheafValGluedMk_val _ _ _ _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
⊢ ∃ b, f ≈ const norm b

Tactic:
obtain ⟨q, hq⟩ := Padic.complete'' ⟨f, cau_seq_norm_e⟩

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
⊢ ∃ b, f ≈ const norm b
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)

Tactic:
induction x using Quotient.inductionOn with | _ f
   =>  _ 

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
⊢ ⟦f⟧ ≠ 0 → ‖⟦f⟧‖ = ↑p ^ (-valuation ⟦f⟧)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ⟦f⟧ ≠ 0
⊢ ¬f ≈ 0

Tactic:
apply CauSeq.not_limZero_of_not_congr_zero
    contrapose hf
    apply Quotient.sound
    simpa using hf

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

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:
have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ (x * y).valuation = x.valuation + y.valuation
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 : ChainComplex C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
by_cases h₄ : Isδ₀ i'
    · rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
    · simp only [mapMono_eq_zero K i' h₂ h₄, comp_zero]

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
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ s.πSummand A ≫ (s.cofan (op ⦋n⦌)).inj A ≫ PInfty.f n = 0

Tactic:
s.cofan_inj_comp_PInfty_eq_zero A hA,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ s.πSummand A ≫ 0 = 0
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
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
n : ℕ
⊢ Φ.f n ≫ (Y✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    (X✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n ≫ Φ.F.app (op ⦋n⦌)

Tactic:
← Split.cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋n⦌))

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
n : ℕ
⊢ (X✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ Φ.F.app (op ⦋n⦌) ≫ PInfty.f n =
    (X✝.s.cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n ≫ Φ.F.app (op ⦋n⦌)
Module: Mathlib.Topology.Homotopy.Equiv

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ ((↑h).comp ↑h.symm).Homotopic (ContinuousMap.id Y)

Tactic:
toContinuousMap_comp_symm

Goal state after:
X : Type u
Y : Type v
Z : Type w
Z' : Type x
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
h : X ≃ₜ Y
⊢ (ContinuousMap.id Y).Homotopic (ContinuousMap.id Y)
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₂
⊢ projLeft (prod (Quotient.mk a✝) (Quotient.mk b✝)) = Quotient.mk a✝

Tactic:
projLeft,

Goal state after:
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₂
⊢ (prod (Quotient.mk a✝) (Quotient.mk b✝)).map { toFun := Prod.fst, continuous_toFun := ⋯ } = Quotient.mk a✝
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))

Tactic:
set p₁ : Path ((0, 0) : I × I) (1, 1) := .prod (.trans (.refl _) .id) (.trans .id (.refl _))

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
F : f.Homotopy g
x₁ x₂ : X
p : Path x₁ x₂
G : C(↑I × ↑I, Y) := F.comp ((ContinuousMap.id ↑I).prodMap ↑p)
p₁ : Path (0, 0) (1, 1) := ((Path.refl 0).trans Path.id).prod (Path.id.trans (Path.refl 1))
⊢ ((p.map ⋯).trans (F.evalAt x₂)).Homotopic ((F.evalAt x₁).trans (p.map ⋯))
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : C
f : X ⟶ Y
⊢ WeakEquivalence (resolutionMap f) ↔ WeakEquivalence f

Tactic:
by
  rw [← weakEquivalence_postcomp_iff _ (pResolutionObj Y),
    HoCat.resolutionMap_fac, weakEquivalence_precomp_iff]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) ≫
      adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))) =
    𝟙 (bifibrantResolution.obj (toHoCat.obj (mk X)))

Tactic:
rw [comp_hom_eq_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) =
    inv (adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))))
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)) =
    𝟙 (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X))

Tactic:
rw [comp_hom_eq_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) =
    inv (BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)))
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
c : Multicofork I
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (I.fst default) (I.snd default)
⊢ c.π (J.fst default) ≫ hc.desc (isPushout.multicofork h h' s) = s.inl

Tactic:
simpa using! hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))

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

Goal state before:
pp: case a
X : SSet
n : ℕ
⊢ ∀ (i : Fin (n + 1)) (i_1 : ↑(X.nonDegenerate ↑i)),
    Subcomplex.ofSimplex ↑i_1 ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
rintro ⟨d, hd⟩ x

Goal state after:
case a
X : SSet
n d : ℕ
hd : d < n + 1
x : ↑(X.nonDegenerate ↑⟨d, hd⟩)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton n ⊔ ⨆ x, Subcomplex.ofSimplex ↑x
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₁ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
inst✝¹ : Mono r'
inst✝ : Mono k
h₂ : Set.range ⇑(ConcreteCategory.hom r) ⊔ Set.range ⇑(ConcreteCategory.hom b) = Set.univ
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) → (ConcreteCategory.hom b') x₃ = (ConcreteCategory.hom b') y₃ → x₃ = y₃
φ : pushout t l ⟶ X₄
hφ₁ : pushout.inl t l ≫ φ = r
hφ₂ : pushout.inr t l ≫ φ = b
this : Mono (φ ≫ k)
x₂ : X₂
⊢ ∃ a, (ConcreteCategory.hom φ) a = (ConcreteCategory.hom r) x₂

Tactic:
exact ⟨_, ConcreteCategory.congr_hom hφ₁ x₂⟩

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    sx.spineToDiagonal l ⋯ (f.interval j l hjl)

Tactic:
dsimp only [spineToDiagonal, Function.comp_apply]
  rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    ← tr_comp, diag_subinterval_eq]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 (homEquiv h) ≫ Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
iterate 4 rw [← CatEnriched.hComp_comp, id_eq_eqToHom, CatEnriched.eqToHom_hComp_eqToHom]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (CatEnriched.hComp (Hom.base θ) (Hom.base κ)) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ (λ_ (F.obj (X ⟶[V] Y))).inv ≫
      (ε F ≫ F.map (eId V X)) ▷ F.obj (X ⟶[V] Y) ≫ μ F (X ⟶[V] X) (X ⟶[V] Y) ≫ F.map (eComp V X X Y) =
    𝟙 (F.obj (X ⟶[V] Y))

Tactic:
simp only [comp_whiskerRight, Category.assoc, Functor.LaxMonoidal.μ_natural_left_assoc,
      Functor.LaxMonoidal.left_unitality_inv_assoc]

Goal state after:
V : Type v
inst✝⁵ : Category.{w, v} V
inst✝⁴ : MonoidalCategory V
C : Type u₁
inst✝³ : EnrichedCategory V C
W : Type v'
inst✝² : Category.{w', v'} W
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X Y : TransportEnrichment F C
⊢ F.map (λ_ (X ⟶[V] Y)).inv ≫ F.map (eId V X ▷ X ⟶[V] Y) ≫ F.map (eComp V X X Y) = 𝟙 (F.obj (X ⟶[V] Y))
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
⊢ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y
      ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map φ)) (𝟙 (Opposite.unop (Opposite.op X))))

Tactic:
have := HomObj.congr_app (ConcreteCategory.congr_hom (f.naturality φ) PUnit.unit) Y (𝟙 Y)

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
this :
  ((ConcreteCategory.hom ((𝟙_ (C ⥤ Type (max v' v u))).map φ ≫ f.app Y)) PUnit.unit).app Y (𝟙 Y) =
    ((ConcreteCategory.hom (f.app X ≫ (F.functorHom G).map φ)) PUnit.unit).app Y (𝟙 Y)
⊢ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y
      ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map φ)) (𝟙 (Opposite.unop (Opposite.op X))))