mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ ∃ a, v a = γ

pp: case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ ∃ a, v a = γ

Tactic:
<;>

Goal state after:
case mp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ ∃ a, v a = γ

case mpr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
h : Function.Surjective ⇑v
γ : Γ₀
⊢ ∃ a, v a = γ
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

case inr
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

pp: case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
<;>

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  (algebraMap (↥(valuationSubringAtPrime K v)) K) (r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2) =
    (algebraMap (↥(valuationSubringAtPrime K v)) K) ((algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1)
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

pp: case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  (algebraMap (↥(valuationSubringAtPrime K v)) K) (r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2) =
    (algebraMap (↥(valuationSubringAtPrime K v)) K) ((algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1)
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
<;>

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  (algebraMap (↥(valuationSubringAtPrime K v)) K) (r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2) =
    (algebraMap (↥(valuationSubringAtPrime K v)) K) ((algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1)
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  (algebraMap (↥(valuationSubringAtPrime K v)) K) (r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2) =
    (algebraMap (↥(valuationSubringAtPrime K v)) K) ((algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1)
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), x i ∈ (f.rangeIcc g) i) ↔ f ≤ x ∧ x ≤ g

Tactic:
mem_rangeIcc_apply_iff

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f✝ g✝ f g x : ι →₀ α
⊢ (∀ (i : ι), f i ≤ x i ∧ x i ≤ g i) ↔ f ≤ x ∧ x ≤ g
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
x : σ →₀ ℕ
r : R
h : x ∉ s
⊢ (truncFinset R s) ((monomial x) r) = 0

Tactic:
by
  classical
  ext; simp [truncFinset, MvPolynomial.coeff_sum, coeff_monomial]
  grind

Goal state after:
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ #(Ioo f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2

Tactic:
by
  rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑((truncFinset R t) p)) = MvPolynomial.coeff x ((truncFinset R s) p)

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∉ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑((truncFinset R t) p)) = MvPolynomial.coeff x ((truncFinset R s) p)

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑((truncFinset R t) p)) = MvPolynomial.coeff x ((truncFinset R s) p)

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
h : s ⊆ t
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∉ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑((truncFinset R t) p)) = MvPolynomial.coeff x ((truncFinset R s) p)
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
s : Finset (σ →₀ ℕ)
inst✝ : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset S s) ((map f) p)) =
    MvPolynomial.coeff x ((MvPolynomial.map f) ((truncFinset R s) p))

pp: case neg
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
s : Finset (σ →₀ ℕ)
inst✝ : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∉ s
⊢ MvPolynomial.coeff x ((truncFinset S s) ((map f) p)) =
    MvPolynomial.coeff x ((MvPolynomial.map f) ((truncFinset R s) p))

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
s : Finset (σ →₀ ℕ)
inst✝ : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset S s) ((map f) p)) =
    MvPolynomial.coeff x ((MvPolynomial.map f) ((truncFinset R s) p))

case neg
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : CommSemiring R
s : Finset (σ →₀ ℕ)
inst✝ : CommSemiring S
f : R →+* S
p : MvPowerSeries σ R
x : σ →₀ ℕ
h✝ : x ∉ s
⊢ MvPolynomial.coeff x ((truncFinset S s) ((map f) p)) =
    MvPolynomial.coeff x ((MvPolynomial.map f) ((truncFinset R s) p))
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
h✝ : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑p) = MvPolynomial.coeff x p

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
h✝ : x ∉ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑p) = MvPolynomial.coeff x p

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
h✝ : x ∈ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑p) = MvPolynomial.coeff x p

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPolynomial σ R
h : p.support ⊆ s
x : σ →₀ ℕ
h✝ : x ∉ s
⊢ MvPolynomial.coeff x ((truncFinset R s) ↑p) = MvPolynomial.coeff x p
Module: Mathlib.Topology.Algebra.TopologicallyNilpotent

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
⊢ ∀ (ib : Ideal R), ↑ib ∈ 𝓝 0 → ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑ib

Tactic:
intro I I_mem_nhds

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : ↑I ∈ 𝓝 0
⊢ ∃ ia, ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ ↑I
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p = weightedOrder w f
hf' : (weightedHomogeneousComponent w p) f = 0
⊢ ↑(weightedOrder w f).toNat = weightedOrder w f

