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

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

pp: 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✝)

pp: 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

pp: 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✝)

pp: 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

pp: 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✝)

pp: 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

pp: 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✝)

Tactic:
<;>

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 : ℤ
⊢ (padicValuation p) x = 0 ↔ x = 0

Tactic:
by
  simp [← Rat.padicValuation_cast]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (padicValuation p) ↑p = exp (-1)

Tactic:
by
  simp [← Rat.padicValuation_cast]

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

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ -↑(padicValInt p x) ≤ log 1

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ 1 ≠ 0

Tactic:
<;>

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℤ
h✝ : ¬x = 0
⊢ -↑(padicValInt p x) ≤ log 1

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) ↑x.num / (padicValuation p) ↑x.den ≤ 1 ↔ ¬↑p ∣ ↑x.den

Tactic:
← Int.padicValuation_eq_one_iff,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ (padicValuation p) ↑x.num / (padicValuation p) ↑x.den ≤ 1 ↔ (Int.padicValuation p) ↑x.den = 1
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.natAbs ≠ 0

pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.natAbs ≠ 0

Tactic:
<;>

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.natAbs ≠ 0

case a
p : ℕ
hp : Fact (Nat.Prime p)
a b : ℤ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.natAbs ≠ 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
h0 : x = 0
⊢ False

Tactic:
h0,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x✝ y : ℤ_[p]
x : ℚ_[p]
hx : ¬‖0‖ ≤ 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
h0 : x = 0
⊢ False
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this : (g - 0).LimZero
⊢ LimZero (f + g - f)

Tactic:
simpa only [add_sub_cancel_left, sub_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
⊢ f.norm = max f.norm 0

Tactic:
max_eq_left (norm_nonneg _)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : f.norm ≠ g.norm
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : (g - 0).LimZero
this : f + g ≈ f
h1 : (f + g).norm = f.norm
h2 : g.norm = 0
⊢ f.norm = f.norm
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: case h₁
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.fst' (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.fst' (f i)

pp: case h₂
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.snd (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.snd (f i)

Tactic:
<;>

Goal state after:
case h₁
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.fst' (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.fst' (f i)

case h₂
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i✝ j k i : ι
⊢ ⋯.symmetry ⋯ ≫ ⋯.snd (f i) =
    𝟙
        (match (i, i) with
        | (i, j) => ⋯.pullback (f j)) ≫
      ⋯.snd (f i)
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: case h₀
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)

pp: case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)

Tactic:
<;>

Goal state after:
case h₀
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)

case h₁
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst✝¹ : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst✝ : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)
Module: Mathlib.AlgebraicGeometry.Sites.Representability

Goal state before:
pp: case left
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst✝ : Presheaf.IsLocallySurjective zariskiTopology (Sigma.desc f)
⊢ Sheaf.IsLocallyInjective (yonedaGluedToSheaf hf)

pp: case right
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst✝ : Presheaf.IsLocallySurjective zariskiTopology (Sigma.desc f)
⊢ Sheaf.IsLocallySurjective (yonedaGluedToSheaf hf)

Tactic:
<;>

Goal state after:
case left
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst✝ : Presheaf.IsLocallySurjective zariskiTopology (Sigma.desc f)
⊢ Sheaf.IsLocallyInjective (yonedaGluedToSheaf hf)

case right
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → yoneda.obj (X i) ⟶ F.obj
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
inst✝ : Presheaf.IsLocallySurjective zariskiTopology (Sigma.desc f)
⊢ Sheaf.IsLocallySurjective (yonedaGluedToSheaf hf)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
by
  simpa [p.coprime_comm] using norm_intCast_eq_one_iff (p := p) (z := n)

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

Goal state before:
pp: case neg.h
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
⊢ ∀ (a : Fin (n + 1)), φ ≫ X.σ 0 ≫ ((-1) ^ ↑a.succ.succ • X.δ a.succ.succ) = 0

Tactic:
intro j
      rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
      · simp [Fin.succ_ne_zero]
      · dsimp
        lia
      · simp only [Fin.succ_lt_succ_iff, j.succ_pos]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ ⊤ = (if x = 0 then ⊤ else ↑x.valuation) + ⊤

Tactic:
WithTop.add_top

Goal state after:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ ⊤ = ⊤
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ↑⟨b + 1, ⋯⟩ < ↑j.succ

