harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_eq_zero_of_lt_weightedOrder {d : σ →₀ ℕ} (h : (weight w d) < f.weightedOrder w) :
    coeff R d f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)

Tactic:
exact weightedOrder_le w h

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w f
⊢ (coeff R d) f = 0

Tactic:
contrapose! h

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ weightedOrder w f ≤ ↑((weight w) d)
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_biUnion_null_iff {I : Set ι} (hI : I.Countable) {s : ι → Set α} :
    μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
⊢ μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0

Tactic:
refine ⟨fun h i hi ↦ measure_mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩

Result:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, μ (s i) = 0
⊢ μ (⋃ i ∈ I, s i) = 0

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, μ (s i) = 0
⊢ μ (⋃ i ∈ I, s i) = 0

Tactic:
have _ := hI.to_subtype

Result:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, μ (s i) = 0
x✝ : Countable ↑I
⊢ μ (⋃ i ∈ I, s i) = 0

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
I : Set ι
hI : I.Countable
s : ι → Set α
h : ∀ i ∈ I, μ (s i) = 0
x✝ : Countable ↑I
⊢ μ (⋃ i ∈ I, s i) = 0

Tactic:
simpa [h] using measure_iUnion_le (μ := μ) fun x : I ↦ s x

Result:
no goals
-- Mathlib/FieldTheory/Extension.lean
theorem le_iff : L₁ ≤ L₂ ↔
    ∃ h : L₁.carrier ≤ L₂.carrier, L₂.emb.comp (inclusion h) = L₁.emb

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb

Tactic:
simp_rw [AlgHom.ext_iff]

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), ∀ (x : ↥L₁.carrier), (L₂.emb.comp (inclusion ⋯)) x = L₁.emb x

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), ∀ (x : ↥L₁.carrier), (L₂.emb.comp (inclusion ⋯)) x = L₁.emb x

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integral_fun_fst (f : α → E) : ∫ z, f z.1 ∂μ.prod ν = (ν univ).toReal • ∫ x, f x ∂μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → E
⊢ ∫ (z : β × α), f z.swap.1 ∂ν.prod μ = (ν univ).toReal • ∫ (x : α), f x ∂μ

Tactic:
apply integral_fun_snd

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → E
⊢ ∫ (z : α × β), f z.1 ∂μ.prod ν = (ν univ).toReal • ∫ (x : α), f x ∂μ

Tactic:
rw [← integral_prod_swap]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → E
⊢ ∫ (z : β × α), f z.swap.1 ∂ν.prod μ = (ν univ).toReal • ∫ (x : α), f x ∂μ
-- Mathlib/CategoryTheory/MorphismProperty/Composition.lean
/-- The multiplicative closure of a multiplicative property is equal to itself. -/
@[simp]
lemma multiplicativeClosure_eq_self [W.IsMultiplicative] : W.multiplicativeClosure = W

Proof state:
case id
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x : C
⊢ W (𝟙 x)

Tactic:
exact W.id_mem x

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W f✝

Tactic:
induction hf with
| of _ hf₀ => exact hf₀
| id x => exact W.id_mem x
| comp_of _ _ _ hg hf => exact W.comp_mem _ _ hf hg

Result:
no goals

Proof state:
case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : W.multiplicativeClosure f✝
hg : W g✝
hf : W f✝
⊢ W (f✝ ≫ g✝)

Tactic:
exact W.comp_mem _ _ hf hg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
⊢ W.multiplicativeClosure ≤ W

Tactic:
intro _ _ _ hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W f✝

Proof state:
case of
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ : C
f✝ : x✝ ⟶ y✝
hf₀ : W f✝
⊢ W f✝

Tactic:
exact hf₀

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
⊢ W.multiplicativeClosure = W

Tactic:
apply le_antisymm _ <| le_multiplicativeClosure W

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
⊢ W.multiplicativeClosure ≤ W
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem ne_zero_of_degree_ge_degree (hpq : p.degree ≤ q.degree) (hp : p ≠ 0) : q ≠ 0 :=
  Polynomial.ne_zero_of_degree_gt
    (lt_of_lt_of_le (bot_lt_iff_ne_bot.mpr (by rwa [Ne, Polynomial.degree_eq_bot])) hpq :
      q.degree > ⊥)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
⊢ p.degree ≠ ⊥

Tactic:
rwa [Ne, Polynomial.degree_eq_bot]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_eq_exp : (exp 𝕂 : 𝔸 → 𝔸) = exp 𝕂'

