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

Goal state before:
pp: case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ v x * v y < ↑((Units.map ↑embedding) γ)

Tactic:
Hx,

Goal state after:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ofClass v).ValueGroup₀ˣ
γx : Γ₀ˣ
Hx : v x = ↑γx
u : (ofClass v).ValueGroup₀ˣ := Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu_def : u = Units.mk0 ((restrict₀ (ofClass v)) x) ⋯
hu : embedding ↑u⁻¹ = ↑γx⁻¹
y : R
vy_lt : v y < embedding ↑(u⁻¹ * γ)
⊢ ↑γx * v y < ↑((Units.map ↑embedding) γ)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ fromAffine { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P, nonsingular := hP }

Tactic:
rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]

Goal state after:
case neg
R : Type r
S : Type s
A F : Type u
B K : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Field F
inst✝¹ : Field K
W' : Jacobian R
W : Jacobian F
inst✝ : DecidableEq F
point✝ : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) P)
hPz : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsClosed[topologicalSpace] s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ

Tactic:
by
  simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici,
    compl_subset_compl]

Goal state after:
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 0 ×ˢ pure y) (𝓝 0)

Tactic:
prod_pure,

Goal state after:
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun p ↦ p.1 * p.2) (map (fun a ↦ (a, y)) (𝓝 0)) (𝓝 0)
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: α : Type u_3
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : IsUniformAddGroup α
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : IsUniformAddGroup γ
f g : α →+ γ
hf : Continuous ⇑f
hg : Continuous ⇑g
⊢ (f + g).completion ⋯ = f.completion hf + g.completion hg

Tactic:
by
  have hfg := hf.add hg
  ext x
  refine Completion.induction_on x ?_ ?_
  · exact isClosed_eq ((f + g).continuous_completion hfg)
      ((f.continuous_completion hf).add (g.continuous_completion hg))
  · simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]

Goal state after:
Module: Mathlib.Topology.Algebra.UniformRing

Goal state before:
pp: α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
⊢ ⋯.extend (⇑f) 0 = 0

Tactic:
convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0

Goal state after:
case e'_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
⊢ 0 = i 0

case e'_3
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : IsTopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : IsTopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing ⇑i
dr : DenseRange ⇑i
hf : UniformContinuous ⇑f
⊢ 0 = f 0
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ x * x.hatInv = 1

Tactic:
have : T1Space (hat K) := T2Space.t1Space
  let f := fun x : hat K => x * hatInv x
  let c := (fun (x : K) => (x : hat K))
  change f x = 1
  have cont : ContinuousAt f x := by fun_prop
  have clo : x ∈ closure (c '' {0}ᶜ) := by
    have := isDenseInducing_coe.dense x
    rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm,
      image_union] at this
    apply mem_closure_of_mem_closure_union this
    rw [image_singleton]
    exact compl_singleton_mem_nhds x_ne
  have fxclo : f x ∈ closure (f '' c '' {0}ᶜ) := mem_closure_image cont clo
  have : f '' c '' {0}ᶜ ⊆ {1} := by
    rw [image_image]
    rintro _ ⟨z, z_ne, rfl⟩
    rw [mem_singleton_iff]
    rw [mem_compl_singleton_iff] at z_ne
    dsimp [f]
    rw [hatInv_extends z_ne, ← coe_mul]
    rw [mul_inv_cancel₀ z_ne, coe_one]
  replace fxclo := closure_mono this fxclo
  rwa [closure_singleton, mem_singleton_iff] at fxclo

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
⊢ span {x * y} ≤ I

Tactic:
rw [← span_singleton_mul_span_singleton, ← hx, Ideal.sup_mul, sup_le_iff,
        span_singleton_mul_span_singleton, mul_comm a, span_singleton_le_iff_mem]

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
⊢ I * span {y} ≤ I ∧ y * a ∈ I
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
⊢ v ↑r ≤ 1

Tactic:
exact r.2

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
⊢ P.IsPrime → Submodule.IsPrincipal P

Tactic:
hP

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
⊢ Submodule.IsPrincipal P
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
⊢ m ≤ n

Tactic:
have v_π_lt_one := (intValuation_lt_one_iff_dvd (maximalIdeal A) π).mpr
          (dvd_of_eq ((irreducible_iff_uniformizer _).mp hπ))

Goal state after:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
H : (maximalIdeal A).intValuation π ^ n / (maximalIdeal A).intValuation π ^ m ≤ 1
v_π_lt_one : (maximalIdeal A).intValuation π < 1
⊢ m ≤ n
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x y : K
γ : Γ₀ˣ
y_ne : y ≠ 0
h : v (x - y) < min (↑γ * (v y * v y)) (v y)
hyp1 : v (x - y) < ↑γ * (v y * v y)
hyp1' : v (x - y) * (v y * v y)⁻¹ < ↑γ
hyp2 : v (x - y) < v y
key : v x = v y
x_ne : x ≠ 0
decomp : x⁻¹ - y⁻¹ = x⁻¹ * (y - x) * y⁻¹
⊢ v (y - x) * (v y * v y)⁻¹ = v (x - y) * (v y * v y)⁻¹