Tactic:
Fin.val_succ

Goal state after:
case H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ↑⟨b + 1, ⋯⟩ < ↑j + 1
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 : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ ((fun i ↦ i) ⟨0, ⋯⟩) ≫ (P (0 + 1)).f (0 + 1) = 0

Tactic:
change X.σ 0 ≫ (P 1).f 1 = 0

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.σ 0 ≫ (P 1).f 1 = 0
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

pp: 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)

pp: 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

pp: 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)

pp: 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

pp: 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)

pp: 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

pp: 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)

Tactic:
<;>

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)
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ((P q).f n.succ ≫ X.σ i) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0

Tactic:
Preadditive.comp_add,

Goal state after:
case neg.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq : ∀ (i : Fin (n + 1 + 1)), n + 1 + 1 ≤ ↑i + q → X.σ i ≫ (P q).f (n + 1 + 1) = 0
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i)
⊢ ((P q).f n.succ ≫ X.σ i) ≫ 𝟙 (X _⦋n + 1 + 1⦌) + ((P q).f n.succ ≫ X.σ i) ≫ (Hσ q).f (n + 1 + 1) +
      ((Q q).f (n + 1) ≫ X.σ i) ≫ (P q).f (n + 1 + 1) ≫ (𝟙 (X _⦋n + 1 + 1⦌) + (Hσ q).f (n + 1 + 1)) =
    0
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 ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0

Tactic:
Ne

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) = 0
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
⊢ { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } =
    𝟙 (N₁.obj X)

Tactic:
by
    ext n
    simp only [πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, Karoubi.comp_f,
      HomologicalComplex.comp_f, N₁_obj_p, Karoubi.id_f]

Goal state after:
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: case fst
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.fst = (G.symm.trans F.symm).fst

pp: case snd
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.snd = (G.symm.trans F.symm).snd

Tactic:
<;>

Goal state after:
case fst
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.fst = (G.symm.trans F.symm).fst

case snd
X Y : TopPair
f₀ f₁ f₂ : X ⟶ Y
F : Homotopy f₀ f₁
G : Homotopy f₁ f₂
⊢ (F.trans G).symm.snd = (G.symm.trans F.symm).snd
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ (F.extend (2 * ↑x.1)) x.2 = F (⟨2 * ↑x.1, ⋯⟩, x.2)

pp: case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.extend (2 * ↑x.1 - 1)) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

Tactic:
<;>

Goal state after:
case pos
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ↑x.1 ≤ 1 / 2
⊢ (F.extend (2 * ↑x.1)) x.2 = F (⟨2 * ↑x.1, ⋯⟩, x.2)

case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.extend (2 * ↑x.1 - 1)) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case pos
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'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ P { toFun := fun x ↦ (F.extend (2 * ↑t)) x, continuous_toFun := ⋯ }

pp: case neg
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'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ P { toFun := fun x ↦ (G.extend (2 * ↑t - 1)) x, continuous_toFun := ⋯ }

Tactic:
· exact F.extendProp _

Goal state after:
case neg
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'
P : C(X, Y) → Prop
f₀ f₁ f₂ : C(X, Y)
F : f₀.HomotopyWith f₁ P
G : f₁.HomotopyWith f₂ P
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ P { toFun := fun x ↦ (G.extend (2 * ↑t - 1)) x, continuous_toFun := ⋯ }
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝).1 = ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).1

pp: case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝).2 = ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).2

Tactic:
<;>

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝).1 = ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ ((prodToProdTop A B ⋙ (projLeft A B).prod' (projRight A B)).obj X✝).2 = ((𝟭 (↑(π.obj A) × ↑(π.obj B))).obj X✝).2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projLeft A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.1

pp: case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projRight A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.2

Tactic:
<;>

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projLeft A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj A) × ↑(π.obj B)
⊢ (projRight A B).obj { as := (X✝.1.as, X✝.2.as) } = X✝.2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as.1 =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as.1

pp: case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as.2 =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as.2

Tactic:
<;>

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as.1 =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as.1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as.2 =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as.2
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projLeft A B).obj X✝).as = X✝.as.1

pp: case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projRight A B).obj X✝).as = X✝.as.2

Tactic:
<;>

Goal state after:
case h_obj.fst
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projLeft A B).obj X✝).as = X✝.as.1

case h_obj.snd
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projRight A B).obj X✝).as = X✝.as.2