mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case false
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = false
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

pp: case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = true
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
<;>

Goal state after:
case false
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = false
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = true
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case false
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

pp: case true
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

Tactic:
<;>

Goal state after:
case false
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

case true
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
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
ha : HasSubst a
f g : MvPowerSeries σ R
⊢ (substAlgHom ha) (f - g) = (substAlgHom ha) f - (substAlgHom ha) g

Tactic:
map_sub

Goal state after:
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
ha : HasSubst a
s : σ
⊢ (substAlgHom ha) (X s) = a s

Tactic:
substAlgHom_X

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
ha : HasSubst a
s : σ
⊢ a s = a s
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a
⊢ 𝔠 ≤ #ℝ

Tactic:
convert! mk_le_of_injective (cantorFunction_injective _ _)
    · rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
    · exact 1 / 3
    · simp
    · norm_num

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

Goal state before:
pp: case «0»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![subst ![X i, X j] f, X k] ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

pp: case «1»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![subst ![X i, X j] f, X k] ((fun i ↦ i) ⟨1, ⋯⟩)) = 0

Tactic:
<;>

Goal state after:
case «0»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![subst ![X i, X j] f, X k] ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

case «1»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![subst ![X i, X j] f, X k] ((fun i ↦ i) ⟨1, ⋯⟩)) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case «0»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![X i, subst ![X j, X k] f] ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

pp: case «1»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![X i, subst ![X j, X k] f] ((fun i ↦ i) ⟨1, ⋯⟩)) = 0

Tactic:
<;>

Goal state after:
case «0»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![X i, subst ![X j, X k] f] ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

case «1»
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
f : MvPowerSeries (Fin 2) R
i j k : σ
hF : constantCoeff f = 0
⊢ constantCoeff (![X i, subst ![X j, X k] f] ((fun i ↦ i) ⟨1, ⋯⟩)) = 0
Module: Mathlib.Analysis.Real.Cardinality

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

Tactic:
Cardinal.mk_Ioc_real h,

Goal state after:
x y : ℝ
h : x < y
⊢ ¬𝔠 ≤ ℵ₀
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case pos
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : n = 0
⊢ 0 = f n * ↑n ^ (-s)

pp: case neg
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : ¬n = 0
⊢ f n / ↑n ^ s = f n * ↑n ^ (-s)

Tactic:
<;>

Goal state after:
case pos
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : n = 0
⊢ 0 = f n * ↑n ^ (-s)

case neg
f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
n : ℕ
h : ¬n = 0
⊢ f n / ↑n ^ s = f n * ↑n ^ (-s)
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ 0 = f 0 / 0

Tactic:
div_zero

Goal state after:
case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ 0 = 0
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
hn : n = 0
⊢ term f s n = term g s n

pp: case inr
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = term g s n

Tactic:
<;>

Goal state after:
case inl
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
hn : n = 0
⊢ term f s n = term g s n

case inr
f g : ℕ → ℂ
h : ∀ {n : ℕ}, n ≠ 0 → f n = g n
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term f s n = term g s n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

Tactic:
obtain ⟨hab, -⟩ := Nat.mem_divisorsAntidiagonal.mp hk

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0
Module: Mathlib.NumberTheory.LSeries.Basic

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

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

Tactic:
<;>

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
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case pos
f : ℕ → ℂ
n : ℕ
hn : n = 1
⊢ (f * δ) n = (f 1 • δ) n

pp: case neg
f : ℕ → ℂ
n : ℕ
hn : ¬n = 1
⊢ (f * δ) n = (f 1 • δ) n

Tactic:
<;>

Goal state after:
case pos
f : ℕ → ℂ
n : ℕ
hn : n = 1
⊢ (f * δ) n = (f 1 • δ) n

case neg
f : ℕ → ℂ
n : ℕ
hn : ¬n = 1
⊢ (f * δ) n = (f 1 • δ) n
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
⊢ ‖f 1‖ ≤ C

Tactic:
simpa using hC 1 one_ne_zero

Goal state after:
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 g : R⟦X⟧
⊢ (substAlgHom ha) (f - g) = (substAlgHom ha) f - (substAlgHom ha) g

Tactic:
map_sub

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 g : R⟦X⟧
⊢ (substAlgHom ha) f - (substAlgHom ha) g = (substAlgHom ha) f - (substAlgHom ha) g
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q x✝ : ℕ
h✝ : 1 < q
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 0) 0, map_zero' := ⋯ } x✝ = 0 x✝

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q x✝ : ℕ
h✝ : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 0)) x✝ = 0 x✝

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q x✝ : ℕ
h✝ : 1 < q
⊢ { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 0) 0, map_zero' := ⋯ } x✝ = 0 x✝

case neg
R : Type u_1
inst✝ : CommSemiring R
q x✝ : ℕ
h✝ : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 0)) x✝ = 0 x✝
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
τ : Type u_3
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
a : MvPowerSeries τ S
inst✝¹ : Algebra A S
inst✝ : IsScalarTower A R S
ha : HasSubst a
r : A
f : R⟦X⟧
⊢ (substAlgHom ha) (r • f) = r • (substAlgHom ha) f

Tactic:
AlgHom.map_smul_of_tower

Goal state after:
A : Type u_1
inst✝⁶ : CommRing A
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Algebra A R
τ : Type u_3
S : Type u_4
inst✝³ : CommRing S
inst✝² : Algebra R S
a : MvPowerSeries τ S
inst✝¹ : Algebra A S
inst✝ : IsScalarTower A R S
ha : HasSubst a
r : A
f : R⟦X⟧
⊢ r • (substAlgHom ha) f = r • (substAlgHom ha) f
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
hn : n = 1
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
hn : ¬n = 1
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
hn : n = 1
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
hn : ¬n = 1
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f + g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) +
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n
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 : σ →₀ ℕ
⊢ (coeff (e s)) f • (MvPowerSeries.coeff e) (MvPowerSeries.X s ^ e s) =
    if e = Finsupp.single s (e s) then (coeff (e s)) f else 0

pp: R : Type u_2
inst✝¹ : CommRing R
σ : Type u_7
inst✝ : DecidableEq σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∀ (x : ℕ), x ≠ e s → (coeff x) f • (MvPowerSeries.coeff e) (MvPowerSeries.X s ^ x) = 0

Tactic:
<;>

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

R : Type u_2
inst✝¹ : CommRing R
σ : Type u_7
inst✝ : DecidableEq σ
s : σ
f : R⟦X⟧
e : σ →₀ ℕ
⊢ ∀ (x : ℕ), x ≠ e s → (coeff x) f • (MvPowerSeries.coeff e) (MvPowerSeries.X s ^ x) = 0
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
⊢ (substAlgHom ha) X = a

Tactic:
substAlgHom_X

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
⊢ a = a
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑‖c‖₊⁻¹

Tactic:
rw [← nnnorm_inv]
  exact egauge_le_of_mem_smul <| (mem_inv_smul_set_iff₀ hc _ _).2 h

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

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

pp: case succ.zero.ha.succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
a✝ : 0 + 1 ≠ 1
⊢ (coeff (0 + 1)) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ (0 + 1)) = 0

pp: case succ.zero.ha.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n✝ : ℕ
a✝ : n✝ + 1 + 1 ≠ 1
⊢ (coeff (n✝ + 1 + 1)) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ (n✝ + 1 + 1)) = 0

Tactic:
<;>

Goal state after:
case succ.zero.ha.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
a✝ : 0 ≠ 1
⊢ (coeff 0) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ 0) = 0

case succ.zero.ha.succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
a✝ : 0 + 1 ≠ 1
⊢ (coeff (0 + 1)) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ (0 + 1)) = 0