Tactic:
rw [Valuation.map_sub_swap]

Goal state after:
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case refine_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
h : x ∈ IsUnit.submonoid A
⊢ (valuation K (maximalIdeal A)) ((algebraMap A K) x) = 1

Tactic:
simpa [IsDiscreteValuationRing.maximalIdeal] using! h

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero G
inst✝ : MulArchimedean G
a : G
ha : a < 1
b : Gˣ
ha' : a ≠ 0
⊢ ∃ n, a ^ n < ↑b

Tactic:
· lift a to Gˣ using IsUnit.mk0 _ ha'
    simpa using! exists_pow_lt ha b

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
f : G₀ ≃*o WithZero (Multiplicative ℤ)
⊢ ∀ {a b : G₀ˣ},
    (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun a ≤
        (MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans ↑f)).toFun b ↔
      a ≤ b

Tactic:
intros
      rw [← WithZero.coe_le_coe]
      simp

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ (a : G₀),
    g ≤ a →
      ¬a = 0 →
        ∀ (b : G₀),
          g ≤ b → ¬b = 0 → a < b → (if h : a = 0 then 1 else Units.mk0 a h) < if h : b = 0 then 1 else Units.mk0 b h

Tactic:
intro _

Goal state after:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝ : G₀
⊢ g ≤ a✝ →
    ¬a✝ = 0 →
      ∀ (b : G₀),
        g ≤ b → ¬b = 0 → a✝ < b → (if h : a✝ = 0 then 1 else Units.mk0 a✝ h) < if h : b = 0 then 1 else Units.mk0 b h
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean (WithZero α) → MulArchimedean α

Tactic:
intro _

Goal state after:
case mp
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
a✝ : MulArchimedean (WithZero α)
⊢ MulArchimedean α
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
⊢ MulArchimedean α → MulArchimedean (WithZero α)

Tactic:
intro _

Goal state after:
case mpr
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : PartialOrder α
a✝ : MulArchimedean α
⊢ MulArchimedean (WithZero α)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ˣ → MulArchimedean G₀

Tactic:
intro _

Goal state after:
case mp
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
a✝ : MulArchimedean G₀ˣ
⊢ MulArchimedean G₀
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
⊢ MulArchimedean G₀ → MulArchimedean G₀ˣ

Tactic:
intro _

Goal state after:
case mpr
G₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero G₀
a✝ : MulArchimedean G₀
⊢ MulArchimedean G₀ˣ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ (MvPowerSeries.coeff n) φ = (MvPowerSeries.coeff n) ψ

Tactic:
← coeff_def

Goal state after:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ (coeff ?m.21) φ = (coeff ?m.21) ψ

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ n () = ?m.21

R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : ∀ (n : ℕ), (coeff n) φ = (coeff n) ψ
n : Unit →₀ ℕ
⊢ ℕ
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff (n + 1)) φ = (coeff (n + 1)) ((X * mk fun p ↦ (coeff (p + 1)) φ) + C (constantCoeff φ))

Tactic:
simp only [coeff_succ_X_mul, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

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

Goal state before:
pp: S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(map f)

Tactic:
by
  intro g
  use PowerSeries.mk fun k ↦ Function.surjInv hf (PowerSeries.coeff k g)
  ext k
  simp only [Function.surjInv, coeff_map, coeff_mk]
  exact Classical.choose_spec (hf (coeff k g))

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ exp
      (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors +
            (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)) =
    exp
      (-(↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors) +
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))

Tactic:
Nat.cast_add

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
⊢ exp
      (-(↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors) +
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))) =
    exp
      (-(↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors) +
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)))
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
h : single s 1 ≤ 0
⊢ False

Tactic:
by simpa using h s

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

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
t : σ
hst : s = t
⊢ (m - single s n + single s n) t = m t

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
t : σ
hst : ¬s = t
⊢ (m - single s n + single s n) t = m t

Tactic:
· subst t
          simpa using! tsub_add_cancel_of_le H

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : n ≤ m s
t : σ
hst : ¬s = t
⊢ (m - single s n + single s n) t = m t
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff d) f ≠ 0 ∧ (weight w) d = n

Tactic:
by
  simpa using ne_zero_iff_exists_coeff_ne_zero f

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ Function.Injective toMvPowerSeries

Tactic:
by
  intro x y h
  ext
  simp_rw [← coeff_coe, h]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
f✝ : ι →₀ α
i✝ : ι
a : α
f : ι →₀ α
i : ι
⊢ i ∈ f.support ↔ {f i} ≠ 0

Tactic:
rw [← not_iff_not, notMem_support_iff, not_ne_iff]
    exact singleton_injective.eq_iff.symm

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ ↑((weight w) i + (weight w) j) = ↑((weight w) i) + ↑((weight w) j)

