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

Goal state before:
pp: case inr
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
this : ∃ V' ∈ 𝓝 1, 0 ∉ V' ∧ ∀ x ∈ V', ∀ y ∈ V', x * y⁻¹ ∈ V
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)

Tactic:
rcases this with ⟨V', V'_in, zeroV', hV'⟩

Goal state after:
case inr
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
⊢ ∃ c, Tendsto (⇑v.restrict) (Filter.comap Completion.coe' (𝓝 x₀)) (𝓝 c)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₁
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₁ ∈ (valuation R K).integer

Tactic:
simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]

Goal state after:
case h.h₁
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 : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ a⁻¹ * W.a₁ ∈ (valuation R K).integer
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₂
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₂ ∈ (valuation R K).integer

Tactic:
simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]

Goal state after:
case h.h₂
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 : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (a ^ 2)⁻¹ * W.a₂ ∈ (valuation R K).integer
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₃
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₃ ∈ (valuation R K).integer

Tactic:
simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]

Goal state after:
case h.h₃
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 : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (a ^ 3)⁻¹ * W.a₃ ∈ (valuation R K).integer
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₄
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₄ ∈ (valuation R K).integer

Tactic:
simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]

Goal state after:
case h.h₄
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 : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (a ^ 4)⁻¹ * W.a₄ ∈ (valuation R K).integer
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₆
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 := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ ({ u := Units.mk0 a ha₀, r := 0, s := 0, t := 0 } • W).a₆ ∈ (valuation R K).integer

Tactic:
simp only [variableChange_def, Units.val_inv_eq_inv_val, Units.val_mk0, mul_zero, add_zero,
        inv_pow, zero_mul, sub_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]

Goal state after:
case h.h₆
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 : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ (a ^ 6)⁻¹ * W.a₆ ∈ (valuation R K).integer
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
inst✝ : DecidableEq σ
⊢ (coeff n) (φ * ψ) = ∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ

Tactic:
refine Finset.sum_congr ?_ fun _ _ => rfl
  rw [Subsingleton.elim (Classical.decEq σ) ‹DecidableEq σ›]

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

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

Tactic:
have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
this : ∀ p ∈ antidiagonal m, (coeff p.1) ((monomial n) a) * (coeff p.2) φ ≠ 0 → p.1 = n
⊢ (coeff m) ((monomial n) a * φ) = if n ≤ m then a * (coeff (m - n)) φ else 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff d) f ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑((weight w) d)

Tactic:
simp only [ne_eq, Nat.cast_le, Nat.find_le_iff]
    exact ⟨weight w d, le_rfl, d, h, rfl⟩

Goal state after:
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
a : A
f : MvPowerSeries σ R
⊢ a • f = (algebraMap A R) a • f

Tactic:
IsScalarTower.algebraMap_smul

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
e : σ →₀ ℕ
a✝ : σ → A
a : A
f : MvPowerSeries σ R
⊢ a • f = a • f
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg.right.hnc
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
hb : (weight w) b < (weight w) b
⊢ False

Tactic:
exact hb.false

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ weightedOrder w ((monomial d) a) = if a = 0 then ⊤ else ↑((weight w) d)

Tactic:
split_ifs with h
  · rw [h, weightedOrder_eq_top_iff, map_zero]
  · rw [weightedOrder_eq_nat]
    constructor
    · use d
      simp only [coeff_monomial_same, ne_eq, h, not_false_eq_true, and_self]
    · intro b hb
      rw [coeff_monomial, if_neg]
      rintro rfl
      exact hb.false

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : ι →₀ α
t : ι → Finset α
h : f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
i : ι
⊢ ({ toFun := indicator s, inj' := ⋯ } fun i x ↦ f i) i = f i

Tactic:
exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι →₀ Finset α
⊢ #f.pi = f.prod fun i ↦ ↑(#(f i))

Tactic:
rw [pi, card_finsupp]
  exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : Finset (σ →₀ ℕ)
p : MvPowerSeries σ R
⊢ ((truncFinset R s) p).totalDegree ≤ s.sup ⇑degree

Tactic:
by
  simpa [MvPolynomial.totalDegree] using! sup_mono (support_truncFinset_subset p)

Goal state after:
Module: Mathlib.Topology.Instances.ENat

Goal state before:
pp: n : ℕ
⊢ 𝓝 ↑n = pure ↑n

Tactic:
simp [nhds_natCast]

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

Goal state before:
pp: case pos.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.1 = p ∧ (weight w) x.2 = q
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0

Tactic:
rw [if_pos h.1, if_pos h.2]

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

Goal state before:
pp: 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
inst✝ : Algebra S K
r : S
x : WithVal (valuation K v)
⊢ { toCompletion := ↑(r • x) } = r • { toCompletion := ↑x }

Tactic:
by
  apply adicCompletion.ext
  exact UniformSpace.Completion.coe_smul r x

Goal state after:
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
r : R
⊢ Valued.v ↑r = (valuation K v) ↑r

Tactic:
← adicCompletion.valued_toCompletion

Goal state after:
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
r : R
⊢ Valued.v (↑r).toCompletion = (valuation K v) ↑r
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
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) } = (valuation K v) k

Tactic:
← adicCompletion.valued_toCompletion

Goal state after:
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
k : K
⊢ Valued.v { toCompletion := ↑((WithVal.equiv (valuation K v)).symm k) }.toCompletion = (valuation K v) k
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
← hi

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) (φ + ψ) ≠ 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

Tactic:
first | rfl | try simp_all

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

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

