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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : BR.SubmodulesBasis B
x✝ : TopologicalSpace R := BR.topology
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i

Tactic:
let := BR.topology
      intro m i
      rcases hB.smul m i with ⟨V, V_in, hV⟩
      exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV

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

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ y * ↑s * ↑v * ↑u ≤ᵥ 0 * (↑s * ↑v)

Tactic:
apply (mul_vle_mul_left (mul_vle_mul_left h₂ v) u).trans

Goal state after:
case pos.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ x * ↑t * ↑v * ↑u ≤ᵥ 0 * (↑s * ↑v)
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (𝓤 R).HasBasis (fun x ↦ True) fun γ ↦ {p | v.restrict (p.2 - p.1) < ↑γ}

Tactic:
by
  rw [uniformity_eq_comap_nhds_zero]
  exact (hasBasis_nhds_zero R Γ₀).comap _

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
γ : Γ₀
hγ : γ ≠ 0
x : Γ₀
hx : x ∈ Iio (γ / y)
⊢ ((fun p ↦ p.1 * p.2) ∘ fun a ↦ (a, y)) x ∈ Iio γ

Tactic:
calc x * y < γ / y * y := mul_lt_mul_of_pos_right hx (zero_lt_iff.2 hy)
      _ = γ := div_mul_cancel₀ _ hy

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addX P Q = ((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)) ^ 2

Tactic:
div_pow,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addX P Q = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 / (P z * Q z) ^ 2
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
⊢ x ∈ {x | v.restrict x = r} ↔ x ∈ {x | v.restrict x ≤ r} \ {x | v.restrict x < r}

