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

Goal state before:
pp: α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : IsUniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : IsUniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
a : α
⊢ (extensionHom f hf) ↑a = f a

Tactic:
simp only [Completion.extensionHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    UniformSpace.Completion.extension_coe <| uniformContinuous_addMonoidHom_of_continuous hf]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.negAddY P P = 0

Tactic:
by
  rw [negAddY]
  ring1

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

Goal state before:
pp: K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
have : NeBot F := cau_F.1

Goal state after:
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : IsTopologicalDivisionRing L
inst✝¹ : T0Space L
inst✝ : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
⊢ Cauchy (map (fun x ↦ x⁻¹) F)
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
g : Γˣ := Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hγ0 : ↑g ∉ {0}
π : K
hπ : v π = ↑g
⊢ ↑(Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup) = ↑(generator v)

Tactic:
valueGroup_genLTOne_eq_generator

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
g : Γˣ := Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hg : g = Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup
hγ0 : ↑g ∉ {0}
π : K
hπ : v π = ↑g
⊢ ↑(generator v) = ↑(generator v)
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✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
h : ∀ {a : ↥v.valuationSubring}, a ≠ 0 → ∃ b, a * b = 1
⊢ False

Tactic:
have := hπ.ne_zero

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
h : ∀ {a : ↥v.valuationSubring}, a ≠ 0 → ∃ b, a * b = 1
this : ↑π ≠ 0
⊢ False
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: case hp
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 : ∀ (x : UniformSpace.Completion (WithVal v)), Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1
⊢ IsClosed {a | Valued.v a ≤ 1 ↔ Valued.v ((mapEquiv h.uniformEquiv) a) ≤ 1}

Tactic:
h1

Goal state after:
case hp
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 : ∀ (x : UniformSpace.Completion (WithVal v)), Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1
⊢ IsClosed {a | Valued.v.restrict a ≤ 1 ↔ Valued.v ((mapEquiv h.uniformEquiv) a) ≤ 1}
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 1
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
r : Function.RightInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
c : Continuous fun x ↦ x * x₀⁻¹
⊢ (fun x ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀

Tactic:
← mul_inv_cancel₀ h

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x₀ : hat K
h : x₀ ≠ 0
preimage_one : ⇑v ⁻¹' {1} ∈ 𝓝 1
V : Set (hat K)
V_in : V ∈ 𝓝 1
hV : ∀ (x : K), ↑x ∈ V → v x = 1
V' : Set (hat K)
V'_in : V' ∈ 𝓝 (x₀ * x₀⁻¹)
zeroV' : 0 ∉ V'
hV' : ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
l : Function.LeftInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
r : Function.RightInverse (fun x ↦ x * x₀⁻¹) fun x ↦ x * x₀
c : Continuous fun x ↦ x * x₀⁻¹
⊢ (fun x ↦ x * x₀⁻¹) ⁻¹' V' ∈ 𝓝 x₀
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered G

Tactic:
rw [← denselyOrdered_units_iff]

Goal state after:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ∨ DenselyOrdered Gˣ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
⊢ (map' ↑↑f) (if h : a✝ = 0 then 0 else ↑(Units.mk0 a✝ h)) ≤ (map' ↑↑f) (if h : b✝ = 0 then 0 else ↑(Units.mk0 b✝ h)) ↔
    a✝ ≤ b✝

Tactic:
split_ifs

Goal state after:
case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) 0 ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝

case pos
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) 0 ↔ a✝ ≤ b✝

case neg
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
h✝¹ : ¬a✝ = 0
h✝ : ¬b✝ = 0
⊢ (map' ↑↑f) ↑(Units.mk0 a✝ h✝¹) ≤ (map' ↑↑f) ↑(Units.mk0 b✝ h✝) ↔ a✝ ≤ b✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
⊢ ∃ a, (valuation R K) a = lmax

Tactic:
let i : ℕ := l.idxOf lmax

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
i : ℕ := List.idxOf lmax l
⊢ ∃ a, (valuation R K) a = lmax
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n) ((monomial n) a) = a

Tactic:
rw [monomial_def]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
a : R
⊢ (coeff n) ((LinearMap.single R (fun x ↦ R) n) a) = a
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff m) ((monomial n) a) = 0