Tactic:
Nat.cast_add

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w f + weightedOrder w g
i j : σ →₀ ℕ
hi : weightedOrder w f ≤ ↑((weight w) i)
hj : weightedOrder w g ≤ ↑((weight w) j)
hij : i + j = d
⊢ ↑((weight w) i) + ↑((weight w) j) = ↑((weight w) i) + ↑((weight w) j)
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: x✝ : ℕ∞ × ℕ∞
a✝ b : ℕ∞
a : ℕ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a, ⊤)

Tactic:
exact tendsto_nhds_top_mono' continuousAt_snd fun p ↦ le_add_left le_rfl

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ + (coeff i) ψ ≠ 0

Tactic:
coeff_of_lt_order i H,

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ + 0 ≠ 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: 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
a : ↥(adicCompletionIntegers K v)
⊢ IsUnit a ↔ Valued.v ↑a = 1

Tactic:
simp [Valuation.Integers.isUnit_iff_valuation_eq_one (integers K v)]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
⊢ ∀ x ∈ range (n + 1), G (((trunc (n + 1)) f).coeff x) * s ^ x = G ((coeff x) f) * s ^ x

Tactic:
intro _

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
x✝ : ℕ
⊢ x✝ ∈ range (n + 1) → G (((trunc (n + 1)) f).coeff x✝) * s ^ x✝ = G ((coeff x✝) f) * s ^ x✝
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ (coeff m) (↑((trunc n) f) * g) = (coeff m) (f * g)

Tactic:
rw [coeff_mul, coeff_mul, sum_congr rfl]

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ∀ x ∈ antidiagonal m, (coeff x.1) ↑((trunc n) f) * (coeff x.2) g = (coeff x.1) f * (coeff x.2) g
Module: Mathlib.RingTheory.PowerSeries.Trunc

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ ∀ x ∈ antidiagonal m, (coeff x.1) ↑((trunc n) f) * (coeff x.2) g = (coeff x.1) f * (coeff x.2) g

Tactic:
intro _

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x✝ : ℕ × ℕ
⊢ x✝ ∈ antidiagonal m → (coeff x✝.1) ↑((trunc n) f) * (coeff x✝.2) g = (coeff x✝.1) f * (coeff x✝.2) g
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.order = 1

Tactic:
by
  simpa only [Nat.cast_one] using! order_monomial_of_ne_zero 1 (1 : R) one_ne_zero

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ ↑φ.order.toNat + ψ.order

Tactic:
← coe_toNat_order h.2,

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (φ * ψ).order ≤ ↑φ.order.toNat + ↑ψ.order.toNat
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d

Tactic:
classical
  constructor
  · simp only [basis, TwoSidedIdeal.le_iff, TwoSidedIdeal.coe_mk', ofPred_subset_ofPred]
    intro h
    constructor
    · intro x hx
      have (d' : _) : coeff d' (C (σ := σ) x) ∈ J := by
        rw [coeff_C]; split_ifs <;> [exact hx; exact J.zero_mem]
      simpa using h (C x) (fun _ _ ↦ this _) _ zero_le
    · by_contra h'
      apply hK
      rw [eq_top_iff]
      intro x _
      have (d') (hd'_le : d' ≤ d) : coeff d' (monomial e x) ∈ J := by
        rw [coeff_monomial]
        split_ifs with hd' <;> [exact (h' (hd' ▸ hd'_le)).elim; exact J.zero_mem]
      simpa using h (monomial e x) this _ le_rfl
  · rintro ⟨hJK, hed⟩
    exact basis_le hJK hed

Goal state after:
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
f : Polynomial R
⊢ MvPowerSeries.eval₂ φ (fun x ↦ a)
      ↑((MvPolynomial.uniqueAlgEquiv R Unit) ((MvPolynomial.uniqueAlgEquiv R Unit).symm f)) =
    MvPolynomial.eval₂ φ (fun x ↦ a) ((MvPolynomial.uniqueAlgEquiv R Unit).symm f)

Tactic:
← MvPolynomial.toMvPowerSeries_pUnitAlgEquiv,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
φ : R →+* S
a : S
inst✝¹ : UniformSpace R
inst✝ : UniformSpace S
f : Polynomial R
⊢ MvPowerSeries.eval₂ φ (fun x ↦ a) ↑((MvPolynomial.uniqueAlgEquiv R Unit).symm f) =
    MvPolynomial.eval₂ φ (fun x ↦ a) ((MvPolynomial.uniqueAlgEquiv R Unit).symm f)
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ lift.{v, u_1} 𝔠 = 𝔠

Tactic:
← two_power_aleph0,

Goal state after:
⊢ lift.{v, u_1} (2 ^ ℵ₀) = 𝔠
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: ⊢ 𝔠 ^ ℵ₀ = 𝔠

Tactic:
← two_power_aleph0,

Goal state after:
⊢ (2 ^ ℵ₀) ^ ℵ₀ = 2 ^ ℵ₀
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case true
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ ¬cantorFunction c f = cantorFunction c g

Tactic:
· apply _root_.ne_of_gt
      refine increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) ?_ fn
      apply Bool.eq_false_of_not_eq_true
      rw [← fn]
      apply Ne.symm
      exact Nat.find_spec this

Goal state after: