harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_eq_empty_iff [LawfulBEq α] {xs : Array α} {a : α} :
    xs.erase a = #[] ↔ xs = #[] ∨ xs = #[a]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : Array α
a : α
⊢ xs.erase a = #[] ↔ xs = #[] ∨ xs = #[a]

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
xs : List α
⊢ { toList := xs }.erase a = #[] ↔ { toList := xs } = #[] ∨ { toList := xs } = #[a]

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
xs : List α
⊢ { toList := xs }.erase a = #[] ↔ { toList := xs } = #[] ∨ { toList := xs } = #[a]

Tactic:
simp [List.erase_eq_nil_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem edist_comm (f g : PiLp p β) : edist f g = edist g f

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
⊢ edist f g = edist g f

Tactic:
rcases p.trichotomy with (rfl | rfl | h)

Result:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp 0 β
⊢ edist f g = edist g f

case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ⊤ β
⊢ edist f g = edist g f

case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < p.toReal
⊢ edist f g = edist g f

Proof state:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp 0 β
⊢ edist f g = edist g f

Tactic:
simp only [edist_eq_card, edist_comm]

Result:
no goals

Proof state:
case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
simp only [edist_eq_sum h, edist_comm]

Result:
no goals

Proof state:
case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ⊤ β
⊢ edist f g = edist g f

Tactic:
simp only [edist_eq_iSup, edist_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/ZPow.lean
theorem iter_deriv_pow (n : ℕ) (x : 𝕜) (k : ℕ) :
    deriv^[k] (fun x : 𝕜 => x ^ n) x = (∏ i ∈ Finset.range k, ((n : 𝕜) - i)) * x ^ (n - k)

Proof state:
case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

Tactic:
have : (∏ i ∈ Finset.range k, (n - i : 𝕜)) = 0 :=
  Finset.prod_eq_zero (Finset.mem_range.2 hnk) (sub_self _)

Result:
case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
this : ∏ i ∈ Finset.range k, (↑n - ↑i) = 0
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

Proof state:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

Tactic:
rw [Int.ofNat_sub hkn]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

Tactic:
rcases le_or_lt k n with hkn | hnk

Result:
case inl
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hkn : k ≤ n
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

Proof state:
case inr
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
hnk : n < k
this : ∏ i ∈ Finset.range k, (↑n - ↑i) = 0
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)

Tactic:
simp only [this, zero_mul]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
⊢ deriv^[k] (fun x => x ^ n) x = (∏ i ∈ Finset.range k, (↑n - ↑i)) * x ^ (n - k)

Tactic:
simp only [← zpow_natCast, iter_deriv_zpow, Int.cast_natCast]

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
k : ℕ
⊢ (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ (↑n - ↑k) = (∏ x ∈ Finset.range k, (↑n - ↑x)) * x ^ ↑(n - k)
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem support_single_mul [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k)
    (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
    (single x r * f : MonoidAlgebra k G).support = f.support.map (mulLeftEmbedding x)

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
classical
  ext
  simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
    mem_map, mulLeftEmbedding_apply]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
ext

Result:
case h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (single x r * f).support ↔ a✝ ∈ map (mulLeftEmbedding x) f.support

Proof state:
case h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : MonoidAlgebra k G
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (single x r * f).support ↔ a✝ ∈ map (mulLeftEmbedding x) f.support

Tactic:
simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
  mem_map, mulLeftEmbedding_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_vsub_const_eq_weightedVSubOfPoint_sub (w : ι → k) (p₁ : ι → P) (p₂ b : P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.weightedVSubOfPoint p₁ b w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ : ι → P
p₂ b : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSubOfPoint p₁ b) w - (∑ i ∈ s, w i) • (p₂ -ᵥ b)

Tactic:
rw [sum_smul_vsub_eq_weightedVSubOfPoint_sub, weightedVSubOfPoint_apply_const]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean
lemma exact₂ :
    (ShortComplex.mk ((homologyFunctor C n₀).map T.mor₁) ((homologyFunctor C n₀).map T.mor₂)
      (by simp only [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT,
        Functor.map_zero])).Exact :=
  (homologyFunctor C 0).homologySequence_exact₂ _ hT _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctor C n₀).map T.mor₁ ≫ (homologyFunctor C n₀).map T.mor₂ = 0

Tactic:
simp only [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT,
Functor.map_zero]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_eq_ofScalarsSum : exp 𝕂 = ofScalarsSum (E := 𝔸) fun n ↦ (n !⁻¹ : 𝕂)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ exp 𝕂 = ofScalarsSum fun n => (↑n !)⁻¹

Tactic:
rw [exp_eq_tsum, ofScalarsSum_eq_tsum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_some_of_exists {xs : Array α} {p : α → Bool} (h : ∃ x, x ∈ xs ∧ p x) :
    xs.findIdx? p = some (xs.findIdx p)

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx? p xs = some (findIdx p xs)

Tactic:
rw [findIdx?_eq_some_iff_findIdx_eq]

Result:
α : Type u_1
xs : Array α
p : α → Bool
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs < xs.size ∧ findIdx p xs = findIdx p xs

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs < xs.size ∧ findIdx p xs = findIdx p xs

Tactic:
exact ⟨findIdx_lt_size_of_exists h, rfl⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem recDiag_succ_zero {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m) :
    Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m+1) 0
      = succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0)

Proof state:
motive : Nat → Nat → Sort u_1
zero_zero : motive 0 0
zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)
succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
m : Nat
⊢ Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) 0 =
    succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0)

Tactic:
simp [Nat.recDiag]

Result:
motive : Nat → Nat → Sort u_1
zero_zero : motive 0 0
zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)
succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
m : Nat
⊢ Nat.recDiagAux (recDiag.left zero_zero zero_succ) (recDiag.right zero_zero succ_zero) succ_succ (m + 1) 0 =
    succ_zero m (Nat.recDiagAux (recDiag.left zero_zero zero_succ) (recDiag.right zero_zero succ_zero) succ_succ m 0)

Proof state:
motive : Nat → Nat → Sort u_1
zero_zero : motive 0 0
zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)
succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
m : Nat
⊢ Nat.recDiagAux (recDiag.left zero_zero zero_succ) (recDiag.right zero_zero succ_zero) succ_succ (m + 1) 0 =
    succ_zero m (Nat.recDiagAux (recDiag.left zero_zero zero_succ) (recDiag.right zero_zero succ_zero) succ_succ m 0)

Tactic:
cases m <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem forall_measure_inter_spanningSets_eq_zero [MeasurableSpace α] {μ : Measure α}
    [SigmaFinite μ] (s : Set α) : (∀ n, μ (s ∩ spanningSets μ n) = 0) ↔ μ s = 0

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ s = ⋃ n, s ∩ spanningSets μ n

Tactic:
rw [← inter_iUnion, iUnion_spanningSets, inter_univ]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), μ (s ∩ spanningSets μ n) = 0) ↔ μ s = 0

Tactic:
nth_rw 2 [show s = ⋃ n, s ∩ spanningSets μ n by
    rw [← inter_iUnion, iUnion_spanningSets, inter_univ] ]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), μ (s ∩ spanningSets μ n) = 0) ↔ μ (⋃ n, s ∩ spanningSets μ n) = 0

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), μ (s ∩ spanningSets μ n) = 0) ↔ μ (⋃ n, s ∩ spanningSets μ n) = 0

Tactic:
rw [measure_iUnion_null_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_of_tendsto_eLpNorm {l : Filter ι} (hp_ne_zero : p ≠ 0)
    (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : AEStronglyMeasurable g μ)
    (hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)) : TendstoInMeasure μ f l g

Proof state:
case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ⊤
⊢ TendstoInMeasure μ f l g

Tactic:
subst hp_ne_top

Result:
case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hp_ne_zero : ⊤ ≠ 0
hfg : Tendsto (fun n => eLpNorm (f n - g) ⊤ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Proof state:
case neg
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ⊤
⊢ TendstoInMeasure μ f l g

Tactic:
exact tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top hp_ne_zero hp_ne_top hf hg hfg

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
by_cases hp_ne_top : p = ∞

Result:
case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ⊤
⊢ TendstoInMeasure μ f l g

case neg
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ⊤
⊢ TendstoInMeasure μ f l g

Proof state:
case pos
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hp_ne_zero : ⊤ ≠ 0
hfg : Tendsto (fun n => eLpNorm (f n - g) ⊤ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
exact tendstoInMeasure_of_tendsto_eLpNorm_top hfg

Result:
no goals
-- Mathlib/AlgebraicGeometry/Limits.lean
lemma coprodSpec_apply (x) :
    (coprodSpec R S).base x = (PrimeSpectrum.primeSpectrumProd R S).symm
      ((coprodMk (Spec (.of R)) (Spec (.of S))).symm x)

Proof state:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↑↑(Spec (CommRingCat.of R) ⨿ Spec (CommRingCat.of S)).toPresheafedSpace
⊢ (ConcreteCategory.hom (coprodSpec R S).base) x =
    (PrimeSpectrum.primeSpectrumProd R S).symm ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))).symm x)

Tactic:
rw [← coprodSpec_coprodMk, Homeomorph.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem rootMultiplicity_sub_one_le_derivative_rootMultiplicity [CharZero R] (p : R[X]) (t : R) :
    p.rootMultiplicity t - 1 ≤ p.derivative.rootMultiplicity t

Proof state:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

Tactic:
exact (derivative_rootMultiplicity_of_root h).symm.le

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

Tactic:
by_cases h : p.IsRoot t

Result:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

Proof state:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬p.IsRoot t
⊢ 0 ≤ rootMultiplicity t (derivative p)

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬p.IsRoot t
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t (derivative p)

Tactic:
rw [rootMultiplicity_eq_zero h, zero_tsub]

Result:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
h : ¬p.IsRoot t
⊢ 0 ≤ rootMultiplicity t (derivative p)
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_rel_mulIndicator {r : M → M → Prop} (h1 : r 1 1) (ha : a ∈ s → r (f a) (g a)) :
    r (mulIndicator s f a) (mulIndicator s g a)

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (s.mulIndicator f a) (s.mulIndicator g a)

Tactic:
simp only [mulIndicator]

Result:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)

Tactic:
split_ifs with has

Result:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∉ s
⊢ r 1 1

Proof state:
case pos
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∈ s
⊢ r (f a) (g a)

case neg
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
has : a ∉ s
⊢ r 1 1

Tactic:
exacts [ha has, h1]

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
/-- A linear endomorphism is semisimple if every invariant submodule has in invariant complement.

See also `Module.End.isSemisimple_iff`. -/
lemma isSemisimple_iff' :
    f.IsSemisimple ↔ ∀ p : invtSubmodule f, ∃ q : invtSubmodule f, IsCompl p q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ (∀ (a : ↥((Algebra.lsmul R R M) f).invtSubmodule), ∃ b, IsCompl a b) ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ f.IsSemisimple ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q

Tactic:
rw [IsSemisimple, IsSemisimpleModule, (AEval.mapSubmodule R M f).symm.complementedLattice_iff,
  complementedLattice_iff]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ (∀ (a : ↥((Algebra.lsmul R R M) f).invtSubmodule), ∃ b, IsCompl a b) ↔ ∀ (p : ↥f.invtSubmodule), ∃ q, IsCompl p q
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem range_const (α) [MeasurableSpace α] [Nonempty α] (b : β) : (const α b).range = {b} :=
  Finset.coe_injective <| by simp (config := { unfoldPartialApp := true }) [Function.const]

Proof state:
β : Type u_2
α : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : Nonempty α
b : β
⊢ ↑(const α b).range = ↑{b}

Tactic:
simp (config := { unfoldPartialApp := true }) [Function.const]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem aeval_eq (p : R[X]) : aeval (root f) p = mk f p :=
  Polynomial.induction_on p
    (fun x => by
      rw [aeval_C]
      rfl)
    (fun p q ihp ihq => by rw [map_add, RingHom.map_add, ihp, ihq]) fun n x _ => by
    rw [_root_.map_mul, aeval_C, map_pow, aeval_X, RingHom.map_mul, mk_C, RingHom.map_pow, mk_X]
    rfl

Proof state:
R : Type u
inst✝ : CommRing R
f p : R[X]
x : R
⊢ (aeval (root f)) (C x) = (mk f) (C x)

Tactic:
rw [aeval_C]

Result:
R : Type u
inst✝ : CommRing R
f p : R[X]
x : R
⊢ (algebraMap R (AdjoinRoot f)) x = (mk f) (C x)

Proof state:
R : Type u
inst✝ : CommRing R
f p : R[X]
x : R
⊢ (algebraMap R (AdjoinRoot f)) x = (mk f) (C x)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f p✝ p q : R[X]
ihp : (aeval (root f)) p = (mk f) p
ihq : (aeval (root f)) q = (mk f) q
⊢ (aeval (root f)) (p + q) = (mk f) (p + q)

Tactic:
rw [map_add, RingHom.map_add, ihp, ihq]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : (aeval (root f)) (C x * X ^ n) = (mk f) (C x * X ^ n)
⊢ (aeval (root f)) (C x * X ^ (n + 1)) = (mk f) (C x * X ^ (n + 1))

Tactic:
rw [_root_.map_mul, aeval_C, map_pow, aeval_X, RingHom.map_mul, mk_C, RingHom.map_pow, mk_X]

Result:
R : Type u
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : (aeval (root f)) (C x * X ^ n) = (mk f) (C x * X ^ n)
⊢ (algebraMap R (AdjoinRoot f)) x * root f ^ (n + 1) = (of f) x * root f ^ (n + 1)

Proof state:
R : Type u
inst✝ : CommRing R
f p : R[X]
n : ℕ
x : R
x✝ : (aeval (root f)) (C x * X ^ n) = (mk f) (C x * X ^ n)
⊢ (algebraMap R (AdjoinRoot f)) x * root f ^ (n + 1) = (of f) x * root f ^ (n + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem lcm_mul_left [NormalizedGCDMonoid α] (a b c : α) :
    lcm (a * b) (a * c) = normalize a * lcm b c :=
  (by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero]))
    fun ha : a ≠ 0 =>
    suffices lcm (a * b) (a * c) = normalize (a * lcm b c) by simpa
    have : a ∣ lcm (a * b) (a * c) := (dvd_mul_right _ _).trans (dvd_lcm_left _ _)
    let ⟨_, eq⟩ := this
    lcm_eq_normalize
      (lcm_dvd (mul_dvd_mul_left a (dvd_lcm_left _ _)) (mul_dvd_mul_left a (dvd_lcm_right _ _)))
      (eq.symm ▸
        (mul_dvd_mul_left a <|
          lcm_dvd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_left _ _)
            ((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_right _ _)))

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
ha : a ≠ 0
this : lcm (a * b) (a * c) = normalize (a * lcm b c)
⊢ lcm (a * b) (a * c) = normalize a * lcm b c

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
b c : α
⊢ lcm (0 * b) (0 * c) = normalize 0 * lcm b c

Tactic:
simp only [zero_mul, lcm_zero_left, normalize_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b c : α
⊢ a = 0 → lcm (a * b) (a * c) = normalize a * lcm b c

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
b c : α
⊢ lcm (0 * b) (0 * c) = normalize 0 * lcm b c
-- Mathlib/Order/SymmDiff.lean
theorem Disjoint.le_symmDiff_sup_symmDiff_left (h : Disjoint a b) : c ≤ a ∆ c ⊔ b ∆ c

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ a ∆ c ⊔ b ∆ c

Tactic:
trans c \ (a ⊓ b)

Result:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)

α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c

Tactic:
exact sup_le_sup le_sup_right le_sup_right

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)

Tactic:
rw [h.eq_bot, sdiff_bot]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c

Tactic:
rw [sdiff_inf]

Result:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c