harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
theorem LFunction_apply_one_ne_zero_of_quadratic {χ : DirichletCharacter ℂ N}
    (hχ : χ ^ 2 = 1) (χ_ne : χ ≠ 1) :
    χ.LFunction 1 ≠ 0

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : DirichletCharacter.BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ False

Tactic:
refine B.F_neg_two.not_gt ?_

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : DirichletCharacter.BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ 0 < B.F ↑(-2)

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
⊢ False

Tactic:
let B : BadChar N := {χ := χ, χ_sq := hχ, hχ := hL, χ_ne := χ_ne}

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : DirichletCharacter.BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ False

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : DirichletCharacter.BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ 0 < B.F ↑(-2)

Tactic:
refine ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn (zetaMul_nonneg hχ)
  (χ.isMultiplicative_zetaMul.map_one ▸ zero_lt_one) B.F_differentiable ?_
  (fun _ ↦ B.F_eq_LSeries) _

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : DirichletCharacter.BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ LSeries.abscissaOfAbsConv ⇑χ.zetaMul ≤ ↑1

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : DirichletCharacter.BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ LSeries.abscissaOfAbsConv ⇑χ.zetaMul ≤ ↑1

Tactic:
exact LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable
  fun _ a ↦ χ.LSeriesSummable_zetaMul a

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
⊢ LFunction χ 1 ≠ 0

Tactic:
intro hL

Result:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
⊢ False
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)] lemma pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose!

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ≠ ∅ ∨ n = 0 → s ^ n ≠ ∅

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Result:
case mpr.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Proof state:
case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ s ^ 0 ≠ ∅

Tactic:
rw [← nonempty_iff_ne_empty]

Result:
case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Proof state:
case mp.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : s ≠ ∅
⊢ s ^ n ≠ ∅

Tactic:
exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).pow

Result:
no goals

Proof state:
case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
exact empty_pow hn

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ≠ ∅ ∨ n = 0 → s ^ n ≠ ∅

Tactic:
rintro (hs | rfl)

Result:
case mp.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : s ≠ ∅
⊢ s ^ n ≠ ∅

case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ s ^ 0 ≠ ∅

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem hasFiniteIntegral_comp_iff ⦃f : γ → E⦄ (hf : StronglyMeasurable f) :
    HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ x ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ y, ‖f y‖ ∂η x) (κ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ⊤
⊢ ∫⁻ (b : β), ∫⁻ (a : γ), ‖f a‖ₑ ∂η b ∂κ a < ⊤ ↔ ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal ∂κ a < ⊤

Tactic:
rw [lintegral_congr_ae]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ⊤
⊢ (fun b => ∫⁻ (a : γ), ‖f a‖ₑ ∂η b) =ᶠ[ae (κ a)] fun a => ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
⊢ (∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ⊤) →
    (∫⁻ (b : β), ∫⁻ (a : γ), ‖f a‖ₑ ∂η b ∂κ a < ⊤ ↔
      ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal ∂κ a < ⊤)

Tactic:
intro h

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : StronglyMeasurable f
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h : ∀ᵐ (x : β) ∂κ a, ∫⁻ (a : γ), ‖f a‖ₑ ∂η x < ⊤
⊢ ∫⁻ (b : β), ∫⁻ (a : γ), ‖f a‖ₑ ∂η b ∂κ a < ⊤ ↔ ∫⁻ (a : β), ENNReal.ofReal (∫⁻ (a : γ), ‖f a‖ₑ ∂η a).toReal ∂κ a < ⊤
-- Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
lemma volumeIoiPow_apply_Iio (n : ℕ) (x : Ioi (0 : ℝ)) :
    volumeIoiPow n (Iio x) = ENNReal.ofReal (x.1 ^ (n + 1) / (n + 1))

Proof state:
case h
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
y : ℝ
hy : y ∈ Ioc 0 ↑x
⊢ 0 y ≤ y ^ n

Tactic:
exact pow_nonneg hy.1.le _

Result:
no goals

Proof state:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ 0 ≤ᶠ[ae (volume.restrict (Ioc 0 ↑x))] fun x => x ^ n

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioc] with y hy

Result:
case h
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
y : ℝ
hy : y ∈ Ioc 0 ↑x
⊢ 0 y ≤ y ^ n

Proof state:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ (volumeIoiPow n) (Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
rw [volumeIoiPow, withDensity_apply _ measurableSet_Iio,
  setLIntegral_subtype measurableSet_Ioi _ fun a : ℝ ↦ .ofReal (a ^ n),
  image_subtype_val_Ioi_Iio, restrict_congr_set Ioo_ae_eq_Ioc,
  ← ofReal_integral_eq_lintegral_ofReal (intervalIntegrable_pow _).1, ← integral_of_le hr₀]

Result:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ENNReal.ofReal (∫ (x : ℝ) in 0 ..↑x, x ^ n) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ 0 ≤ᶠ[ae (volume.restrict (Ioc 0 ↑x))] fun x => x ^ n

Proof state:
n : ℕ
x : ↑(Ioi 0)
⊢ (volumeIoiPow n) (Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
have hr₀ : 0 ≤ x.1 := le_of_lt x.2

Result:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ (volumeIoiPow n) (Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Proof state:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ENNReal.ofReal (∫ (x : ℝ) in 0 ..↑x, x ^ n) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean
lemma exact_iff_degreewise_exact :
    S.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact

Proof state:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact

Tactic:
constructor

Result:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.Exact → ∀ (i : ι), (S.map (eval C c i)).Exact

case mpr
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ (∀ (i : ι), (S.map (eval C c i)).Exact) → S.Exact

Proof state:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.Exact → ∀ (i : ι), (S.map (eval C c i)).Exact

Tactic:
intro hS i

Result:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
i : ι
⊢ (S.map (eval C c i)).Exact

Proof state:
case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
i : ι
⊢ (S.map (eval C c i)).Exact

Tactic:
exact hS.map (eval C c i)

Result:
no goals

Proof state:
case mpr
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ (∀ (i : ι), (S.map (eval C c i)).Exact) → S.Exact

Tactic:
exact exact_of_degreewise_exact S

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem preimage_extChartAt_eventuallyEq_compl_singleton (y : M) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    ((extChartAt I x).symm ⁻¹' s ∩ range I : Set E) =ᶠ[𝓝[{extChartAt I x x}ᶜ] (extChartAt I x x)]
    ((extChartAt I x).symm ⁻¹' t ∩ range I : Set E)

Proof state:
case pos
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ ↑(extChartAt I x).symm z ∈ s ↔ ↑(extChartAt I x).symm z ∈ t

Tactic:
rw [← eq_iff_iff]

Result:
case pos
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ (↑(extChartAt I x).symm z ∈ s) = (↑(extChartAt I x).symm z ∈ t)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
h'z : z ∈ {↑(extChartAt I x) x}ᶜ
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
⊢ ↑(extChartAt I x).symm z ∈ {x}ᶜ

Tactic:
simp only [mem_compl_iff, mem_singleton_iff, ne_comm, ne_eq] at h'z ⊢

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
this : T1Space M
u : Set M
u_mem : u ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
hu : u ∩ {x}ᶜ ⊆ {y | (y ∈ s) = (y ∈ t)}
B : (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 (↑(extChartAt I x) x)
z : E
hIz : z ∈ range ↑I
hz : ↑(extChartAt I x).symm z ∈ u ∧ z ∈ (extChartAt I x).target
h'z : ¬z = ↑(extChartAt I x) x
⊢ ¬x = ↑(extChartAt I x).symm z
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem weight_add_weight_pairMap {k : ℕ} (t : Finset σ × σ) (h : t ∈ pairs σ k) :
    weight σ R k t + weight σ R k (pairMap σ t) = 0

Proof state:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * (X t.2 * X t.2 ^ (k - #t.1))) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0

Tactic:
nth_rewrite 1 [← pow_one (X t.snd)]

Result:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * (X t.2 ^ 1 * X t.2 ^ (k - #t.1))) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0
-- Mathlib/Data/Multiset/Count.lean
theorem countP_eq_zero {s} : countP p s = 0 ↔ ∀ a ∈ s, ¬p a :=
  Quot.inductionOn s fun _l => by simp [List.countP_eq_zero]

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) _l) = 0 ↔ ∀ a ∈ Quot.mk (⇑(isSetoid α)) _l, ¬p a

Tactic:
simp [List.countP_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem Away.isLocalization_mul (hd : d ≠ 0) :
    letI := (awayMap 𝒜 hg hx).toAlgebra
    IsLocalization.Away (isLocalizationElem hf hg) (Away 𝒜 x)

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
⊢ s * g ^ (n * d) ∈ 𝒜 ((n * (e + 1)) • (d + 1))

Tactic:
convert SetLike.mul_mem_graded hs (SetLike.pow_mem_graded _ hg) using 2

Result:
case h.e'_4.h.e'_1
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
⊢ (n * (e + 1)) • (d + 1) = n • (d + 1 + e) + (n * d) • e

Proof state:
case h.e'_4.h.e'_1
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
n : ℕ
s : A
d : ℕ
hf : f ∈ 𝒜 (d + 1)
hd : d + 1 ≠ 0
hs : s ∈ 𝒜 (n • (d + 1 + e))
⊢ n * (e + 1) * (d + 1) = n * (d + 1 + e) + n * d * e

Tactic:
ring

Result:
no goals

Proof state:
case surj'
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
⊢ ∀ (z : Away 𝒜 x), ∃ x_1, z * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1

Tactic:
intro z

Result:
case surj'
R : Type u_2
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
e d : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : d ≠ 0
this : Algebra (Away 𝒜 f) (Away 𝒜 x) := (awayMap 𝒜 hg hx).toAlgebra
z : Away 𝒜 x
⊢ ∃ x_1, z * (algebraMap (Away 𝒜 f) (Away 𝒜 x)) ↑x_1.2 = (algebraMap (Away 𝒜 f) (Away 𝒜 x)) x_1.1
-- Mathlib/Data/ZMod/Basic.lean
theorem val_add_le {n : ℕ} (a b : ZMod n) : (a + b).val ≤ a.val + b.val

Proof state:
case zero
a b : ZMod 0
⊢ (a + b).val ≤ a.val + b.val

Tactic:
simpa [ZMod.val] using Int.natAbs_add_le _ _

Result:
no goals

Proof state:
case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val

Tactic:
simpa [ZMod.val_add] using Nat.mod_le _ _

Result:
no goals

Proof state:
n : ℕ
a b : ZMod n
⊢ (a + b).val ≤ a.val + b.val

Tactic:
cases n

Result:
case zero
a b : ZMod 0
⊢ (a + b).val ≤ a.val + b.val

case succ
n✝ : ℕ
a b : ZMod (n✝ + 1)
⊢ (a + b).val ≤ a.val + b.val
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_flatten {p : α → Prop} {L : Array (Array α)} :
    (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x

Proof state:
case mpr
α : Type u_1
p : α → Prop
L : Array (Array α)
a✝² : ∀ (l : Array α), l ∈ L → ∀ (x : α), x ∈ l → p x
x✝¹ : α
x✝ : Array α
a✝¹ : x✝ ∈ L
a✝ : x✝¹ ∈ x✝
⊢ p x✝¹

Tactic:
solve_by_elim

Result:
no goals

Proof state:
case mpr
α : Type u_1
p : α → Prop
L : Array (Array α)
⊢ (∀ (l : Array α), l ∈ L → ∀ (x : α), x ∈ l → p x) → ∀ (x : α) (x_1 : Array α), x_1 ∈ L → x ∈ x_1 → p x

Tactic:
intros

Result:
case mpr
α : Type u_1
p : α → Prop
L : Array (Array α)
a✝² : ∀ (l : Array α), l ∈ L → ∀ (x : α), x ∈ l → p x
x✝¹ : α
x✝ : Array α
a✝¹ : x✝ ∈ L
a✝ : x✝¹ ∈ x✝
⊢ p x✝¹

Proof state:
α : Type u_1
p : α → Prop
L : Array (Array α)
⊢ (∀ (x : α) (x_1 : Array α), x_1 ∈ L → x ∈ x_1 → p x) ↔ ∀ (l : Array α), l ∈ L → ∀ (x : α), x ∈ l → p x

Tactic:
constructor <;> (intros; solve_by_elim)

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
L : Array (Array α)
⊢ (∀ (x : α), x ∈ L.flatten → p x) ↔ ∀ (l : Array α), l ∈ L → ∀ (x : α), x ∈ l → p x

Tactic:
simp only [mem_flatten, forall_exists_index, and_imp]

Result:
α : Type u_1
p : α → Prop
L : Array (Array α)
⊢ (∀ (x : α) (x_1 : Array α), x_1 ∈ L → x ∈ x_1 → p x) ↔ ∀ (l : Array α), l ∈ L → ∀ (x : α), x ∈ l → p x
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors'
    {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t)
    (hnzd : ∀ m ≤ n, m ≠ 0 → (m : R) ∈ nonZeroDivisors R) :
    n < p.rootMultiplicity t

Proof state:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ 1 ∈ nonZeroDivisors R

Tactic:
exact Submonoid.one_mem _

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑n.factorial ∈ nonZeroDivisors R

Tactic:
induction n with
| zero =>
  simp only [Nat.factorial_zero, Nat.cast_one]
  exact Submonoid.one_mem _
| succ n ih =>
  rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
  exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑n.factorial ∈ nonZeroDivisors R

Tactic:
clear hroot

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑n.factorial ∈ nonZeroDivisors R

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ n < rootMultiplicity t p

Tactic:
apply lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
n : ℕ
h : p ≠ 0
hroot : ∀ m ≤ n, ((⇑derivative)^[m] p).IsRoot t
hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑n.factorial ∈ nonZeroDivisors R

Proof state:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(Nat.factorial 0) ∈ nonZeroDivisors R

Tactic:
simp only [Nat.factorial_zero, Nat.cast_one]

Result:
case zero
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
hnzd : ∀ m ≤ 0, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ 1 ∈ nonZeroDivisors R

Proof state:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n.factorial ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1).factorial ∈ nonZeroDivisors R

Tactic:
rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]

Result:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n.factorial ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1) ∈ nonZeroDivisors R ∧ ↑n.factorial ∈ nonZeroDivisors R

Proof state:
case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n.factorial ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1) ∈ nonZeroDivisors R ∧ ↑n.factorial ∈ nonZeroDivisors R

Tactic:
exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem insepDegree_bot : insepDegree F (⊥ : IntermediateField F E) = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
⊢ insepDegree F ↥⊥ = 1

Tactic:
rwa [insepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ insepDegree F ↥⊥ = 1

Tactic:
have := lift_insepDegree_eq_of_equiv _ _ _ (botEquiv F E)

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)
⊢ insepDegree F ↥⊥ = 1
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_lt_div_iff : 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Proof state:
case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0

Tactic:
simp [lt_irrefl, zero_le_one]

Result:
no goals

Proof state:
case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
simp [hb, hb.not_lt, one_lt_div]

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
simp [hb, hb.not_lt, one_lt_div_of_neg]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
rcases lt_trichotomy b 0 with (hb | rfl | hb)

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

case inr.inl
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0

case inr.inr
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b