mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Goal state before:
pp: case exists_of_eq.succ
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := (awayMap 𝒜 hg ⋯).toAlgebra
hc :
  ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ m * (a * g ^ n)) =
    ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ n * (b * g ^ m))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b))

Tactic:
convert! congr(f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * $hc) using 1

Goal state after:
case e'_2
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := (awayMap 𝒜 hg ⋯).toAlgebra
hc :
  ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ m * (a * g ^ n)) =
    ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ n * (b * g ^ m))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ m * ((g ^ (d + 1)) ^ (k + m + n) * a)) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * (↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ m * (a * g ^ n)))

case e'_3
A : Type u_2
σ : Type u_3
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
n : ℕ
a : A
m : ℕ
b : A
k d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
ha : a ∈ 𝒜 (n • (d + 1))
hb : b ∈ 𝒜 (m • (d + 1))
this : Algebra (Away 𝒜 f) (Away 𝒜 (f * g)) := (awayMap 𝒜 hg ⋯).toAlgebra
hc :
  ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ m * (a * g ^ n)) =
    ↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ n * (b * g ^ m))
⊢ (fun x ↦ f ^ x) k * ((f ^ e) ^ (k + m + n) * f ^ n * ((g ^ (d + 1)) ^ (k + m + n) * b)) =
    f ^ (e * (k + m + n)) * g ^ (d * (k + m + n)) * (↑⟨(fun x ↦ (f * g) ^ x) k, ⋯⟩ * ((f * g) ^ n * (b * g ^ m)))
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
U : (Spec R).Opens
f : ↑R
hf : U ≤ PrimeSpectrum.basicOpen f
this :
  ⇑((algebraMap (↑R) (Module.End ↑R ↑Γ(M, U))) f) =
    ⇑((algebraMap (↑Γ(Spec R, U)) (Module.End ↑Γ(Spec R, U) ↑Γ(M, U)))
        ((ConcreteCategory.hom ((Spec R).presheaf.map (homOfLE hf).op))
          ((algebraMap ↑R ↑Γ(Spec R, PrimeSpectrum.basicOpen f)) f)))
⊢ IsUnit
    ((algebraMap (↑Γ(Spec R, U)) (Module.End ↑Γ(Spec R, U) ↑Γ(M, U)))
      ((ConcreteCategory.hom ((Spec R).presheaf.map (homOfLE hf).op))
        ((algebraMap ↑R ↑Γ(Spec R, PrimeSpectrum.basicOpen f)) f)))

Tactic:
exact ((IsLocalization.Away.algebraMap_isUnit _).map _).map _

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

Goal state before:
pp: R : CommRingCat
M : (Spec R).Modules
S : CommRingCat
f : R ⟶ S
inst✝ : IsOpenImmersion (Spec.map f)
U : (Spec S).Opens
r : ↑R
x : ↑Γ(M.restrict (Spec.map f), U)
⊢ (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom)
      ((ConcreteCategory.hom ((Spec S).presheaf.map (Opens.leTop U).op))
          ((ConcreteCategory.hom (ΓSpecIso S).inv) ((ConcreteCategory.hom f) r)) •
        x) =
    (ConcreteCategory.hom ((Spec R).presheaf.map (Opens.leTop (Spec.map f ''ᵁ U)).op))
        ((ConcreteCategory.hom (ΓSpecIso R).inv) r) •
      (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom) x

Tactic:
smul_restrictAppIso_hom_apply,

Goal state after:
R : CommRingCat
M : (Spec R).Modules
S : CommRingCat
f : R ⟶ S
inst✝ : IsOpenImmersion (Spec.map f)
U : (Spec S).Opens
r : ↑R
x : ↑Γ(M.restrict (Spec.map f), U)
⊢ (ConcreteCategory.hom (Hom.appIso (Spec.map f) U).inv)
        ((ConcreteCategory.hom ((Spec S).presheaf.map (Opens.leTop U).op))
          ((ConcreteCategory.hom (ΓSpecIso S).inv) ((ConcreteCategory.hom f) r))) •
      (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom) x =
    (ConcreteCategory.hom ((Spec R).presheaf.map (Opens.leTop (Spec.map f ''ᵁ U)).op))
        ((ConcreteCategory.hom (ΓSpecIso R).inv) r) •
      (ConcreteCategory.hom (restrictAppIso (Spec.map f) M U).hom) x
Module: Mathlib.RingTheory.Valuation.Integral

Goal state before:
pp: case pos
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hf : eval₂ (algebraMap O R) x f = 0
hn : f.natDegree = 0
⊢ v x ≤ 1