case succ.zero.ha.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n✝ : ℕ
a✝ : n✝ + 1 + 1 ≠ 1
⊢ (coeff (n✝ + 1 + 1)) P • (coeff (0 + 1)) ((∑ i, C (P.substInvFun ↑i) * X ^ ↑i) ^ (n✝ + 1 + 1)) = 0
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 : t ⊆ u
hv : t ⊆ v
⊢ ((∏ x ∈ u \ t, f x) * ∏ x ∈ t, f x) n = (∏ b ∈ v, f b) n

Tactic:
← Finset.prod_sdiff hv

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 : t ⊆ u
hv : t ⊆ v
⊢ ((∏ x ∈ u \ t, f x) * ∏ x ∈ t, f x) n = ((∏ x ∈ v \ t, f x) * ∏ x ∈ t, f x) n
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case 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
⊢ ∑ᶠ (d : ℕ),
      (coeff d) P *
        (coeff (n + 1 + 1)) ((B + -(C (⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P)) * X ^ (n + 2))) ^ d) =
    0

Tactic:
generalize hk : ⅟(P.coeff 1) * coeff (n + 1 + 1) (subst B P) = k

Goal state after:
case 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
⊢ ∑ᶠ (d : ℕ), (coeff d) P * (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ d) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case «0»
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
⊢ (single 0 (e 0) + single 1 (e 1)) ((fun i ↦ i) ⟨0, ⋯⟩) = e ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
⊢ (single 0 (e 0) + single 1 (e 1)) ((fun i ↦ i) ⟨1, ⋯⟩) = e ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
⊢ (single 0 (e 0) + single 1 (e 1)) ((fun i ↦ i) ⟨0, ⋯⟩) = e ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
⊢ (single 0 (e 0) + single 1 (e 1)) ((fun i ↦ i) ⟨1, ⋯⟩) = e ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Semiring 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst✝³ : Semiring 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : Module 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝⁴] s
⊢ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ⊆ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x))

pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Semiring 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst✝³ : Semiring 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : Module 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝⁴] s
⊢ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x)) ⊆ ↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x))

Tactic:
<;>

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Semiring 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst✝³ : Semiring 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : Module 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝⁴] s
⊢ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ⊆ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x))

𝕜 : Type u_1
E : Type u_2
inst✝⁷ : Semiring 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
x : E
s : Set E
𝕜' : Type u_3
inst✝³ : Semiring 𝕜'
inst✝² : SMul 𝕜 𝕜'
inst✝¹ : Module 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
hs : Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ∧ x ∈ closure[inst✝⁴] s
⊢ ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x)) ⊆ ↑(Submodule.span 𝕜' (tangentConeAt 𝕜' s x))
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤

Tactic:
apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'

Goal state after:
E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x : E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst✝²] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ (interior ↑(Submodule.span ℝ (tangentConeAt ℝ s x))).Nonempty
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
hx : DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
hx : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
hx : DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
hx : ¬DifferentiableAt 𝕜 f x
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : ¬DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
hx : ¬DifferentiableWithinAt 𝕜 f t x
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
s : Set F
x : 𝕜
⊢ derivWithin f t x ∈ s ↔
    DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s

Tactic:
by_cases hx : DifferentiableWithinAt 𝕜 f t x <;>
    simp [derivWithin_zero_of_not_differentiableWithinAt, *]

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

Goal state before:
pp: case pos
𝕜 : 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
s : Set (E →L[𝕜] F)
x : E
hx : DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

pp: case neg
𝕜 : 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
s : Set (E →L[𝕜] F)
x : E
hx : ¬DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
<;>

Goal state after:
case pos
𝕜 : 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
s : Set (E →L[𝕜] F)
x : E
hx : DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

case neg
𝕜 : 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
s : Set (E →L[𝕜] F)
x : E
hx : ¬DifferentiableAt 𝕜 f x
⊢ fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s