Tactic:
first | rfl | try simp_all

Goal state after:
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
⊢ 0 = a

Tactic:
first | rfl | try simp_all

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

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

Tactic:
first | rfl | try simp_all

Goal state after:
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
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
⊢ r' • i ∈ A

Tactic:
by
    refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
    case base => exact AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx
    case zero => simp_rw [smul_zero]; exact zero_mem _
    case add => simp_rw [smul_add]; exact add_mem hx hy
    case neg => simp_rw [smul_neg]; exact neg_mem hx

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 : ℚ
⊢ (valuation ℚ 𝔭) x ≤ 1 ↔ ↑x.den ∉ 𝔭.asIdeal

Tactic:
have : CharZero R := ⟨.of_comp (f := algebraMap R ℚ) (by simpa using Nat.cast_injective)⟩

Goal state after:
R : Type u_4
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
inst✝¹ : Algebra R ℚ
inst✝ : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
this : CharZero R
⊢ (valuation ℚ 𝔭) x ≤ 1 ↔ ↑x.den ∉ 𝔭.asIdeal
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
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
⊢ (eval₂ (algebraMap R S) fun s ↦ ε.toRingHom (X s)) = ⇑ε

Tactic:
refine (eval₂_unique (continuous_algebraMap R S) (HasEval.X.map hε) hε ?_).symm

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
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
⊢ ∀ (p : MvPolynomial σ R), ε ↑p = MvPolynomial.eval₂ (algebraMap R S) (fun s ↦ ε.toRingHom (X s)) p
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ subst = eval₂ (algebraMap R (MvPowerSeries τ S))

Tactic:
ext; simp +instances [subst, DiscreteUniformity.eq_bot]

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
⊢ cantorFunction c f < cantorFunction c g

Tactic:
have h3 : c < 1 := by
    apply h2.trans
    norm_num

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
h3 : c < 1
⊢ cantorFunction c f < cantorFunction c g
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
h3 : c < 1
⊢ cantorFunction c f < cantorFunction c g

Tactic:
induction n generalizing f g with

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case false
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 = false
⊢ ¬cantorFunction c f = cantorFunction c g

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_lt
      refine increasing_cantorFunction h1 h2 hn fn ?_
      apply Bool.eq_true_of_not_eq_false
      rw [← fn]
      apply Ne.symm
      exact Nat.find_spec this

Goal state after:
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
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n : ℕ
⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, (coeff n') (f ^ m) = 0

Tactic:
obtain ⟨k, hk⟩ := id hf

Goal state after:
A : Type u_1
inst✝ : CommRing A
f : A⟦X⟧
hf : HasSubst f
n k : ℕ
hk : MvPowerSeries.constantCoeff f ^ k = 0
⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, (coeff n') (f ^ m) = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos.succ
R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
j n✝ : ℕ
hmn : (p ^ (n✝ + 1)).Coprime (p ^ j)
⊢ ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ (n✝ + 1) * p ^ j) =
    ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ (n✝ + 1)) *
      ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ j)

Tactic:
cases j
        · simp [hk.ne', hf]
        · simp [hp.ne_one] at hmn

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
σ : Type u_7
inst✝ : DecidableEq σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ (MvPowerSeries.coeff e) (subst (MvPowerSeries.X s) f) = if e = Finsupp.single s (e s) then (coeff (e s)) f else 0

Tactic:
rw [coeff_subst (HasSubst.X s), finsum_eq_single _ (e s)] <;>
  grind [MvPowerSeries.coeff_X_pow, smul_eq_mul]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ ‖f n‖ / ↑n ^ (x - 1) ≤ C'

Tactic:
refine (le_max' _ _ <| mem_insert_of_mem ?_).trans <| le_max_right ..

Goal state after:
case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
h : f =O[atTop] fun n ↦ ↑n ^ (x - 1)
C : ℝ
hC : ∀ᶠ (x_1 : ℕ) in atTop, ‖f x_1‖ ≤ C * ‖↑x_1 ^ (x - 1)‖
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ‖f b‖ ≤ C * ‖↑b ^ (x - 1)‖
C' : ℝ := max C ((insert 0 (image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m))).max' ⋯)
hC'₀ : 0 ≤ C'
hCC' : C ≤ C'
n : ℕ
hn₀ : n ≠ 0
hn : n < m
hn' : 0 < n
⊢ ‖f n‖ / ↑n ^ (x - 1) ∈ image (fun n ↦ ‖f n‖ / ↑n ^ (x - 1)) (range m)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
i : ι
w : Finset ι
hi : i ∉ w
hw' : (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
hw : ∀ i_1 ∈ insert i w, i_1 ∈ s
k : ℕ
hk : k ≤ n
j : ℕ × ℕ
hj : j ∈ k.divisorsAntidiagonal
h1 : (f i) j.1 = 1 j.1
h2 : (∏ x ∈ w, f x) j.2 = 1 j.2
⊢ 1 j.1 * (∏ x ∈ w, f x) j.2 = 1 j.1 * 1 j.2

Tactic:
h2

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
i : ι
w : Finset ι
hi : i ∉ w
hw' : (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
hw : ∀ i_1 ∈ insert i w, i_1 ∈ s
k : ℕ
hk : k ≤ n
j : ℕ × ℕ
hj : j ∈ k.divisorsAntidiagonal
h1 : (f i) j.1 = 1 j.1
h2 : (∏ x ∈ w, f x) j.2 = 1 j.2
⊢ 1 j.1 * 1 j.2 = 1 j.1 * 1 j.2