Tactic:
simp [← le_antisymm_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
r : (ofClass v).ValueGroup₀
hr : r ≠ 0
x : R
⊢ x ∈ {x | v.restrict x = r} ↔ x ∈ {x | v.restrict x ≤ r} \ {x | v.restrict x < r}

Tactic:
simp [← le_antisymm_iff]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = ((P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)) ^ 3

Tactic:
div_pow,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.negAddY P Q = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3 / (P z * Q z) ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
rw [addY, negY_eq, addX_self hP, negAddY_self, addZ_self]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -0 - W'.a₁ * 0 * 0 - W'.a₃ * 0 ^ 3 = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addY P Q = (-(P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z)) ^ 3

Tactic:
div_pow,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W.addY P Q = (-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 / (P z * Q z) ^ 3
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case h.e_a.e_a
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
h_mn : m ≤ n
⊢ (algebraMap A K) π ^ (n - m) = (algebraMap A K) π ^ n * ((algebraMap A K) π ^ m)⁻¹

Tactic:
rw [pow_sub₀ _ _ h_mn]

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
h_mn : m ≤ n
⊢ (algebraMap A K) π ≠ 0
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ ¬∃ x y, x < y

Tactic:
suffices DenselyOrdered (WithBot.some ⁻¹' s) by
    rintro ⟨x, y, H⟩
    rw [_root_.denselyOrdered_set_iff_subsingleton] at this
    obtain ⟨z, hz, hz'⟩ := exists_between H
    have hz0 : (⊥ : WithBot X) < z := by simp [(Subtype.coe_lt_coe.mpr hz).trans_le']
    replace hz' : WithBot.unbot z.val hz0.ne' < WithBot.unbot y (hz0.trans hz').ne' := by
      rwa [← WithBot.coe_lt_coe, WithBot.coe_unbot, WithBot.coe_unbot]
    refine absurd (this ?_ ?_) hz'.ne <;>
    simp

Goal state after:
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
⊢ DenselyOrdered ↑(some ⁻¹' s)
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ 1 ≤ a⁻¹

Tactic:
simpa using le_of_not_ge ha

Goal state after:
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:
by
  rw [← denselyOrdered_units_iff,
      ← LinearOrderedCommGroup.discrete_iff_not_denselyOrdered]
  refine Nonempty.congr ?_ ?_ <;> intro f
  · refine ⟨MulEquiv.withZero.symm (withZeroUnitsEquiv.trans f), ?_⟩
    intros
    simp only [MulEquiv.withZero, withZeroUnitsEquiv, MulEquiv.trans_apply,
      MulEquiv.coe_mk, Equiv.coe_fn_mk, recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv,
      MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, map_eq_zero, coe_ne_zero,
      ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]
    rw [← Units.val_le_val, ← map_le_map_iff f, ← coe_le_coe, coe_unzero, coe_unzero]
  · refine ⟨withZeroUnitsEquiv.symm.trans (MulEquiv.withZero f), ?_⟩
    intros
    simp only [withZeroUnitsEquiv, MulEquiv.symm_mk, MulEquiv.withZero,
      MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
      MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]
    split_ifs <;>
    simp_all [← Units.val_le_val]

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

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

Tactic:
simp only [coeff_mul_monomial, coeff_monomial]

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
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.Injective ⇑f
⊢ Function.Injective ⇑(map f)

Tactic:
intro u v huv
  ext k
  apply hf
  rw [← PowerSeries.coeff_map, ← PowerSeries.coeff_map, huv]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : IsEmpty σ
p : MvPowerSeries σ R
⊢ C (p 0) = p

Tactic:
ext n; simpa [coeff_C, Subsingleton.eq_zero n] using! coeff_apply _ _

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 : m - single s n + single s n = m
⊢ (coeff m) φ = (coeff m) (X s ^ n * fun m ↦ (coeff (m + single s n)) φ)

Tactic:
rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
      · rw [coeff_X_pow, if_pos rfl, one_mul]
        simpa using! congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm
      · rintro ⟨i, j⟩ hij hne
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]
        · exact zero_mul _
      · intro hni
        exfalso
        apply hni
        rwa [mem_antidiagonal, add_comm]

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

Goal state before:
pp: σ✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
σ : MvPowerSeries σ✝ A
n : σ✝ →₀ ℕ
⊢ (coeff n) (a • σ) = (coeff n) (((map (algebraMap R A)).comp C) a * σ)

Tactic:
simp [(coeff A n).map_smul_of_tower a, Algebra.smul_def]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
⊢ MvPolynomial.coeff x ((truncFinset R s) f * (truncFinset R t) g) = (coeff x) (f * g)

Tactic:
by
  classical
  simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
  apply sum_congr rfl
  rintro ⟨i, j⟩ hij
  simp only [mem_antidiagonal] at hij
  rw [coeff_truncFinset_of_mem _ (hs (show i ≤ x by simp [← hij]) hxs),
    coeff_truncFinset_of_mem _ (ht (show j ≤ x by simp [← hij]) hxt)]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
f' : MvPowerSeries σ R
⊢ (coeff n) f' = MvPolynomial.coeff n ((trunc' R n) f')

Tactic:
rw [coeff_trunc', if_pos le_rfl]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
hf : constantCoeff f = 0
⊢ ↑n ≤ n • f.order

Tactic:
simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)

Goal state after:
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
d : σ →₀ ℕ
hd : ¬(coeff d) f = 0 ∧ (weight w) d = p
⊢ (coeff d) f = 0

Tactic:
rw [MvPowerSeries.ext_iff] at hf'

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
p : ℕ
hf : ↑p = weightedOrder w f
hf' : ∀ (n : σ →₀ ℕ), (coeff n) ((weightedHomogeneousComponent w p) f) = (coeff n) 0
d : σ →₀ ℕ
hd : ¬(coeff d) f = 0 ∧ (weight w) d = p
⊢ (coeff d) f = 0
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
f : MvPowerSeries σ R
h : constantCoeff f = 0
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑m ≤ m • f.order

Tactic:
simpa [nsmul_eq_mul] using ENat.self_le_mul_right m (order_ne_zero_iff_constCoeff_eq_zero.mpr h)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hf : constantCoeff φ = 0
⊢ ↑n ≤ n • φ.order

Tactic:
simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
f : R⟦X⟧
⊢ (trunc n) (C r * f) = Polynomial.C r * (trunc n) f

Tactic:
by
  ext i; simp [coeff_trunc]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
r : R
⊢ (trunc n) (f * C r) = (trunc n) f * Polynomial.C r

Tactic:
by
  ext i; simp [coeff_trunc]

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

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

pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : ¬d < n
⊢ 0 = 0

Tactic:
· rw [coeff_trunc, if_pos <| lt_of_lt_of_le h hnm]

Goal state after:
case neg
R : Type u_2
inst✝ : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : ¬d < n
⊢ 0 = 0
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case e'_4
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunction c g_min = 1

Tactic:
refine (tsum_eq_single 0 ?_).trans ?_

Goal state after:
case e'_4.refine_1
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ∀ (b' : ℕ), b' ≠ 0 → cantorFunctionAux c g_min b' = 0

case e'_4.refine_2
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunctionAux c g_min 0 = 1
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ (Function.support fun d ↦ (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)) =
    ⇑(Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv ''
      Function.support fun d ↦ (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (d.prod fun s e ↦ a ^ e)

Tactic:
← Equiv.preimage_eq_iff_eq_image,

Goal state after:
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f : R⟦X⟧
e : τ →₀ ℕ
⊢ (⇑(Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv ⁻¹'
      Function.support fun d ↦ (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)) =
    Function.support fun d ↦ (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (d.prod fun s e ↦ a ^ e)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Finsupp.degree d = 1
f : R⟦X⟧
⊢ subst p ((rescale a) f) = (MvPowerSeries.rescale (Function.const σ a)) (subst p f)

Tactic:
by
  have hp : PowerSeries.HasSubst p := by
    apply HasSubst.of_constantCoeff_zero
    rw [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_apply]
    have : (p 0 ≠ 0) → (0 : σ →₀ ℕ).degree = 1 := hp_lin 0
    grind
  rw [rescale_eq_subst, MvPowerSeries.rescale_eq_subst,
    subst_comp_subst_apply (HasSubst.smul_X' a) hp]
  nth_rewrite 3 [subst]
  rw [MvPowerSeries.subst_comp_subst_apply hp.const (MvPowerSeries.HasSubst.smul_X _),
    MvPowerSeries.ext_iff]
  intro _
  rw [subst_smul hp, ← Polynomial.coe_X, subst_coe hp, Polynomial.aeval_X,
    ← MvPowerSeries.rescale_eq_subst, MvPowerSeries.rescale_homogeneous_eq_smul hp_lin,
    subst, pow_one]

Goal state after:
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
this : ∀ (w : Finset ι), (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
k : ℕ
hk : k ≤ n
⊢ 1 k = (∏ x ∈ v \ t, f x) k

Tactic:
this (v \ t) hv k hk

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
this : ∀ (w : Finset ι), (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
k : ℕ
hk : k ≤ n
⊢ 1 k = 1 k
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun n ↦ c n • d n) (l ⊓ 𝓟 {y | x + d y ∈ s}) (map (fun p ↦ p.1 • p.2) (⊤ ×ˢ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' s] 0))

Tactic:
refine tendsto_map.comp (tendsto_top.prodMk (tendsto_nhdsWithin_iff.mpr ⟨?_, ?_⟩))

Goal state after:
case refine_1
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto d (l ⊓ 𝓟 {y | x + d y ∈ s}) (𝓝 0)

case refine_2
R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
α : Type u_1
l : Filter α
c : α → R
d : α → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∃ᶠ (n : α) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : α) in l ⊓ 𝓟 {y | x + d y ∈ s}, d n ∈ (fun x_1 ↦ x + x_1) ⁻¹' s
Module: Mathlib.Analysis.Calculus.FDeriv.Congr

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Tactic:
by
  classical
  simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff hx]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
hf : Injective ⇑(fderiv 𝕜 f x)
⊢ DifferentiableAt 𝕜 f x

Tactic:
by
  simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢
  exact differentiableWithinAt_of_fderivWithin_injective hf

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : (𝓝 0).HasBasis pE sE
hF : (𝓝 0).HasBasis pF sF
⊢ f =O[𝕜; l] g ↔ ∀ (i : ιE), pE i → ∃ j, pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)

Tactic:
by
  rw [isBigOTVS_iff]
  refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_iff ?_
  · rintro s t hsub ⟨V, hV₀, hV⟩
    exact ⟨V, hV₀, hV.mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩
  · exact fun s t hsub h ↦ h.mono fun x hx ↦ hx.trans <| egauge_anti 𝕜 hsub (g x)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
g : α → F
l : Filter α
⊢ 0 =o[𝕜; l] g

Tactic:
refine ⟨fun U hU ↦ ?_⟩
  use univ
  simp [egauge_zero_right _ (Filter.nonempty_of_mem hU), EventuallyLE]

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n)‖ = ‖p.coeff n‖

Tactic:
ContinuousMultilinearMap.norm_mkPiRing

Goal state after:
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ ‖p.coeff n‖ = ‖p.coeff n‖