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 β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
⊢ Completion.extension (⇑f) 0 = 0

Tactic:
simp_rw [← coe_zero, extension_coe hf, f.map_zero]

Goal state after:
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 β
hf' : Continuous ⇑↑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ Completion.extension (⇑f) (↑a + ↑b) = Completion.extension ⇑f ↑a + Completion.extension ⇑f ↑b

Tactic:
simp_rw [← coe_add, extension_coe hf, f.map_add]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Ring B
inst✝⁵ : ValuativeRel A
inst✝⁴ : ValuativeRel B
inst✝³ : Algebra A B
inst✝² : ValuativeExtension A B
Γ : Type u_3
inst✝¹ : LinearOrderedCommMonoidWithZero Γ
w : Valuation B Γ
inst✝ : w.Compatible
⊢ (Valuation.comap (algebraMap A B) w).Compatible

Tactic:
constructor
  simp [← vle_iff_vle (A := A) (B := B), Valuation.Compatible.vle_iff_le (v := w)]

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
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ Cauchy (map (fun x ↦ x⁻¹) (map (⇑i) F))

Tactic:
apply CompletableTopField.nice _ F_cau

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
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := ⋯
F_cau : Cauchy (map (⇑i) F)
hi : IsUniformInducing ⇑i
⊢ 𝓝 0 ⊓ map (⇑i) F = ⊥
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f
⊢ Cauchy (map (fun x ↦ x⁻¹) (map (⇑f) F))

Tactic:
apply CompletableTopField.nice _ F_cau

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x ↦ x⁻¹) = (fun x ↦ x⁻¹) ∘ ⇑f
⊢ 𝓝 0 ⊓ map (⇑f) 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 Γ
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
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
⊢ (v ↑r)⁻¹ * v ↑r = 1

Tactic:
inv_mul_cancel₀ hr₀

Goal state after:
Γ : 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
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
⊢ 1 = 1
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
⊢ e 1 = 1 ∨ -e 1 = 1

Tactic:
have he : ¬IsOfFinAddOrder (e 1) :=
    not_isOfFinAddOrder_of_isAddTorsionFree ((AddEquiv.map_ne_zero_iff e).mpr Int.one_ne_zero)

Goal state after:
e : ℤ ≃+ ℤ
he : ¬IsOfFinAddOrder (e 1)
⊢ e 1 = 1 ∨ -e 1 = 1
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
⊢ ∀ (x : G ≃+o ℤ), ¬DenselyOrdered G

Tactic:
intro e

Goal state after:
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
e : G ≃+o ℤ
⊢ ¬DenselyOrdered G
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 Γ₀
⊢ embedding 1 = 1

Tactic:
map_one

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ 1 = 1
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff d) (X ^ n * p) = (coeff (d - n)) p

pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (X ^ n * p) = 0

Tactic:
· rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul]
    simp

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff d) (X ^ n * p) = 0
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
hx0 : ¬x = 0
⊢ (if h : extensionValuation ↑xy = 0 then 0 else ↑⟨Units.mk0 (v xy) ⋯, ⋯⟩) =
    if h : extensionValuation ↑y = 0 then 0
    else if h : extensionValuation ↑x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩

Tactic:
by_cases hy0 : y = 0
      · simpa [← hy, hy0] using hxy
      · rw [dif_neg, dif_neg, dif_neg]
        · simp only [← WithZero.coe_mul, MulMemClass.mk_mul_mk, WithZero.coe_inj, Subtype.mk.injEq]
          rw [← Units.mk0_mul]
          · ext
            simp [Units.val_mk0, hx, hy, hxy]
          · aesop
        · simpa
        · simpa
        · simp [extensionValuation_apply_coe, hxy, ← hx, ← hy, hx0, hy0]

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

Goal state before:
pp: case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ m < n, (coeff m) φ = 0) → ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0

Tactic:
intro h m hm

Goal state after:
case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ (∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0) → ∀ m < n, (coeff m) φ = 0

Tactic:
intro h m hm

Goal state after:
case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0
m : ℕ
hm : m < n
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
⊢ (coeff 1) (φ ^ n) = ↑n * (coeff 1) φ * constantCoeff φ ^ (n - 1)

Tactic:
rcases Nat.eq_zero_or_pos n with (rfl | hn)