Tactic:
by rw [← hf, toNat_natCast]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
⊢ ∃ t ∈ 𝓝 0, toCompletion ⁻¹' t ⊆ s

Tactic:
· refine ⟨{y | Valued.v.restrict y < ↑(Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv γ)},
        ?_, fun x hx ↦ hγ ?_⟩
      · rw [Valued.mem_nhds_zero]
        exact ⟨Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv γ, subset_rfl⟩
      · rw [Set.mem_ofPred_eq, ← map_lt_map_iff (valueGroupOrderIso K v),
          valueGroupOrderIso_restrict]
        simpa using hx

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ ⊤ < ⊤ ↔ φ ≠ 0

pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ¬φ = 0
⊢ ↑(Nat.find ⋯) < ⊤ ↔ φ ≠ 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ ⊤ < ⊤ ↔ φ ≠ 0

case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ¬φ = 0
⊢ ↑(Nat.find ⋯) < ⊤ ↔ φ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h✝ : m = 0
⊢ a = a

pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0

pp: case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a

pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h✝ : m = 0
⊢ a = a

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0

case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : m = 0
⊢ 0 = a

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h✝ : ¬m = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i = ↑n → (coeff i) ((monomial n) a) ≠ 0

pp: case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i < ↑n → (coeff i) ((monomial n) a) = 0

Tactic:
<;>

Goal state after:
case neg.left
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i = ↑n → (coeff i) ((monomial n) a) ≠ 0

case neg.right
R : Type u_1
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (i : ℕ), ↑i < ↑n → (coeff i) ((monomial n) a) = 0
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: case mp
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology Rᵐᵒᵖ M → IsLinearTopology R M

pp: case mpr
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology R M → IsLinearTopology Rᵐᵒᵖ M

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology Rᵐᵒᵖ M → IsLinearTopology R M

case mpr
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology R M → IsLinearTopology Rᵐᵒᵖ M
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.34 ≤ 0

pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞

Tactic:
← @order_one R _ _,

Goal state after:
case self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.34 ≤ order 1

R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

pp: case pos.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

Tactic:
<;>

Goal state after:
case pos.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order

case pos.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : ψ = 0
⊢ (φ * ψ).order ≤ φ.order + ψ.order
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ ContinuousAt (⇑(eval₂Hom φ a)) 0

Tactic:
ContinuousAt,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ Tendsto (⇑(eval₂Hom φ a)) (𝓝 0) (𝓝 ((eval₂Hom φ a) 0))
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

pp: case pos.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
<;>

Goal state after:
case pos.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

case pos.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
⊢ HasSum (fun d ↦ φ ((coeff d) f) * a ^ d) (eval₂ φ a f)

Tactic:
by
  have := MvPowerSeries.hasSum_eval₂ hφ (hasEval ha) f
  simp only [PowerSeries.eval₂]
  rw [← (Finsupp.single_injective ()).hasSum_iff] at this
  · convert this; simp
  · intro d hd
    exact False.elim (hd ⟨d (), by ext; simp⟩)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case pos
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
h✝ : 0 < x i
⊢ IsNilpotent (constantCoeff (a i))

pp: case neg
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
h✝ : ¬0 < x i
⊢ IsNilpotent 0

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
h✝ : 0 < x i
⊢ IsNilpotent (constantCoeff (a i))

case neg
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
h✝ : ¬0 < x i
⊢ IsNilpotent 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case e'_4
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst✝³

pp: case e'_7
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst✝¹

Tactic:
<;>

Goal state after:
case e'_4
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst✝³

case e'_7
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
⊢ ⊥ = inst✝¹
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case false
c : ℝ
f : ℕ → Bool
h : f 0 = false
⊢ cantorFunctionAux c f 0 = bif false then 1 else 0

pp: case true
c : ℝ
f : ℕ → Bool
h : f 0 = true
⊢ cantorFunctionAux c f 0 = bif true then 1 else 0

Tactic:
<;>

Goal state after:
case false
c : ℝ
f : ℕ → Bool
h : f 0 = false
⊢ cantorFunctionAux c f 0 = bif false then 1 else 0

case true
c : ℝ
f : ℕ → Bool
h : f 0 = true
⊢ cantorFunctionAux c f 0 = bif true then 1 else 0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
cases h : f (n + 1)

Goal state after:
case false
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = false
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = true
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n