Proof state:
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 => x) = (expSeries 𝕂' 𝔸 n) fun x_1 => x

Tactic:
rw [expSeries_eq_expSeries 𝕂 𝕂' 𝔸 n x]

Result:
no goals

Proof state:
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
⊢ (expSeries 𝕂 𝔸).sum x = (expSeries 𝕂' 𝔸).sum x

Tactic:
refine tsum_congr fun n => ?_

Result:
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 => x) = (expSeries 𝕂' 𝔸 n) fun x_1 => x

Proof state:
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
⊢ exp 𝕂 x = exp 𝕂' x

Tactic:
rw [exp, exp]

Result:
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
⊢ (expSeries 𝕂 𝔸).sum x = (expSeries 𝕂' 𝔸).sum x

Proof state:
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ exp 𝕂 = exp 𝕂'

Tactic:
ext x

Result:
case h
𝕂 : Type u_1
𝕂' : Type u_2
𝔸 : Type u_3
inst✝⁶ : Field 𝕂
inst✝⁵ : Field 𝕂'
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : Algebra 𝕂' 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
⊢ exp 𝕂 x = exp 𝕂' x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_replicate {β} (f : α → List β) : (replicate n a).flatMap f = (replicate n (f a)).flatten

Proof state:
α : Type u_1
n : Nat
a : α
β : Type u_2
f : α → List β
⊢ flatMap f (replicate n a) = (replicate n (f a)).flatten

Tactic:
induction n with
| zero => simp
| succ n ih => simp only [replicate_succ, flatMap_cons, ih, flatten_cons]

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
β : Type u_2
f : α → List β
n : Nat
ih : flatMap f (replicate n a) = (replicate n (f a)).flatten
⊢ flatMap f (replicate (n + 1) a) = (replicate (n + 1) (f a)).flatten

Tactic:
simp only [replicate_succ, flatMap_cons, ih, flatten_cons]

Result:
no goals

Proof state:
case zero
α : Type u_1
a : α
β : Type u_2
f : α → List β
⊢ flatMap f (replicate 0 a) = (replicate 0 (f a)).flatten

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/LagrangeMultipliers.lean
theorem IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt
    (hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀) (hf' : HasStrictFDerivAt f f' x₀)
    (hφ' : HasStrictFDerivAt φ φ' x₀) :
    ∃ (Λ : Module.Dual ℝ F) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ ∀ x, Λ (f' x) + Λ₀ • φ' x = 0

Proof state:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
Λ' : F × ℝ →ₗ[ℝ] ℝ
h0 : Λ' ≠ 0
hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker Λ'
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0

Tactic:
rcases e.surjective Λ' with ⟨⟨Λ, Λ₀⟩, rfl⟩

Result:
case intro.intro.intro.mk
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : E →L[ℝ] ℝ
hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ :=
  (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ
Λ : F →ₗ[ℝ] ℝ
Λ₀ : ℝ
h0 : e (Λ, Λ₀) ≠ 0
hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))
⊢ ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIsoAt_of_comp_left (φ : K ⟶ L) (φ' : L ⟶ M) (i : ι) [K.HasHomology i]
    [L.HasHomology i] [M.HasHomology i]
    [hφ : QuasiIsoAt φ i] [hφφ' : QuasiIsoAt (φ ≫ φ') i] :
    QuasiIsoAt φ' i

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : IsIso (homologyMap φ i)
hφφ' : IsIso (homologyMap (φ ≫ φ') i)
⊢ IsIso (homologyMap φ' i)

Tactic:
rw [homologyMap_comp] at hφφ'

Result:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : IsIso (homologyMap φ i)
hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)
⊢ IsIso (homologyMap φ' i)

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
hφφ' : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap] at hφ hφφ' ⊢

Result:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : IsIso (homologyMap φ i)
hφφ' : IsIso (homologyMap (φ ≫ φ') i)
⊢ IsIso (homologyMap φ' i)

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : IsIso (homologyMap φ i)
hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)
⊢ IsIso (homologyMap φ' i)

Tactic:
exact IsIso.of_isIso_comp_left (homologyMap φ i) (homologyMap φ' i)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_desc {S T U V W : C} [HasBinaryCoproduct U W] [HasBinaryCoproduct T V]
    (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) :
    coprod.map h k ≫ coprod.desc f g = coprod.desc (h ≫ f) (k ≫ g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
S T U V W : C
inst✝¹ : HasBinaryCoproduct U W
inst✝ : HasBinaryCoproduct T V
f : U ⟶ S
g : W ⟶ S
h : T ⟶ U
k : V ⟶ W
⊢ map h k ≫ desc f g = desc (h ≫ f) (k ≫ g)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem nodup_roots_iff_of_splits {f : F[X]} (hf : f ≠ 0) (h : f.Splits (RingHom.id F)) :
    f.roots.Nodup ↔ f.Separable

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬f.Separable
⊢ ¬f.roots.Nodup

Tactic:
rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep

Result:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
⊢ ¬f.roots.Nodup

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
⊢ f.roots.Nodup ↔ f.Separable

Tactic:
refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩

Result:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬f.Separable
⊢ ¬f.roots.Nodup

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
⊢ f.roots.Nodup ↔ f.Separable

Tactic:
classical
refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
obtain ⟨x, hx⟩ := exists_root_of_splits _
  (splits_of_splits_of_dvd _ hf h (gcd_dvd_left f _)) hnsep
simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩

Result:
no goals

Proof state:
case intro
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval₂ (RingHom.id F) x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ∃ x, 1 < Multiset.count x f.roots

Tactic:
exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
⊢ ¬f.roots.Nodup

Tactic:
obtain ⟨x, hx⟩ := exists_root_of_splits _
  (splits_of_splits_of_dvd _ hf h (gcd_dvd_left f _)) hnsep

Result:
case intro
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval₂ (RingHom.id F) x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ¬f.roots.Nodup

Proof state:
case intro
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval₂ (RingHom.id F) x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ¬f.roots.Nodup

Tactic:
simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]

Result:
case intro
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
h : Splits (RingHom.id F) f
hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0
x : F
hx : eval₂ (RingHom.id F) x (GCDMonoid.gcd f (derivative f)) = 0
⊢ ∃ x, 1 < Multiset.count x f.roots
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem Prime.left_dvd_or_dvd_right_of_dvd_mul [CancelCommMonoidWithZero M] {p : M} (hp : Prime p)
    {a b : M} : a ∣ p * b → p ∣ a ∨ a ∣ b

Proof state:
case intro.inl
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b

Tactic:
exact Or.inl h

Result:
no goals

Proof state:
case intro.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b x : M
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b

Tactic:
exact Or.inr (hc.symm ▸ dvd_mul_right _ _)

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b

Tactic:
rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)

Result:
case intro.inl
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
h : p ∣ a
⊢ p ∣ a ∨ a ∣ b

case intro.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b : M
⊢ a ∣ p * b → p ∣ a ∨ a ∣ b

Tactic:
rintro ⟨c, hc⟩

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b c : M
hc : p * b = a * c
⊢ p ∣ a ∨ a ∣ b

Proof state:
case intro.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b x : M
hc : p * b = a * (p * x)
⊢ p ∣ a ∨ a ∣ b

Tactic:
rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc

Result:
case intro.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
hp : Prime p
a b x : M
hc : b = a * x
⊢ p ∣ a ∨ a ∣ b
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q)
    (hPz : P z = 0) (hQz : Q z = 0) : P ≈ Q

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ P ≈ Q

Tactic:
use (isUnit_Y_of_Z_eq_zero hP hPz).unit / (isUnit_Y_of_Z_eq_zero hQ hQz).unit

Result:
case h
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ (fun m => m • Q) (⋯.unit / ⋯.unit) = P

Proof state:
case h
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ (fun m => m • Q) (⋯.unit / ⋯.unit) = P

Tactic:
simp only [Units.smul_def, smul_fin3, X_eq_zero_of_Z_eq_zero hQ.left hQz, hQz, mul_zero,
  Units.val_div_eq_div_val, IsUnit.unit_spec, (isUnit_Y_of_Z_eq_zero hQ hQz).div_mul_cancel]

Result:
case h
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ ![0, P y, 0] = P

Proof state:
case h
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ ![0, P y, 0] = P

Tactic:
conv_rhs => rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma forall_uIoc_iff {P : α → Prop} :
    (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
P : α → Prop
⊢ (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x

Tactic:
simp only [uIoc_eq_union, mem_union, or_imp, forall_and]

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma update_piecewise_of_mem [DecidableEq ι] {i : ι} (hi : i ∈ s) (v : π i) :
    update (s.piecewise f g) i v = s.piecewise (update f i v) g

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
j : ι
hj : j ∉ s
⊢ j ≠ i

Tactic:
exact fun h => hj (h.symm ▸ hi)

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise (update f i v) g

Tactic:
rw [update_piecewise]

Result:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise (update f i v) g

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
⊢ s.piecewise (update f i v) (update g i v) = s.piecewise (update f i v) g

Tactic:
refine s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..

Result:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
hi : i ∈ s
v : π i
j : ι
hj : j ∉ s
⊢ j ≠ i
-- Mathlib/Logic/Equiv/List.lean
theorem list_ofNat_zero : ofNat (List α) 0 = []

Proof state:
α : Type u_1
inst✝ : Denumerable α
⊢ ofNat (List α) 0 = []

Tactic:
rw [← @encode_list_nil α, ofNat_encode]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel (hf : Measurable f) (a : α) {s : Set β}
    (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) :
    ∫⁻ b in s, ∫⁻ ω in t, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a)
      = ∫⁻ x in s ×ˢ t, f x ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a

Tactic:
rw [Kernel.setLIntegral_compProd _ _ _ hf hs ht]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂κ a

Tactic:
conv_rhs => rw [← κ.disintegrate κ.condKernel]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂(κ.fst ⊗ₖ κ.condKernel) a
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem of_boundedUnder_abs_im (hre : Tendsto re l atTop)
    (him : IsBoundedUnder (· ≤ ·) l fun z => |z.im|) : IsExpCmpFilter l :=
  of_isBigO_im_re_pow hre 0 <| by
    simpa only [pow_zero] using him.isBigO_const (f := im) one_ne_zero

Proof state:
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun z => |z.im|
⊢ im =O[l] fun z => z.re ^ 0

Tactic:
simpa only [pow_zero] using him.isBigO_const (f := im) one_ne_zero

Result:
no goals