Goal state after:
case inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
⊢ (coeff 1) (φ ^ 0) = ↑0 * (coeff 1) φ * constantCoeff φ ^ (0 - 1)

case inr
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
hn : n > 0
⊢ (coeff 1) (φ ^ n) = ↑n * (coeff 1) φ * constantCoeff φ ^ (n - 1)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0

Tactic:
intro h m hm

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0
m : σ →₀ ℕ
hm : m s = 0
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0) → ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0

Tactic:
intro h m hm

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0
m : σ →₀ ℕ
hm : m s < 1
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
φ ψ : R[X]
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (↑↑((PowerSeries.map (algebraMap R A)).comp ringHom)).toFun ((algebraMap R R[X]) r) = (algebraMap R (PowerSeries A)) r

Tactic:
by simp [PowerSeries.algebraMap_apply]

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
h : ∀ (n : σ →₀ ℕ), (trunc' R n) f = (trunc' R n) g
n : σ →₀ ℕ
⊢ (coeff n) f = (coeff n) g

Tactic:
specialize h n

Goal state after:
σ : 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
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
d : σ →₀ ℕ
hd : ↑((weight w) d) < weightedOrder w (p.toSubring T hp)
⊢ (coeff d) p = 0

Tactic:
simp [coeff_eq_zero_of_lt_weightedOrder w hd, ← p.coeff_toSubring T hp]

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

Goal state before:
pp: case refine_2
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ weightedOrder w p ≤ weightedOrder w (p.toSubring T hp)

Tactic:
refine le_weightedOrder w fun d hd => by
      exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_eq_zero_of_lt_weightedOrder w hd)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
h : n ≠ 0
⊢ 0 ∈ ⋯.toFinset

Tactic:
by revert h; contrapose; simp

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
⊢ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 1)) }, ⋯⟩ = 1

Tactic:
ext; simp

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
⊢ ⟨{ toCompletion := ↑((WithVal.equiv (valuation K v)).symm ((algebraMap R K) 0)) }, ⋯⟩ = 0

Tactic:
ext; simp

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

Goal state before:
pp: case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ↑φ.order.toNat ≤ emultiplicity X φ

Tactic:
apply le_emultiplicity_of_pow_dvd

Goal state after:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ X ^ φ.order.toNat ∣ φ
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case e_l₂
R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
u : Filter ι
g : R⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d ())

Tactic:
ext; simp

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
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ Finsupp.single () (d ()) = d

Tactic:
ext; simp

Goal state after:
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] ⇑ε
p : MvPolynomial σ R
| (MvPolynomial.aeval fun i ↦ (ε.comp (coeToMvPowerSeries.algHom R)) (MvPolynomial.X i)) p

Tactic:
MvPolynomial.aeval_def

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
| MvPolynomial.eval₂ (algebraMap R S) (fun i ↦ (ε.comp (coeToMvPowerSeries.algHom R)) (MvPolynomial.X i)) 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
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p = (MvPolynomial.aeval a) p

Tactic:
MvPolynomial.aeval_def

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
p : MvPolynomial σ R
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p = MvPolynomial.eval₂ (algebraMap R (MvPowerSeries τ S)) a p
Module: Mathlib.Analysis.Real.Cardinality

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

Tactic:
cantorFunction,

Goal state after:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∑' (n : ℕ), cantorFunctionAux c f 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: case a
⊢ #(ℕ → ℚ) = 𝔠

Tactic:
← power_def,

Goal state after:
case a
⊢ #ℚ ^ #ℕ = 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case e'_3
⊢ 𝔠 = #(ℕ → Bool)

Tactic:
← power_def,

Goal state after:
case e'_3
⊢ 𝔠 = #Bool ^ #ℕ
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠

Tactic:
← h2

Goal state after:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x ↦ a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x ↦ a + a - x) '' Ioi a) + #↑{a} + #↑(Ioi a) < 𝔠
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: x y : ℝ
h : x < y
⊢ ¬#↑(Ico x y) ≤ ℵ₀

Tactic:
Cardinal.mk_Ico_real h,

Goal state after:
x y : ℝ
h : x < y
⊢ ¬𝔠 ≤ ℵ₀
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
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
n : σ →₀ ℕ
hc : Finsupp.degree d < Finsupp.degree n
⊢ (coeff d) (∏ a_1 ∈ n.support, a a_1 ^ n a_1) = 0