Tactic:
Polynomial.natDegree_eq_zero

Goal state after:
case pos
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : R
a✝ : Nontrivial R
this : Nontrivial O
f : O[X]
hm : f.Monic
hf : eval₂ (algebraMap O R) x f = 0
hn : ∃ x, C x = f
⊢ v x ≤ 1
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

Goal state before:
pp: A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ (HomogeneousLocalization.mk { deg := m * nx, num := ⟨(proj 𝒜 nx) x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal ∧
      ∀ (b : ℕ),
        b ≠ nx →
          HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) x ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
            q.asIdeal) ∨
    ∀ (x : ℕ),
      HomogeneousLocalization.mk { deg := m * x, num := ⟨(proj 𝒜 x) y ^ m, ⋯⟩, den := ⟨f ^ x, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

Tactic:
and_iff_left,

Goal state after:
A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ HomogeneousLocalization.mk { deg := m * nx, num := ⟨(proj 𝒜 nx) x ^ m, ⋯⟩, den := ⟨f ^ nx, ⋯⟩, den_mem := ⋯ } ∈
      q.asIdeal ∨
    ∀ (x : ℕ),
      HomogeneousLocalization.mk { deg := m * x, num := ⟨(proj 𝒜 x) y ^ m, ⋯⟩, den := ⟨f ^ x, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal

A : Type u_1
σ : Type u_2
inst✝³ : CommRing A
inst✝² : SetLike σ A
inst✝¹ : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝ : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
x y : A
x✝¹ : IsHomogeneousElem 𝒜 x
x✝ : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ ∀ (b : ℕ),
    b ≠ nx →
      HomogeneousLocalization.mk { deg := m * b, num := ⟨(proj 𝒜 b) x ^ m, ⋯⟩, den := ⟨f ^ b, ⋯⟩, den_mem := ⋯ } ∈
        q.asIdeal
Module: Mathlib.AlgebraicGeometry.Modules.Tilde

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

Tactic:
have hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i) := by
            rw [← mul_assoc]
            exact basicOpen_mul_le_left _ _

Goal state after:
case refine_1
R : CommRingCat
M : (Spec R).Modules
V : (Spec R).Opens
ι : Type u_1
inst✝ : Finite ι
g : ι → ↑R
hg : V = ⨆ i, basicOpen (g i)
h₁ : ∀ (i : ι), Aux M (basicOpen (g i))
h₂ : ∀ (i j : ι), Aux M (basicOpen (g i * g j))
hgle : ∀ (i : ι), basicOpen (g i) ≤ V
hug : ∀ (i : ι) (m : ℕ), IsUnit ((algebraMap (↑R) (Module.End ↑R ↑Γ(M, basicOpen (g i)))) (g i ^ m))
f : ↑R
hf : basicOpen f ≤ V
s : ↑Γ(M, basicOpen f)
hfgi : ∀ (i : ι), basicOpen (f * g i) ≤ basicOpen (g i)
s' : (i : ι) → ↑Γ(M, basicOpen (f * g i)) := fun i ↦ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) s
N : ℕ
t : (i : ι) → ↑Γ(M, basicOpen (g i))
ht : ∀ (i : ι), f ^ N • s' i = (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i)
i j : ι
hfgigi : basicOpen (f * (g i * g j)) ≤ basicOpen (f * g i)
⊢ (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t i) -
        (ConcreteCategory.hom (M.presheaf.map (homOfLE ⋯).op)) (t j)) =
    0
Module: Mathlib.AlgebraicGeometry.ValuativeCriterion

Goal state before:
pp: case right
X Y : Scheme
f : X ⟶ Y
inst✝ : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := ⋯
g : Z ⟶ Spec (CommRingCat.of S.R) := ⋯
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop g))

Tactic:
rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
    exact this.right

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

Goal state before:
pp: case refine_3.inr.refine_1
P : MorphismProperty Scheme
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
F : Schemeᵒᵖ ⥤ Type u_1
inst✝ : IsZariskiLocalAtSource P
x✝ :
  Presieve.IsSheaf zariskiTopology F ∧
    ∀ {R S : CommRingCat} (f : R ⟶ S),
      P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
hzar : Presieve.IsSheaf zariskiTopology F
hff :
  ∀ {R S : CommRingCat} (f : R ⟶ S),
    P (Spec.map f) → Surjective (Spec.map f) → Presieve.IsSheafFor F (Presieve.singleton (Spec.map f))
T : Scheme
𝒰 : Cover (propQCPrecoverage P) T
this : ∀ ⦃T : Scheme⦄ (𝒰 : Cover (propQCPrecoverage P) T), (∃ R, T = Spec R) → Presieve.IsSheafFor F 𝒰.presieve₀
hT : ¬∃ R, T = Spec R
i : T.affineOneHypercover.I₀
⊢ Presieve.IsSheafFor F
    (Presieve.ofArrows (fun i_1 ↦ pullback (𝒰.f i_1) (T.affineOneHypercover.f i)) fun x ↦
      pullback.snd (𝒰.f x) (T.affineOneHypercover.f i))

Tactic:
exact this (𝒰.pullback₂ (T.affineCover.f i)) ⟨_, rfl⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
Y : C
a : α
g : Y ⟶ X a
⊢ (generate (Presieve.ofArrows X π)).arrows (g ≫ π a)

Tactic:
exact ⟨_, g, π a, ⟨a⟩, rfl⟩

Goal state after:
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
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) = val₀

Tactic:
simp only [← e.map_zero]

Goal state after:
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
hj : ¬IsMax j
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) (d.succ j hj e.val) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e.val
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w'
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
α : J → Type t
A B : (j : J) → α j → C
basicCell : (j : J) → (i : α j) → A j i ⟶ B j i
X Y : C
f : X ⟶ Y
c✝ : RelativeCellComplex basicCell f
c : RelativeCellComplex basicCell f
I : MorphismProperty C
hc : ∀ (s : c.Cells), I (basicCell s.j s.i)
j : J
hj : ¬IsMax j
⊢ (coproducts.{w, v, u} I).pushouts (c.F.map (homOfLE ⋯))

Tactic:
by
    let a := c.attachCells j hj
    exact ⟨_, _, _, _, _,
      colimitsOfShape_le_coproducts _ a.ι _
        (colimitsOfShape.mk' _ _ _ _ a.isColimit₁ a.isColimit₂
        (Discrete.natTrans (fun _ ↦ basicCell _ _))
        (fun ⟨k⟩ ↦ hc { j := j, hj := hj, k := k }) _
        (fun _ ↦ a.hm _)),
      a.isPushout⟩

Goal state after:
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 κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
⊢ (succStruct I κ).prop f✝ → (propArrow I).functorCategory (Arrow C) f✝

Tactic:
⟨F⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
this✝² : LocallySmall.{w, v, u} C
this✝¹ : IsSmall.{w, v, u} I
this✝ : ∀ (X Y : C) (p : X ⟶ Y), HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C
this : HasPushouts C
X✝ Y✝ : Arrow C ⥤ Arrow C
f✝ : X✝ ⟶ Y✝
F : Arrow C ⥤ Arrow C
⊢ (propArrow I).functorCategory (Arrow C) ((succStruct I κ).toSucc F)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ 0 ≤ f.norm

Tactic:
by
  classical exact if hf : f ≈ 0 then by simp [hf, norm] else by simp [norm, hf, padicNorm.nonneg]

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
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
have hfg' : f + g ≈ f := by
          change LimZero (g - 0) at hg
          change LimZero (f + g - f); · simpa only [add_sub_cancel_left, sub_zero] using hg
        have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
        have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
        have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
        rw [this, hcfg]

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

Goal state before:
pp: case e_a
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 η
Y : B
⊢ hF.inv.app (G.obj Y) ≫
      (eA.functor ⋙ e'.functor).map (eA.unitIso.hom.app (G.obj Y)) ≫
        (eA.functor ⋙ e'.functor).map (eA.inverse.map (hG.inv.app Y)) ≫
          e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y)) ≫ hG.hom.app Y) ≫
            hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y

Tactic:
simp only [Functor.comp_map, Equivalence.fun_inv_map, comp_obj, id_obj, map_comp, assoc]

Goal state after:
case e_a
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 η
Y : B
⊢ hF.inv.app (G.obj Y) ≫
      e'.functor.map (eA.functor.map (eA.unitIso.hom.app (G.obj Y))) ≫
        e'.functor.map (eA.counit.app (eA.functor.obj (G.obj Y))) ≫
          e'.functor.map (hG.inv.app Y) ≫
            e'.functor.map (eA.counitInv.app (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (eA.counitIso.hom.app (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (hG.hom.app Y) ≫ hF.hom.app (G.obj Y) ≫ η.hom.app Y =
    η.hom.app Y
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
⊢ PadicSeq.valuation f = PadicSeq.valuation g

Tactic:
by_cases hf : f ≈ 0
    · have hg : g ≈ 0 := Setoid.trans (Setoid.symm h) hf
      simp [hf, hg, PadicSeq.valuation]
    · have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)
      rw [PadicSeq.val_eq_iff_norm_eq hf hg]
      exact PadicSeq.norm_equiv h

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

Goal state before:
pp: case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬0 + 1 ≤ ↑((fun i ↦ i) ⟨0, ⋯⟩) + q
hi : 0 = ↑((fun i ↦ i) ⟨0, ⋯⟩) + q
⊢ X.σ ((fun i ↦ i) ⟨0, ⋯⟩) ≫ (P (q + 1)).f (0 + 1) = 0

Tactic:
dsimp at h hi

Goal state after:
case neg.zero.«_@».Mathlib.AlgebraicTopology.DoldKan.Degeneracies.1127126258._hygCtx._hyg.66.«0»
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : ∀ (i : Fin (0 + 1)), 0 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (0 + 1) = 0
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ ((fun i ↦ i) ⟨0, ⋯⟩) ≫ (P (q + 1)).f (0 + 1) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case mk.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1 + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
clear h₂ hi

Goal state after:
case mk.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
h₁ : ⦋m⦌.len ≠ n
k : ℕ
hk : n = m + k + 1 + 1
⊢ PInfty.f n ≫ X.map i.op = 0
Module: Mathlib.Topology.Homotopy.Product

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

Tactic:
rw [← Path.Homotopic.Quotient.mk_trans, Path.trans_pi_eq_pi_trans, ← pi_lift]

Goal state after:
case h.h
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs cs : (i : ι) → X i
a : (i : ι) → Path (bs i) (cs i)
a✝ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i ↦ Quotient.mk ((a✝ i).trans (a i))) = pi fun i ↦ Quotient.mk (a✝ i) ⬝ Quotient.mk (a i)
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₂
⊢ projRight (prod (Quotient.mk a✝) (Quotient.mk b✝)) = Quotient.mk b✝

Tactic:
projRight,

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.snd, continuous_toFun := ⋯ } = Quotient.mk b✝
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : ↑I
hx : x = 1
⊢ { toFun := fun x ↦ p ⟨↑(σ (t, x).1) * ↑(t, x).2 + ↑(t, x).1 * ↑(f (t, x).2), ⋯⟩, continuous_toFun := ⋯ } 1 =
    p.toContinuousMap 1

Tactic:
simp [hf₁]

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

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂

Tactic:
convert! simply_connected_iff_paths_homotopic (Y := Y)

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), p₁.Homotopic p₂) ↔ Subsingleton (Path.Homotopic.Quotient a✝¹ a✝)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ p ⟨reflTransSymmAux (1, x), ⋯⟩ = (p.trans p.symm).toContinuousMap x

Tactic:
simp only [reflTransSymmAux, Path.trans]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ 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
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: X : SSet
f g : ∂Δ[0].toSSet ⟶ X
⊢ f = g

Tactic:
ext _ ⟨x, hx⟩
  simp at hx

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

Goal state before:
pp: Z : SSet
⊢ Z.KanComplex ↔
    ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
      horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj

Tactic:
refine ⟨fun _ n i f hf ↦ hf.exists_lift_of_kanComplex,
    fun h ↦ (isFibrant_iff _).2 ⟨?_⟩⟩

Goal state after:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
⊢ fibrations SSet (terminal.from Z)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case some.left
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x : (span t l).obj (some WalkingPair.left)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.left))) x) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = (ConcreteCategory.hom (h.cocone.ι.app (some WalkingPair.left))) x

Tactic:
exact Or.inl ⟨x, rfl⟩

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

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

Tactic:
exact face_le_horn (2 : Fin 3) 1 (by simp)

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

Goal state before:
pp: n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
⊢ ∀ (a : (MultispanShape.ofLinearOrder ↑{i}ᶜ).L),
    (((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).fst a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).fst a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj) =
      ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor).snd a ≫
        match (MultispanShape.ofLinearOrder ↑{i}ᶜ).snd a with
        | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj

Tactic:
by
    obtain _ | n := n
    · rintro ⟨⟨a, b⟩, hab⟩
      grind
    · rintro ⟨⟨⟨a, ha⟩, ⟨b, hb⟩⟩, hab : a < b⟩
      simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at ha hb
      dsimp
      rw [homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_pred_assoc _ _ hab,
        homOfLE_faceSingletonComplIso_inv_eq_facePairComplIso_inv_δ_castPred_assoc _ _ hab,
        hf.δ_pred_comp ..]

Goal state after: