harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem lt_iff_exists_le {x y : PGame} (ox : x.Numeric) (oy : y.Numeric) :
    x < y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
⊢ x < y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y

Tactic:
rw [← lf_iff_lt ox oy, lf_iff_exists_le]

Result:
no goals
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem dist_le_of_trajectories_ODE_of_mem
    (hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t))
    (hf : ContinuousOn f (Icc a b))
    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t)
    (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
    (hg : ContinuousOn g (Icc a b)) (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
    (hgs : ∀ t ∈ Ico a b, g t ∈ s t) (ha : dist (f a) (g a) ≤ δ) :
    ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ gronwallBound δ (↑K) (0 + 0) (t - a)
⊢ dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))

Tactic:
rwa [zero_add, gronwallBound_ε0] at this

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))

Tactic:
intro t ht

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
⊢ dist (f t) (g t) ≤ δ * rexp (↑K * (t - a))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem mem_insertUnit_fold_units {n : Nat} (units : Array (Literal (PosFin n))) (assignments : Array Assignment)
    (foundContradiction : Bool) (l : CNF.Clause (PosFin n)) :
    let insertUnit_fold_res := List.foldl insertUnit (units, assignments, foundContradiction) l
    ∀ l' : Literal (PosFin n), l' ∈ insertUnit_fold_res.1.toList → l' ∈ l ∨ l' ∈ units.toList

Proof state:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
l'_eq_l'' : l' = l''
⊢ l' ∈ l ∨ l' ∈ units.toList

Tactic:
rw [l'_eq_l'']

Result:
case inl
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
hb : ∀ (l' : Literal (PosFin n)), l' ∈ (units, assignments, foundContradiction).fst.toList → l' ∈ l ∨ l' ∈ units.toList
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
h : ∀ (l' : Literal (PosFin n)), l' ∈ acc.fst.toList → l' ∈ l ∨ l' ∈ units.toList
l'' : Literal (PosFin n)
l''_in_l : l'' ∈ l
l' : Literal (PosFin n)
l'_in_res : l' ∈ (insertUnit acc l'').fst.toList
l'_eq_l'' : l' = l''
⊢ l'' ∈ l ∨ l'' ∈ units.toList

Proof state:
n : Nat
units : Array (Literal (PosFin n))
assignments : Array Assignment
foundContradiction : Bool
l : CNF.Clause (PosFin n)
l' : Literal (PosFin n)
h : l' ∈ (units, assignments, foundContradiction).fst.toList
⊢ l' ∈ l ∨ l' ∈ units.toList

Tactic:
exact Or.inr h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_pos_of_base_lt_one (hx : 0 < x) (hx' : x < 1) : 0 < logb b x

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ x < 1

Tactic:
exact hx'

Result:
no goals

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ 0 < logb b x

Tactic:
rw [logb_pos_iff_of_base_lt_one b_pos b_lt_one hx]

Result:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ x < 1
-- Mathlib/Data/ENNReal/Basic.lean
theorem iUnion_Iio_coe_nat : ⋃ n : ℕ, Iio (n : ℝ≥0∞) = {∞}ᶜ

Proof state:
case h
x : ℝ≥0∞
⊢ x ∈ ⋃ n, Iio ↑n ↔ x ∈ {⊤}ᶜ

Tactic:
rw [mem_iUnion]

Result:
case h
x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {⊤}ᶜ

Proof state:
case h
x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {⊤}ᶜ

Tactic:
exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩

Result:
no goals

Proof state:
⊢ ⋃ n, Iio ↑n = {⊤}ᶜ

Tactic:
ext x

Result:
case h
x : ℝ≥0∞
⊢ x ∈ ⋃ n, Iio ↑n ↔ x ∈ {⊤}ᶜ
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fundamentalDomain_isBounded [Finite ι] [HasSolidNorm K] :
    IsBounded (fundamentalDomain b)

Proof state:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖x‖ ≤ ∑ j : ι, ‖b j‖

Tactic:
rw [← fract_eq_self.mpr hx]

Result:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖fract b x‖ ≤ ∑ j : ι, ‖b j‖

Proof state:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖fract b x‖ ≤ ∑ j : ι, ‖b j‖

Tactic:
apply norm_fract_le

Result:
no goals

Proof state:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ IsBounded (fundamentalDomain b)

Tactic:
refine isBounded_iff_forall_norm_le.2 ⟨∑ j, ‖b j‖, fun x hx ↦ ?_⟩

Result:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖x‖ ≤ ∑ j : ι, ‖b j‖

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
⊢ IsBounded (fundamentalDomain b)

Tactic:
cases nonempty_fintype ι

Result:
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ IsBounded (fundamentalDomain b)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_update (p : R[X]) (n : ℕ) (a : R) [Decidable (a = 0)] :
    support (p.update n a) = if a = 0 then p.support.erase n else insert n p.support

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
cases p

Result:
case ofFinsupp
R : Type u
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ }.update n a).support =
    if a = 0 then { toFinsupp := toFinsupp✝ }.support.erase n else insert n { toFinsupp := toFinsupp✝ }.support

Proof state:
case ofFinsupp
R : Type u
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ }.update n a).support =
    if a = 0 then { toFinsupp := toFinsupp✝ }.support.erase n else insert n { toFinsupp := toFinsupp✝ }.support

Tactic:
simp only [support, update, Finsupp.support_update]

Result:
case ofFinsupp
R : Type u
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : R[ℕ]
⊢ (if a = 0 then toFinsupp✝.support.erase n else insert n toFinsupp✝.support) =
    if a = 0 then toFinsupp✝.support.erase n else insert n toFinsupp✝.support

Proof state:
case ofFinsupp
R : Type u
inst✝¹ : Semiring R
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : R[ℕ]
⊢ (if a = 0 then toFinsupp✝.support.erase n else insert n toFinsupp✝.support) =
    if a = 0 then toFinsupp✝.support.erase n else insert n toFinsupp✝.support

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
classical
  cases p
  simp only [support, update, Finsupp.support_update]
  congr

Result:
no goals
-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem uniformContinuous_extension₂ : UniformContinuous₂ (pkg.extend₂ pkg' f)

Proof state:
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous ((pkg.prod pkg').extend (uncurry f))

Tactic:
apply uniformContinuous_extend

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous₂ (pkg.extend₂ pkg' f)

Tactic:
rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]

Result:
α : Type u_1
inst✝³ : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝² : UniformSpace β
pkg' : AbstractCompletion β
γ : Type u_3
inst✝¹ : UniformSpace γ
f : α → β → γ
inst✝ : CompleteSpace γ
⊢ UniformContinuous ((pkg.prod pkg').extend (uncurry f))
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_even :
    (∫ x in (0)..π, sin x ^ (2 * n)) = π * ∏ i ∈ range n, (2 * (i : ℝ) + 1) / (2 * i + 2)

Proof state:
case zero
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * 0) = π * ∏ i ∈ Finset.range 0, (2 * ↑i + 1) / (2 * ↑i + 2)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / ↑(2 * k + 2) +
      ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Tactic:
simp [-cast_add, field_simps]

Result:
no goals

Proof state:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * (k + 1)) = π * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 1) / (2 * ↑i + 2)

Tactic:
rw [prod_range_succ_comm, mul_left_comm, ← ih, mul_succ, integral_sin_pow]

Result:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Proof state:
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * n) = π * ∏ i ∈ Finset.range n, (2 * ↑i + 1) / (2 * ↑i + 2)

Tactic:
induction' n with k ih

Result:
case zero
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * 0) = π * ∏ i ∈ Finset.range 0, (2 * ↑i + 1) / (2 * ↑i + 2)

case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * (k + 1)) = π * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 1) / (2 * ↑i + 2)

Proof state:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) +
      (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)

Tactic:
norm_cast

Result:
case succ
n k : ℕ
ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)
⊢ (sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / ↑(2 * k + 2) +
      ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) =
    ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
lemma Integrable.piecewise [DecidablePred (· ∈ s)]
    (hs : MeasurableSet s) (hf : IntegrableOn f s μ) (hg : IntegrableOn g sᶜ μ) :
    Integrable (s.piecewise f g) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s : Set α
μ : Measure α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Integrable f (μ.restrict s)
hg : Integrable g (μ.restrict sᶜ)
⊢ Integrable (s.piecewise f g) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hg ⊢

Result:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s : Set α
μ : Measure α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : MemLp f 1 (μ.restrict s)
hg : MemLp g 1 (μ.restrict sᶜ)
⊢ MemLp (s.piecewise f g) 1 μ

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s : Set α
μ : Measure α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ Integrable (s.piecewise f g) μ

Tactic:
rw [IntegrableOn] at hf hg

Result:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s : Set α
μ : Measure α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Integrable f (μ.restrict s)
hg : Integrable g (μ.restrict sᶜ)
⊢ Integrable (s.piecewise f g) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f g : α → E
s : Set α
μ : Measure α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : MemLp f 1 (μ.restrict s)
hg : MemLp g 1 (μ.restrict sᶜ)
⊢ MemLp (s.piecewise f g) 1 μ

Tactic:
exact MemLp.piecewise hs hf hg

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp]
lemma coheight_coe_enat (n : ℕ) : coheight (n : ℕ∞) = ⊤

Proof state:
n : ℕ
⊢ coheight n + 1 = ⊤

Tactic:
simp only [Nat.cast_id, coheight_nat, top_add]

Result:
no goals

Proof state:
n : ℕ
⊢ coheight ↑n = ⊤

Tactic:
apply (coheight_coe_withTop _).trans

Result:
n : ℕ
⊢ coheight n + 1 = ⊤
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_mul [Ring α] (m n) : ((m * n : ZNum) : α) = m * n

Proof state:
α : Type u_1
inst✝ : Ring α
m n : ZNum
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_zero [Nontrivial n] : cramer (0 : Matrix n n α) = 0

Proof state:
case h.h.h.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ (cramer 0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j = (0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j

Tactic:
apply det_eq_zero_of_column_eq_zero j'

Result:
case h.h.h.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), updateCol 0 j ((LinearMap.single α (fun i => α) i) 1) i_1 j' = 0

Proof state:
case h.h.h.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
j'' : n
⊢ updateCol 0 j ((LinearMap.single α (fun i => α) i) 1) j'' j' = 0

Tactic:
simp [updateCol_ne hj']

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
⊢ cramer 0 = 0

Tactic:
ext i j

Result:
case h.h.h
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j : n
⊢ (cramer 0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j = (0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j

Proof state:
case h.h.h.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), updateCol 0 j ((LinearMap.single α (fun i => α) i) 1) i_1 j' = 0

Tactic:
intro j''

Result:
case h.h.h.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
j'' : n
⊢ updateCol 0 j ((LinearMap.single α (fun i => α) i) 1) j'' j' = 0

Proof state:
case h.h.h
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j : n
⊢ (cramer 0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j = (0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j

Tactic:
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j

Result:
case h.h.h.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ (cramer 0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j = (0 ∘ₗ LinearMap.single α (fun i => α) i) 1 j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_reverse (a : α) (l : Array α) : count a l.reverse = count a l

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ count a l.reverse = count a l

Tactic:
cases l

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
toList✝ : List α
⊢ count a { toList := toList✝ }.reverse = count a { toList := toList✝ }

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
toList✝ : List α
⊢ count a { toList := toList✝ }.reverse = count a { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_lt_iff_right (hb : AddLECancellable b) (hba : b ≤ a) :
    a - b < c ↔ a < c + b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
exact hb.tsub_lt_iff_left hba

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < c + b

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMaxOn.fderivWithin_eq_zero (h : IsLocalMaxOn f s a)
    (hy : y ∈ posTangentConeAt s a) (hy' : -y ∈ posTangentConeAt s a) :
    (fderivWithin ℝ f s a : E → ℝ) y = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
exact if hf : DifferentiableWithinAt ℝ f s a then
  h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
classical
exact if hf : DifferentiableWithinAt ℝ f s a then
  h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem single_eq_zero {i : ι} {xi : β i} : single i xi = 0 ↔ xi = 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ i = i ∧ HEq xi 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = 0 ↔ xi = 0

Tactic:
rw [← single_zero i, single_eq_single_iff]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ i = i ∧ HEq xi 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_false {s : False → α} : iSup s = ⊥

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : False → α
⊢ iSup s = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_mul (m n : ℕ∞) : ofENat (m * n) = m * n :=
  toENat_injOn (by simp)
    (aleph0_mul_aleph0 ▸ mul_le_mul' (ofENat_le_aleph0 _) (ofENat_le_aleph0 _)) (by simp)

Proof state:
m n : ℕ∞
⊢ ↑(m * n) ∈ Iic ℵ₀

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ∞
⊢ toENat ↑(m * n) = toENat (↑m * ↑n)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem isLittleO_coe_const_pow_of_one_lt {R : Type*} [NormedRing R] {r : ℝ} (hr : 1 < r) :
    ((↑) : ℕ → R) =o[atTop] fun n ↦ r ^ n

Proof state:
R : Type u_2
inst✝ : NormedRing R
r : ℝ
hr : 1 < r
⊢ Nat.cast =o[atTop] fun n => r ^ n

Tactic:
simpa only [pow_one] using @isLittleO_pow_const_const_pow_of_one_lt R _ 1 _ hr

Result:
no goals