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

Goal state before:
pp: case e_x
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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ : e₁.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val, ⋯⟩
h₂ : e₂.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val, ⋯⟩
l : J
hl : l ∈ Set.Iio i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val

Tactic:
have := hi' l hl

Goal state after:
case e_x
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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ : e₁.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val, ⋯⟩
h₂ : e₂.val = d.lift i hi ⟨fun x ↦ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.val, ⋯⟩
l : J
hl : l ∈ Set.Iio i
this : Subsingleton (d.Extension val₀ l)
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₁.val = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) e₂.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 κ
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
⊢ (succStruct I κ).prop ≤ (propArrow I).functorCategory (Arrow C)

Tactic:
intro _ _ _ ⟨F⟩ 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
f : Arrow C
⊢ propArrow I (((succStruct I κ).toSucc F).app f)
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 κ
X Y : C
f : X ⟶ Y
⊢ I.rlp.llp (ιObj I κ f)

Tactic:
by
  apply I.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp κ.ord.ToType
  apply transfiniteCompositionsOfShape_ιObj

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
⊢ HasLiftingProperty i p

Tactic:
obtain ⟨J, _, _, _, _, ⟨h⟩⟩ :=
      generatingMonomorphisms.exists_transfiniteCompositionOfShape hG i

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
G : C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
hG : IsSeparator G
X Y : C
p : X ⟶ Y
hp : (generatingMonomorphisms G).rlp p
A B : C
i : A ⟶ B
x✝ : Mono i
J : Type w
w✝³ : LinearOrder J
w✝² : OrderBot J
w✝¹ : SuccOrder J
w✝ : WellFoundedLT J
h : (generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J i
⊢ HasLiftingProperty i p
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ if q = 0 then 0 else ↑p ^ (-padicValRat p q)

Tactic:
split_ifs

Goal state after:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ 0 ≤ ↑p ^ (-padicValRat p q)
Module: Mathlib.NumberTheory.Padics.PadicNorm

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

Tactic:
split_ifs

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

Goal state before:
pp: case mpr
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ ((↑p)⁻¹ < if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) → (if ↑m = 0 then 0 else ↑p ^ (-padicValRat p ↑m)) = 1

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ↑m = 0
⊢ (↑p)⁻¹ < 0 → 0 = 1

case neg
p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
h✝ : ¬↑m = 0
⊢ (↑p)⁻¹ < ↑p ^ (-padicValRat p ↑m) → ↑p ^ (-padicValRat p ↑m) = 1
Module: Mathlib.NumberTheory.Padics.PadicNorm

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m : ℤ
⊢ padicNorm p ↑m = 1 ↔ ¬↑p ∣ m

Tactic:
nth_rw 2 [← pow_one p]
  simp only [dvd_iff_norm_le, Nat.cast_one, zpow_neg, zpow_one, not_le]
  constructor
  · intro h
    rw [h, inv_lt_one₀] <;> norm_cast
    · exact Nat.Prime.one_lt Fact.out
    · exact Nat.Prime.pos Fact.out
  · simp only [padicNorm]
    split_ifs
    · rw [inv_lt_zero, ← Nat.cast_zero, Nat.cast_lt]
      intro h
      exact (Nat.not_lt_zero p h).elim
    · have : 1 < (p : ℚ) := by norm_cast; exact Nat.Prime.one_lt (Fact.out : Nat.Prime p)
      rw [← zpow_neg_one, zpow_lt_zpow_iff_right₀ this]
      have : 0 ≤ padicValRat p m := by simp only [of_int, Nat.cast_nonneg]
      intro h
      rw [← zpow_zero (p : ℚ), zpow_right_inj₀] <;> linarith

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
⊢ (if x✝ * y✝ = 0 then 0 else exp (-padicValRat p (x✝ * y✝))) =
    (if x✝ = 0 then 0 else exp (-padicValRat p x✝)) * if y✝ = 0 then 0 else exp (-padicValRat p y✝)

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ 0 = 0 * 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 = 0 * exp (-padicValRat p y✝)

case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ 0 = exp (-padicValRat p x✝) * 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 = exp (-padicValRat p x✝) * exp (-padicValRat p y✝)

case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = 0 * 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = 0 * exp (-padicValRat p y✝)

case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = exp (-padicValRat p x✝) * 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ * y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ * y✝)) = exp (-padicValRat p x✝) * exp (-padicValRat p y✝)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
⊢ (if x✝ + y✝ = 0 then 0 else exp (-padicValRat p (x✝ + y✝))) ≤
    max (if x✝ = 0 then 0 else exp (-padicValRat p x✝)) (if y✝ = 0 then 0 else exp (-padicValRat p y✝))

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ 0 ≤ max 0 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 ≤ max 0 (exp (-padicValRat p y✝))

case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ 0 ≤ max (exp (-padicValRat p x✝)) 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ 0 ≤ max (exp (-padicValRat p x✝)) (exp (-padicValRat p y✝))

case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max 0 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max 0 (exp (-padicValRat p y✝))

case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max (exp (-padicValRat p x✝)) 0

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ
h✝² : ¬x✝ + y✝ = 0
h✝¹ : ¬x✝ = 0
h✝ : ¬y✝ = 0
⊢ exp (-padicValRat p (x✝ + y✝)) ≤ max (exp (-padicValRat p x✝)) (exp (-padicValRat p y✝))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (if x = 0 then 0 else exp (-↑(padicValInt p x))) ≤ 1

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : x = 0
⊢ 0 ≤ 1

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) ≤ 1
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
⊢ (if x = 0 then 0 else exp (-↑(padicValInt p x))) = 1 ↔ ¬↑p ∣ x

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : x = 0
⊢ 0 = 1 ↔ ¬↑p ∣ x

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ exp (-↑(padicValInt p x)) = 1 ↔ ¬↑p ∣ x
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case pos
p : ℕ
a : ℤ
hp : p = 1
⊢ 1 ^ padicValInt 1 a ∣ a

Tactic:
one_pow

Goal state after:
case pos
p : ℕ
a : ℤ
hp : p = 1
⊢ 1 ∣ a
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) =
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))

Tactic:
split_ifs

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
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
⊢ (if hf : f + g ≈ 0 then 0 else padicNorm p (↑(f + g) (stationaryPoint hf))) ≤
    max (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf)))

Tactic:
split_ifs

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) (stationaryPoint hfg)) ≤
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
⊢ (f + g).norm ≤ max f.norm g.norm

Tactic:
by
  classical
  exact if hfg : f + g ≈ 0 then by
    have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
    simpa only [hfg, norm]
  else
    if hf : f ≈ 0 then by
      have hfg' : f + g ≈ g := by
        change LimZero (f - 0) at hf
        change LimZero (f + g - g); · simpa only [sub_zero, add_sub_cancel_right] using hf
      have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
      have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
      have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
      rw [this, hcfg]
    else
      if hg : g ≈ 0 then by
        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]
      else norm_nonarchimedean_aux hfg hf hg

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

Goal state before:
pp: case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
x : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj (Etale.mk f)
⊢ ∃ j,
    (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j ∧
      Nonempty (j ⟶ ⟨Etale.mk f, x⟩)

Tactic:
obtain ⟨y, hy, rfl⟩ := Over.homMk_surjective x

Goal state after:
case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
Y : Scheme
f : Y ⟶ S
x✝ : Etale f
y : (unop (op (Over.mk s))).left ⟶ ((Etale.forget S).obj (Etale.mk f)).left
hy : y ≫ ((Etale.forget S).obj (Etale.mk f)).hom = (unop (op (Over.mk s))).hom
⊢ ∃ j,
    (Functor.Elements.precomp (AffineEtale.Spec S) (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s)))).essImage j ∧
      Nonempty (j ⟶ ⟨Etale.mk f, Over.homMk y ⋯⟩)
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ P snd

Tactic:
refine (P.arrow_mk_iso_iff ?_).2 H

Goal state after:
case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
P : MorphismProperty C
inst✝² : F.Faithful
inst✝¹ : F.Full
inst✝ : P.RespectsIso
f : X ⟶ Y
h₀ : ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ b fst snd, ∃ (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ Arrow.mk snd ≅ Arrow.mk g_snd
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 : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ = 0

Tactic:
split_ifs

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : c.Rel m n
⊢ 0 ≫ eqToHom ⋯ = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (f.app (op ⦋n⦌) ≫ if n < q then 0 else (-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) =
    (if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)

Tactic:
split_ifs

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
h✝ : n < q
⊢ f.app (op ⦋n⦌) ≫ 0 = 0 ≫ f.app (op ⦋n + 1⦌)

case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
h✝ : ¬n < q
⊢ f.app (op ⦋n⦌) ≫ ((-1) ^ (n - q) • Y.σ ⟨n - q, ⋯⟩) = ((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ f.app (op ⦋n + 1⦌)
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 m : ℕ
hnm : c.Rel m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    G.map ((if n < q then 0 else (-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯)

Tactic:
split_ifs

Goal state after:
case pos
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 m : ℕ
hnm : c.Rel m n
h✝ : n < q
⊢ 0 ≫ eqToHom ⋯ = G.map (0 ≫ eqToHom ⋯)

case neg
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 m : ℕ
hnm : c.Rel m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • (((whiskering C D).obj G).obj X).σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯ =
    G.map (((-1) ^ (n - q) • X.σ ⟨n - q, ⋯⟩) ≫ eqToHom ⋯)
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.mapHomologicalComplex c).map (nullHomotopicMap' (hσ' q))).f n =
    (nullHomotopicMap' fun i j hij ↦ G.map (hσ' q i j hij)).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

Tactic:
simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq

Goal state after:
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
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ {x y : ℚ_[p]}, ↑(padicNormE (x - y)) = 0 → x = y

Tactic:
intro _ _ h

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
h : ↑(padicNormE (x✝ - y✝)) = 0
⊢ x✝ = y✝
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
a b c d e f : Y ⟶ X _⦋n + 1⦌
⊢ b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f

Tactic:
h1

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
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
⊢ d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
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
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ b = f

Tactic:
h1

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
a b c d e f : Y ⟶ X _⦋n + 1⦌
h1 : b = f
h2 : d + e = 0
h3 : c + a = 0
⊢ f = f
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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ∑ i, ((-1) ^ a * (-1) ^ ↑i) • φ ≫ X.δ ⟨↑i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ +
        ((-1) ^ a * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ +
      (∑ i, ((-1) ^ ↑i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨↑i, ⋯⟩ +
          ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 1, ⋯⟩ +
        ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 2, ⋯⟩) =
    -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩

Tactic:
apply simplif

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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ a * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ 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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 1, ⋯⟩ +
      ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 2, ⋯⟩ =
    0

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
simplif : ∀ (a b c d e f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
⊢ ∑ i, ((-1) ^ ↑i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨↑i, ⋯⟩ +
      ∑ i, ((-1) ^ a * (-1) ^ ↑i) • φ ≫ X.δ ⟨↑i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ =
    0
Module: Mathlib.AlgebraicTopology.DoldKan.Faces

Goal state before:
pp: case neg.h.hj₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hqn : n < q
hqn' : ¬n + 1 < q
j : Fin (n + 1)
⊢ n + 2 ≤ ↑(j.succ.succ.pred ⋯) + q

Tactic:
dsimp
        lia

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
⊢ (if x✝¹ * x✝ = 0 then 0 else exp (-(x✝¹ * x✝).valuation)) =
    (if x✝¹ = 0 then 0 else exp (-x✝¹.valuation)) * if x✝ = 0 then 0 else exp (-x✝.valuation)

Tactic:
split_ifs

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ * x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : x✝ = 0
⊢ 0 = 0 * 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ * x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ 0 = 0 * exp (-x✝.valuation)

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ * x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : x✝ = 0
⊢ 0 = exp (-x✝¹.valuation) * 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ * x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ 0 = exp (-x✝¹.valuation) * exp (-x✝.valuation)

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ * x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : x✝ = 0
⊢ exp (-(x✝¹ * x✝).valuation) = 0 * 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ * x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ exp (-(x✝¹ * x✝).valuation) = 0 * exp (-x✝.valuation)

case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ * x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : x✝ = 0
⊢ exp (-(x✝¹ * x✝).valuation) = exp (-x✝¹.valuation) * 0

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ * x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ exp (-(x✝¹ * x✝).valuation) = exp (-x✝¹.valuation) * exp (-x✝.valuation)