Tactic:
refine coeff_of_lt_order (lt_of_lt_of_le (Nat.cast_lt.mpr hc)
        (.trans ?_ (le_order_prod _ n.support)))

Goal state after:
σ : Type u_1
R : Type u_3
inst✝³ : CommRing R
τ : Type u_4
S : Type u_5
inst✝² : CommRing S
inst✝¹ : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
n : σ →₀ ℕ
hc : Finsupp.degree d < Finsupp.degree n
⊢ ↑(Finsupp.degree n) ≤ ∑ i ∈ n.support, (a i ^ n i).order
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 : τ →₀ ℕ
⊢ ∑ᶠ (i : ℕ),
      (MvPowerSeries.coeff ((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.symm i)) f •
        (MvPowerSeries.coeff e) (((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.symm i).prod fun s e ↦ a ^ e) =
    ∑ᶠ (d : ℕ), (coeff d) f • (MvPowerSeries.coeff e) (a ^ d)

Tactic:
apply finsum_congr

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 : τ →₀ ℕ
⊢ ∀ (x : ℕ),
    (MvPowerSeries.coeff ((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.symm x)) f •
        (MvPowerSeries.coeff e) (((Finsupp.uniqueLinearEquiv ℕ ℕ ()).toEquiv.symm x).prod fun s e ↦ a ^ e) =
      (coeff x) f • (MvPowerSeries.coeff e) (a ^ x)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case succ.zero.hb
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
⊢ HasSubst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i)

Tactic:
simp [HasSubst, X, substInvFun]

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

Goal state before:
pp: case h
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∀ i ∈ x.1.support ∪ x.2.support, a i ^ 0 = 1

Tactic:
{simp}

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

Goal state before:
pp: case e_a.succ.succ.h₀.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
hj : 0 ∈ Finset.range (i + 2 + 1)
hj' : 0 ≠ 0
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ 0 * B ^ (i + 2 - 0) * ↑((i + 2).choose 0)) = 0

pp: case e_a.succ.succ.h₀.succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
hj : 0 + 1 ∈ Finset.range (i + 2 + 1)
hj' : 0 + 1 ≠ 0
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ (0 + 1) * B ^ (i + 2 - (0 + 1)) * ↑((i + 2).choose (0 + 1))) = 0

pp: case e_a.succ.succ.h₀.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i j : ℕ
hj : j + 1 + 1 ∈ Finset.range (i + 2 + 1)
hj' : j + 1 + 1 ≠ 0
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ (j + 1 + 1) * B ^ (i + 2 - (j + 1 + 1)) * ↑((i + 2).choose (j + 1 + 1))) = 0

Tactic:
· simp at hj'

Goal state after:
case e_a.succ.succ.h₀.succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
hj : 0 + 1 ∈ Finset.range (i + 2 + 1)
hj' : 0 + 1 ≠ 0
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ (0 + 1) * B ^ (i + 2 - (0 + 1)) * ↑((i + 2).choose (0 + 1))) = 0

case e_a.succ.succ.h₀.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i j : ℕ
hj : j + 1 + 1 ∈ Finset.range (i + 2 + 1)
hj' : j + 1 + 1 ≠ 0
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ (j + 1 + 1) * B ^ (i + 2 - (j + 1 + 1)) * ↑((i + 2).choose (j + 1 + 1))) = 0
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (fun x ↦ ‖c x‖ₑ) I i₀
H : c i₀ ≠ 0 ∨ I = univ
i : ι
hi : i ∈ I
⊢ ‖c i‖ ≤ ‖c i₀‖

Tactic:
by simpa [enorm] using! hc_max hi

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P - X) = 0
⊢ (coeff n) (subst P.substInv P) = (coeff n) X

Tactic:
rw [map_sub, sub_eq_zero] at this

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
this : (coeff n) (subst (∑ i, C (P.substInvFun ↑i) * X ^ ↑i) P) = (coeff n) X
⊢ (coeff n) (subst P.substInv P) = (coeff n) X
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
⊢ HasFDerivWithinAt f 0 {x} x

Tactic:
refine .of_not_accPt ?_
  rw [accPt_iff_clusterPt, inf_principal]
  simp [ClusterPt]

Goal state after: