harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.insertEntryIfNew [BEq α] [PartialEquivBEq α] {k : α} {v : β k}
    {l : List ((a : α) × β a)} (h: DistinctKeys l):
    DistinctKeys (insertEntryIfNew k v l)

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h✝ : ¬containsKey k l = true
⊢ DistinctKeys l ∧ containsKey k l = false

Tactic:
rename_i h'

Result:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h' : ¬containsKey k l = true
⊢ DistinctKeys l ∧ containsKey k l = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
⊢ DistinctKeys (if containsKey k l = true then l else ⟨k, v⟩ :: l)

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h✝ : containsKey k l = true
⊢ DistinctKeys l

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h✝ : ¬containsKey k l = true
⊢ DistinctKeys (⟨k, v⟩ :: l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
⊢ DistinctKeys (List.insertEntryIfNew k v l)

Tactic:
simp only [Std.DHashMap.Internal.List.insertEntryIfNew, cond_eq_if]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
⊢ DistinctKeys (if containsKey k l = true then l else ⟨k, v⟩ :: l)

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h' : ¬containsKey k l = true
⊢ DistinctKeys l ∧ containsKey k l = false

Tactic:
simp [h, h']

Result:
no goals

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h✝ : containsKey k l = true
⊢ DistinctKeys l

Tactic:
exact h

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h✝ : ¬containsKey k l = true
⊢ DistinctKeys (⟨k, v⟩ :: l)

Tactic:
rw [distinctKeys_cons_iff]

Result:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
v : β k
l : List ((a : α) × β a)
h : DistinctKeys l
h✝ : ¬containsKey k l = true
⊢ DistinctKeys l ∧ containsKey k l = false
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.left_ne_right_iff_radius_pos (h : s.IsDiameter p₁ p₂) :
    p₁ ≠ p₂ ↔ 0 < s.radius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ s.radius ≠ 0 ↔ 0 ≤ s.radius ∧ 0 ≠ s.radius

Tactic:
simp [radius_nonneg_of_mem h.left_mem, eq_comm]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ p₁ ≠ p₂ ↔ 0 < s.radius

Tactic:
rw [h.left_ne_right_iff_radius_ne_zero, lt_iff_le_and_ne]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ s.radius ≠ 0 ↔ 0 ≤ s.radius ∧ 0 ≠ s.radius
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem index_empty {V : Set G} : index ∅ V = 0

Proof state:
G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} ∨
    Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} = ∅

Tactic:
left

Result:
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Proof state:
G : Type u_1
inst✝ : Group G
V : Set G
⊢ index ∅ V = 0

Tactic:
simp only [index, Nat.sInf_eq_zero]

Result:
G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} ∨
    Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} = ∅

Proof state:
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ ∅ ∈ {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} ∧ ∅.card = 0

Tactic:
simp only [Finset.card_empty, empty_subset, mem_setOf_eq, eq_self_iff_true, and_self_iff]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Tactic:
use ∅

Result:
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ ∅ ∈ {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} ∧ ∅.card = 0
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsOpen.mul_right (hs : IsOpen s) : IsOpen (s * t)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (op '' t • s)

Tactic:
exact hs.smul_left

Result:
no goals

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (s * t)

Tactic:
rw [← image_op_smul]

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen s
⊢ IsOpen (op '' t • s)
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.disjoint_iff_left (h : l.HasBasis p s) :
    Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'

Proof state:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'

Tactic:
simp only [h.disjoint_iff l'.basis_sets, id, ← disjoint_principal_left,
  (hasBasis_principal _).disjoint_iff l'.basis_sets, true_and, Unique.exists_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem HasFiniteIntegral.tendsto_setIntegral_nhds_zero {ι} {f : α → G}
    (hf : HasFiniteIntegral f μ) {l : Filter ι} {s : ι → Set α} (hs : Tendsto (μ ∘ s) l (𝓝 0)) :
    Tendsto (fun i => ∫ x in s i, f x ∂μ) l (𝓝 0)

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun a => ↑‖∫ (x : α) in s a, f x ∂μ‖₊) l (𝓝 0)

Tactic:
exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
  (tendsto_setLIntegral_zero (ne_of_lt hf) hs) (fun i => zero_le _)
  fun i => enorm_integral_le_lintegral_enorm _

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun x => ‖∫ (x : α) in s x, f x ∂μ‖) l (𝓝 0)

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun x => ‖∫ (x : α) in s x, f x ∂μ‖) l (𝓝 0)

Tactic:
simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe,
  ENNReal.coe_zero]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hf : HasFiniteIntegral f μ
l : Filter ι
s : ι → Set α
hs : Tendsto (⇑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun a => ↑‖∫ (x : α) in s a, f x ∂μ‖₊) l (𝓝 0)
-- Mathlib/Algebra/Field/Periodic.lean
theorem Antiperiodic.add_nat_mul_eq [Semiring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
    f (x + n * c) = (-1) ^ n * f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : Semiring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (x + ↑n * c) = (-1) ^ n * f x

Tactic:
simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
  Int.cast_one] using h.add_nsmul_eq n

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem Intersecting.exists_card_eq (hs : (s : Set α).Intersecting) :
    ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (t : Set α).Intersecting

Proof state:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
this : #s ≤ Fintype.card α / 2
⊢ ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Tactic:
revert hs

Result:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
this : #s ≤ Fintype.card α / 2
⊢ (↑s).Intersecting → ∃ t, s ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting

Proof state:
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * #t ≤ Fintype.card α

Tactic:
exact ht.card_le

Result:
no goals

Proof state:
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ #t ≤ Fintype.card α / 2

Tactic:
rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_comm]

Result:
case neg.intro.intro
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * #t ≤ Fintype.card α
-- Mathlib/CategoryTheory/Limits/Types.lean
theorem colimitEquivQuot_apply (j : J) (x : F.obj j) :
    (colimitEquivQuot F) (colimit.ι F j x) = Quot.mk _ ⟨j, x⟩

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivQuot F) (colimit.ι F j x) = Quot.mk (Quot.Rel F) ⟨j, x⟩

Tactic:
apply (colimitEquivQuot F).symm.injective

Result:
case a
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivQuot F).symm ((colimitEquivQuot F) (colimit.ι F j x)) =
    (colimitEquivQuot F).symm (Quot.mk (Quot.Rel F) ⟨j, x⟩)

Proof state:
case a
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j : J
x : F.obj j
⊢ (colimitEquivQuot F).symm ((colimitEquivQuot F) (colimit.ι F j x)) =
    (colimitEquivQuot F).symm (Quot.mk (Quot.Rel F) ⟨j, x⟩)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem dotProduct_cons (v : Fin n.succ → α) (x : α) (w : Fin n → α) :
    dotProduct v (vecCons x w) = vecHead v * x + dotProduct (vecTail v) w

Proof state:
α : Type u
n : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
v : Fin n.succ → α
x : α
w : Fin n → α
⊢ v ⬝ᵥ vecCons x w = vecHead v * x + vecTail v ⬝ᵥ w

Tactic:
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem empty_vecAppend (v : Fin n → α) : vecAppend n.zero_add.symm ![] v = v

Proof state:
case h
α : Type u
n : ℕ
v : Fin n → α
x✝ : Fin n
⊢ vecAppend ⋯ ![] v x✝ = v x✝

Tactic:
simp [vecAppend_eq_ite]

Result:
no goals

Proof state:
α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ ![] v = v

Tactic:
ext

Result:
case h
α : Type u
n : ℕ
v : Fin n → α
x✝ : Fin n
⊢ vecAppend ⋯ ![] v x✝ = v x✝
-- Mathlib/Algebra/Group/AddChar.lean
theorem pow_mulShift (ψ : AddChar R M) (n : ℕ) : ψ ^ n = mulShift ψ n

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ ^ n) x = (ψ.mulShift ↑n) x

Tactic:
rw [pow_apply, ← mulShift_spec']

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
⊢ ψ ^ n = ψ.mulShift ↑n

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ ^ n) x = (ψ.mulShift ↑n) x
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_compLp_le (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : Lp E p μ) :
    ‖hg.compLp g0 f‖ ≤ c * ‖f‖

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f : ↥(Lp E p μ)
⊢ ‖hg.compLp g0 f‖ ≤ ↑c * ‖f‖

Tactic:
simpa only [compLp_zero, sub_zero] using hg.norm_compLp_sub_le g0 f 0

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem mem_ofSet_self_iff {s : Set α} [DecidablePred (· ∈ s)] {a : α} : a ∈ ofSet s a ↔ a ∈ s

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s

Tactic:
split_ifs <;> simp [*]

Result:
no goals

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ a ∈ (ofSet s) a ↔ a ∈ s

Tactic:
dsimp [ofSet]

Result:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
⊢ (a ∈ if a ∈ s then some a else none) ↔ a ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_dvd_tdiv : ∀ {a b c : Int}, a ∣ b → b ∣ c → b.tdiv a ∣ c.tdiv a
  | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ => by
    by_cases az : a = 0
    · simp [az]
    · rw [Int.mul_tdiv_cancel_left _ az, Int.mul_assoc, Int.mul_tdiv_cancel_left _ az]
      apply Int.dvd_mul_right

Proof state:
case neg
a b c : Int
az : ¬a = 0
⊢ (a * b).tdiv a ∣ (a * b * c).tdiv a

Tactic:
rw [Int.mul_tdiv_cancel_left _ az, Int.mul_assoc, Int.mul_tdiv_cancel_left _ az]

Result:
case neg
a b c : Int
az : ¬a = 0
⊢ b ∣ b * c

Proof state:
a b c : Int
⊢ (a * b).tdiv a ∣ (a * b * c).tdiv a

Tactic:
by_cases az : a = 0

Result:
case pos
a b c : Int
az : a = 0
⊢ (a * b).tdiv a ∣ (a * b * c).tdiv a

case neg
a b c : Int
az : ¬a = 0
⊢ (a * b).tdiv a ∣ (a * b * c).tdiv a

Proof state:
case neg
a b c : Int
az : ¬a = 0
⊢ b ∣ b * c

Tactic:
apply Int.dvd_mul_right

Result:
no goals

Proof state:
case pos
a b c : Int
az : a = 0
⊢ (a * b).tdiv a ∣ (a * b * c).tdiv a

Tactic:
simp [az]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem C_mul_prod_X_sub_C_eq [CommRing S] {w x y z : S} :
    C w * (X - C x) * (X - C y) * (X - C z) =
      toPoly ⟨w, w * -(x + y + z), w * (x * y + x * z + y * z), w * -(x * y * z)⟩

Proof state:
S : Type u_2
inst✝ : CommRing S
w x y z : S
⊢ C w * (X - C x) * (X - C y) * (X - C z) =
    { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly

Tactic:
simp only [toPoly, C_neg, C_add, C_mul]

Result:
S : Type u_2
inst✝ : CommRing S
w x y z : S
⊢ C w * (X - C x) * (X - C y) * (X - C z) =
    C w * X ^ 3 + C w * -(C x + C y + C z) * X ^ 2 + C w * (C x * C y + C x * C z + C y * C z) * X +
      C w * -(C x * C y * C z)

Proof state:
S : Type u_2
inst✝ : CommRing S
w x y z : S
⊢ C w * (X - C x) * (X - C y) * (X - C z) =
    C w * X ^ 3 + C w * -(C x + C y + C z) * X ^ 2 + C w * (C x * C y + C x * C z + C y * C z) * X +
      C w * -(C x * C y * C z)

Tactic:
ring1

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem Measurable.dite [∀ x, Decidable (x ∈ s)] {f : s → β} (hf : Measurable f)
    {g : (sᶜ : Set α) → β} (hg : Measurable g) (hs : MeasurableSet s) :
    Measurable fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩ :=
  measurable_of_restrict_of_restrict_compl hs (by simpa) (by simpa)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : Measurable f
g : ↑sᶜ → β
hg : Measurable g
hs : MeasurableSet s
⊢ Measurable (s.restrict fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : (x : α) → Decidable (x ∈ s)
f : ↑s → β
hf : Measurable f
g : ↑sᶜ → β
hg : Measurable g
hs : MeasurableSet s
⊢ Measurable (sᶜ.restrict fun x => if hx : x ∈ s then f ⟨x, hx⟩ else g ⟨x, hx⟩)

Tactic:
simpa

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_indicator_const₀ (hs : NullMeasurableSet s μ) (hp : p ≠ 0) (hp_top : p ≠ ∞) :
    eLpNorm (s.indicator fun _ => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal) :=
  have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp hp_top
  calc
    eLpNorm (s.indicator fun _ => c) p μ
      = (∫⁻ x, (‖(s.indicator fun _ ↦ c) x‖ₑ ^ p.toReal) ∂μ) ^ (1 / p.toReal) :=
          eLpNorm_eq_lintegral_rpow_enorm hp hp_top
    _ = (∫⁻ x, (s.indicator fun _ ↦ ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal)

Proof state:
case e_a.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ (fun x => ‖x‖ₑ ^ p.toReal) 0 = 0

Tactic:
simp [hp_pos]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ (∫⁻ (x : α), s.indicator (fun x => ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal) = ‖c‖ₑ * μ s ^ (1 / p.toReal)

Tactic:
rw [lintegral_indicator_const₀ hs, ENNReal.mul_rpow_of_nonneg, ← ENNReal.rpow_mul,
  mul_one_div_cancel hp_pos.ne', ENNReal.rpow_one]

Result:
case hz
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Proof state:
case e_a.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ (fun x => ‖s.indicator (fun x => c) x‖ₑ ^ p.toReal) = fun x => s.indicator (fun x => ‖c‖ₑ ^ p.toReal) x

Tactic:
refine (Set.comp_indicator_const c (fun x ↦ (‖x‖ₑ) ^ p.toReal) ?_)

Result:
case e_a.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ (fun x => ‖x‖ₑ ^ p.toReal) 0 = 0

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ (∫⁻ (x : α), ‖s.indicator (fun x => c) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), s.indicator (fun x => ‖c‖ₑ ^ p.toReal) x ∂μ) ^ (1 / p.toReal)

Tactic:
congr 2

Result:
case e_a.e_f
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ (fun x => ‖s.indicator (fun x => c) x‖ₑ ^ p.toReal) = fun x => s.indicator (fun x => ‖c‖ₑ ^ p.toReal) x

Proof state:
case hz
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
s : Set α
c : F
hs : NullMeasurableSet s μ
hp : p ≠ 0
hp_top : p ≠ ⊤
hp_pos : 0 < p.toReal
⊢ 0 ≤ 1 / p.toReal

Tactic:
positivity

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_adjoin_le {A : Type u} [Semiring A] [Algebra R A] (s : Set A) :
    #(adjoin R s) ≤ #R ⊔ #s ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type u
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ #↥(adjoin R s) ≤ #R ⊔ #↑s ⊔ ℵ₀

Tactic:
simpa using lift_cardinalMk_adjoin_le R s

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
/-- This expresses the difference between the values of a multilinear map
at two points "close to `x`" in terms of the "derivative" of the multilinear map at `x`
and of "second-order" terms. -/
lemma map_add_sub_map_add_sub_linearDeriv [DecidableEq ι] [Fintype ι] (x h h' : (i : ι) → M₁ i) :
    f (x + h) - f (x + h') - f.linearDeriv x (h - h') =
    ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x))

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h h' : (i : ι) → M₁ i
⊢ f (x + h) - f (x + h') - (f.linearDeriv x) (h - h') =
    ∑ s ∈ filter (fun s => 2 ≤ #s) Finset.univ, (f (s.piecewise h x) - f (s.piecewise h' x))

Tactic:
simp_rw [map_add_eq_map_add_linearDeriv_add, add_assoc, add_sub_add_comm, sub_self, zero_add,
  ← LinearMap.map_sub, add_sub_cancel_left, sum_sub_distrib]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem le_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f)
    (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hx : 0 < x) (hx' : x ≤ 1) (n : ℕ) :
    f x ≤ f 1 + x * log (n + 1) - x * log n + logGammaSeq x n

Proof state:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f (↑(n + 1) + x) ≤ f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)

Tactic:
refine (f_add_nat_le hf_conv (@hf_feq) (Nat.add_one_ne_zero n) hx hx').trans (le_of_eq ?_)

Result:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f ↑(n + 1) + x * log ↑(n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)

Proof state:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f 1 + log ↑n ! + x * log (↑n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)

Tactic:
ring

Result:
no goals

Proof state:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f ↑(n + 1) + x * log ↑(n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)

Tactic:
rw [f_nat_eq @hf_feq (by omega : n + 1 ≠ 0), Nat.add_sub_cancel, Nat.cast_add_one]

Result:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f 1 + log ↑n ! + x * log (↑n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)

Proof state:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f x ≤ f 1 + x * log (↑n + 1) - x * log ↑n + logGammaSeq x n

Tactic:
rw [logGammaSeq, ← add_sub_assoc, le_sub_iff_add_le, ← f_add_nat_eq (@hf_feq) hx, add_comm x]

Result:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f (↑(n + 1) + x) ≤ f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
    l.map f = replicate l.length b ↔ ∀ x ∈ l, f x = b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
b : β
⊢ map f l = replicate l.length b ↔ ∀ (x : α), x ∈ l → f x = b

Tactic:
simp [eq_replicate_iff]

Result:
no goals