Tactic:
rw [monomial_def]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff m) ((LinearMap.single R (fun x ↦ R) n) a) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff m) ((LinearMap.single R (fun x ↦ R) n) a) = 0

Tactic:
exact Pi.single_eq_of_ne h _

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

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then (coeff (m - n)) φ * a else 0) = if n ≤ m then a * (coeff (m - n)) φ else 0

Tactic:
split_ifs

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
h✝ : n ≤ m
⊢ (coeff (m - n)) φ * a = a * (coeff (m - n)) φ

case neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute ((coeff m) φ) a
m : σ →₀ ℕ
h✝ : ¬n ≤ m
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ (coeff 0) (X s * φ) = 0

Tactic:
← (φ.commute_X s).eq,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
s : σ
⊢ (coeff 0) (φ * X s) = 0
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 : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (i, j) = (single s n, m - single s n)

Tactic:
rw [← hij, ← hi, Prod.mk_inj]

Goal state after:
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 : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ i = (i, j).1 ∧ j = (i, j).1 + (i, j).2 - (i, j).1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
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 : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : ¬(i, j).1 = single s n
⊢ (0 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
· exact zero_mul _

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

Goal state before:
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 : ¬m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hi : ¬(i, j).1 = single s n
⊢ (0 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
· exact zero_mul _

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

Goal state before:
pp: case empty
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (if d = 0 then 1 else 0) = ↑(#(if d = 0 then {0} else ∅))

Tactic:
split_ifs

Goal state after:
case pos
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : d = 0
⊢ 1 = ↑(#{0})

case neg
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ 0 = ↑(#∅)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ v.intValuation r = exp (-1)

Tactic:
rw [v.intValuation_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hv : v.asIdeal = Ideal.span {r}
⊢ Irreducible (Associates.mk v.asIdeal)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support,
    (a x • MvPowerSeries.X x) ^ e x = (MvPowerSeries.C ((algebraMap A R) (a x)) * MvPowerSeries.X x) ^ e x

Tactic:
· intro x _
    rw [algebra_compatible_smul R, MvPowerSeries.smul_eq_C_mul]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
⊢ Tendsto (fun i ↦ if d = 0 then i else 0) (𝓝 r) (𝓝 (if d = 0 then r else 0))

Tactic:
split_ifs

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : d = 0
⊢ Tendsto (fun i ↦ i) (𝓝 r) (𝓝 r)

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
r : R
d : σ →₀ ℕ
h✝ : ¬d = 0
⊢ Tendsto (fun i ↦ 0) (𝓝 r) (𝓝 0)
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
⊢ (𝓝 0).HasBasis (fun I ↦ ↑I ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I) fun I ↦ ↑I

Tactic:
refine IsLinearTopology.hasBasis_submodule R |>.to_hasBasis (fun I hI ↦ ?_)
    (fun I hI ↦ ⟨{I with smul_mem' := fun r x hx ↦ hI.2.1 r x hx}, hI.1, subset_rfl⟩)

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
⊢ ∃ i', (↑i' ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧ ↑i' ⊆ ↑I
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ φ.order ≤ ↑n

Tactic:
rw [order, dif_neg]
  · simpa using ⟨n, le_rfl, h⟩
  · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
⊢ ↑n ≤ if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : φ = 0
⊢ ↑n ≤ ⊤

case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : ¬φ = 0
⊢ ↑n ≤ ↑(Nat.find ⋯)
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
φ ψ : R⟦X⟧
n : ℕ
h : ↑n < ψ.order
⊢ (coeff n) (φ * (1 - ψ)) = (coeff n) φ

Tactic:
simp [coeff_mul_of_lt_order h, mul_sub]

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

Goal state before:
pp: R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
inst✝¹ : Algebra R ℚ
inst✝ : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
this✝ : CharZero R
this : ↑x.den ≠ 0
⊢ (valuation ℚ 𝔭) x ≤ 1 ↔ ↑x.den ∉ 𝔭.asIdeal

Tactic:
simp [x.num_div_den, ← 𝔭.valuation_div_le_one_iff ℚ x.num this
    (Ideal.IsPrime.notMem_of_isCoprime_of_mem (mod_cast x.isCoprime_num_den.symm.intCast))]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
⊢ IsLinearTopology Rᵐᵒᵖ R

Tactic:
rwa [IsCentralScalar.isLinearTopology_iff]

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

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
⊢ ↑n < if 1 = 0 then ⊤ else ↑(φ.order.toNat + 1)

Tactic:
split_ifs

Goal state after:
case pos
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤

case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case h
σ : 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
I : Ideal S
hI : ↑I ∈ 𝓝 0
n✝ : σ → ℕ := ⋯
s : σ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → a s ^ b ∈ ↑I
⊢ n ∈ {n | a s ^ n.succ ∈ I}

Tactic:
simpa using hn n.succ n.le_succ

Goal state after:
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 ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
⊢ (if d' = 0 then x else 0) ∈ J

Tactic:
split_ifs

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
h✝ : d' = 0
⊢ x ∈ J

case neg
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff e) a ∈ J) → ∀ e_1 ≤ e, (coeff e_1) a ∈ K
x : R
hx : x ∈ ↑J
d' : σ →₀ ℕ
h✝ : ¬d' = 0
⊢ 0 ∈ J
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
⊢ ∀ (i' : TwoSidedIdeal R × (σ →₀ ℕ)),
    ↑i'.1 ∈ 𝓝 0 → ∃ i, (i.1.Finite ∧ ↑i.2 ∈ 𝓝 0) ∧ (i.1.pi fun x ↦ ↑i.2) ⊆ ↑(basis σ R i')

Tactic:
intro ⟨I, d⟩ hI

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : IsLinearTopology R R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
I : TwoSidedIdeal R
d : σ →₀ ℕ
hI : ↑(I, d).1 ∈ 𝓝 0
⊢ ∃ i, (i.1.Finite ∧ ↑i.2 ∈ 𝓝 0) ∧ (i.1.pi fun x ↦ ↑i.2) ⊆ ↑(basis σ R (I, d))
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
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε ↑p = Polynomial.eval₂ φ a p
p : MvPolynomial Unit R
⊢ Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) p) = MvPolynomial.eval₂ φ (fun x ↦ a) p

Tactic:
← MvPolynomial.eval₂_uniqueAlgEquiv

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
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
ε : R⟦X⟧ → S
hε : Continuous ε
h : ∀ (p : Polynomial R), ε ↑p = Polynomial.eval₂ φ a p
p : MvPolynomial Unit R
⊢ Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) p) =
    Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R Unit) p)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

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

Tactic:
split_ifs

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.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunctionAux c f 0 + ∑' (b : ℕ), cantorFunctionAux c f (b + 1) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)

Tactic:
cantorFunctionAux_succ,

Goal state after:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunctionAux c f 0 + ∑' (n : ℕ), c * cantorFunctionAux c (fun n ↦ f (n + 1)) n =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
⊢ #↑(Ioi a) = 𝔠

Tactic:
by
  refine le_antisymm (mk_real ▸ mk_set_le _) ?_
  rw [← not_lt]
  intro h
  refine _root_.ne_of_lt ?_ mk_univ_real
  have hu : Iio a ∪ {a} ∪ Ioi a = Set.univ := by
    convert! @Iic_union_Ioi ℝ _ _
    exact Iio_union_right
  rw [← hu]
  grw [mk_union_le, mk_union_le]
  have h2 : (fun x => a + a - x) '' Ioi a = Iio a := by
    convert! @image_const_sub_Ioi ℝ _ _ _
    simp
  rw [← h2]
  refine add_lt_of_lt (cantor _).le ?_ h
  refine add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) ?_
  rw [mk_singleton]
  exact one_lt_aleph0.trans (cantor _)

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: ⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2

Tactic:
← finrank_eq_rank,

Goal state after:
⊢ Cardinal.lift.{u, 0} ↑(finrank ℝ ℂ) = 2
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
rcases eq_or_ne n 1 with hn' | hn'

Goal state after:
case inr.inl
s : ℂ
n : ℕ
hn : n ≠ 0
hn' : n = 1
⊢ term δ s n = if n = 1 then 1 else 0

case inr.inr
s : ℂ
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
⊢ term δ s n = if n = 1 then 1 else 0