harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/Instances/Real.lean
theorem EuclideanQuadrant.convex :
    Convex ℝ { x : EuclideanSpace ℝ (Fin n) | ∀ i, 0 ≤ x i } :=
  fun _ hx _ hy _ _ _ _ _ i ↦ by dsimp at hx hy ⊢; specialize hx i; specialize hy i; positivity

Proof state:
n : ℕ
x✝⁶ x✝⁵ : EuclideanSpace ℝ (Fin n)
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
hx : 0 ≤ x✝⁶ i
hy : 0 ≤ x✝⁵ i
⊢ 0 ≤ x✝⁴ * x✝⁶ i + x✝³ * x✝⁵ i

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : ∀ (i : Fin n), 0 ≤ x✝⁶ i
x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x✝⁵ i
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
⊢ 0 ≤ x✝⁴ * x✝⁶ i + x✝³ * x✝⁵ i

Tactic:
specialize hx i

Result:
n : ℕ
x✝⁶ x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x✝⁵ i
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
hx : 0 ≤ x✝⁶ i
⊢ 0 ≤ x✝⁴ * x✝⁶ i + x✝³ * x✝⁵ i

Proof state:
n : ℕ
x✝⁶ x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x✝⁵ i
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
hx : 0 ≤ x✝⁶ i
⊢ 0 ≤ x✝⁴ * x✝⁶ i + x✝³ * x✝⁵ i

Tactic:
specialize hy i

Result:
n : ℕ
x✝⁶ x✝⁵ : EuclideanSpace ℝ (Fin n)
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
hx : 0 ≤ x✝⁶ i
hy : 0 ≤ x✝⁵ i
⊢ 0 ≤ x✝⁴ * x✝⁶ i + x✝³ * x✝⁵ i

Proof state:
n : ℕ
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : x✝⁶ ∈ {x | ∀ (i : Fin n), 0 ≤ x i}
x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : x✝⁵ ∈ {x | ∀ (i : Fin n), 0 ≤ x i}
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
⊢ 0 ≤ (x✝⁴ • x✝⁶ + x✝³ • x✝⁵) i

Tactic:
dsimp at hx hy ⊢

Result:
n : ℕ
x✝⁶ : EuclideanSpace ℝ (Fin n)
hx : ∀ (i : Fin n), 0 ≤ x✝⁶ i
x✝⁵ : EuclideanSpace ℝ (Fin n)
hy : ∀ (i : Fin n), 0 ≤ x✝⁵ i
x✝⁴ x✝³ : ℝ
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
i : Fin n
⊢ 0 ≤ x✝⁴ * x✝⁶ i + x✝³ * x✝⁵ i
-- Mathlib/Algebra/Lie/Submodule.lean
theorem iSup_toSubmodule {ι} (p : ι → LieSubmodule R L M) :
    (↑(⨆ i, p i) : Submodule R M) = ⨆ i, (p i : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨆ i, p i) = ⨆ i, ↑(p i)

Tactic:
rw [iSup, sSup_toSubmodule]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ sSup {x | ∃ s ∈ range fun i => p i, ↑s = x} = ⨆ i, ↑(p i)

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x✝ : M
⊢ x✝ ∈ sSup {x | ∃ s ∈ range fun i => p i, ↑s = x} ↔ x✝ ∈ ⨆ i, ↑(p i)

Tactic:
simp [Submodule.mem_sSup, Submodule.mem_iSup]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ sSup {x | ∃ s ∈ range fun i => p i, ↑s = x} = ⨆ i, ↑(p i)

Tactic:
ext

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x✝ : M
⊢ x✝ ∈ sSup {x | ∃ s ∈ range fun i => p i, ↑s = x} ↔ x✝ ∈ ⨆ i, ↑(p i)
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_mul_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
    (s : Finset ι) {g : α →  ℝ≥0∞} {f : ι → α → ℝ≥0∞} (hg : AEMeasurable g μ)
    (hf : ∀ i ∈ s, AEMeasurable (f i) μ) (q : ℝ) {p : ι → ℝ} (hpq : q + ∑ i ∈ s, p i = 1)
    (hq :  0 ≤ q) (hp : ∀ i ∈ s, 0 ≤ p i) :
    ∫⁻ a, g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤
      (∫⁻ a, g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ a, f i a ∂μ) ^ p i

Proof state:
case refine_1
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∀ i ∈ insertNone s, AEMeasurable (fun t => i.elim (g t) fun j => f j t) μ

Tactic:
rintro (_|i) hi

Result:
case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
hi : none ∈ insertNone s
⊢ AEMeasurable (fun t => none.elim (g t) fun j => f j t) μ

case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
i : ι
hi : some i ∈ insertNone s
⊢ AEMeasurable (fun t => (some i).elim (g t) fun j => f j t) μ

Proof state:
case refine_2
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ ∑ i ∈ insertNone s, i.elim q p = 1

Tactic:
simp_rw [sum_insertNone, Option.elim]

Result:
case refine_2
α : Type u_2
ι : Type u_3
inst✝ : MeasurableSpace α
μ : Measure α
s : Finset ι
g : α → ℝ≥0∞
f : ι → α → ℝ≥0∞
hg : AEMeasurable g μ
hf : ∀ i ∈ s, AEMeasurable (f i) μ
q : ℝ
p : ι → ℝ
hpq : q + ∑ i ∈ s, p i = 1
hq : 0 ≤ q
hp : ∀ i ∈ s, 0 ≤ p i
⊢ q + ∑ x ∈ s, p x = 1
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_eq_sub_of_hasDeriv_right_of_le (hab : a ≤ b) (hcont : ContinuousOn f (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x)
    (f'int : IntervalIntegrable f' volume a b) : ∫ y in a..b, f' y = f b - f a

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
refine (NormedSpace.eq_iff_forall_dual_eq ℝ).2 fun g => ?_

Result:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ g (∫ (y : ℝ) in a..b, f' y) = g (f b - f a)

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ g (∫ (y : ℝ) in a..b, f' y) = g (f b - f a)

Tactic:
rw [← g.intervalIntegral_comp_comm f'int, g.map_sub]

Result:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ ∫ (x : ℝ) in a..b, g (f' x) = g (f b) - g (f a)

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ ∫ (x : ℝ) in a..b, g (f' x) = g (f b) - g (f a)

Tactic:
exact integral_eq_sub_of_hasDeriv_right_of_le_real hab (g.continuous.comp_continuousOn hcont)
  (fun x hx => g.hasFDerivAt.comp_hasDerivWithinAt x (hderiv x hx))
  (g.integrable_comp ((intervalIntegrable_iff_integrableOn_Icc_of_le hab).1 f'int))

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
lemma sub_eq_fold_erase (s t : Multiset α) : s - t = foldl erase s t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ => by
    show ofList (l₁.diff l₂) = foldl erase l₁ l₂
    rw [diff_eq_foldl l₁ l₂]
    symm
    exact foldl_hom _ _ _ _ _ fun x y => rfl

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ foldl erase ↑l₁ ↑l₂ = ↑(List.foldl List.erase l₁ l₂)

Tactic:
exact foldl_hom _ _ _ _ _ fun x y => rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(l₁.diff l₂) = foldl erase ↑l₁ ↑l₂

Tactic:
rw [diff_eq_foldl l₁ l₂]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(List.foldl List.erase l₁ l₂) = foldl erase ↑l₁ ↑l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(List.foldl List.erase l₁ l₂) = foldl erase ↑l₁ ↑l₂

Tactic:
symm

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ foldl erase ↑l₁ ↑l₂ = ↑(List.foldl List.erase l₁ l₂)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ⟦l₁⟧ - ⟦l₂⟧ = foldl erase ⟦l₁⟧ ⟦l₂⟧

Tactic:
show ofList (l₁.diff l₂) = foldl erase l₁ l₂

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
l₁ l₂ : List α
⊢ ↑(l₁.diff l₂) = foldl erase ↑l₁ ↑l₂
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_eq_iff {f : α → M} {s : Set α} :
    mulSupport f = s ↔ (∀ x, x ∈ s → f x ≠ 1) ∧ ∀ x, x ∉ s → f x = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
s : Set α
⊢ mulSupport f = s ↔ (∀ x ∈ s, f x ≠ 1) ∧ ∀ x ∉ s, f x = 1

Tactic:
simp +contextual only [Set.ext_iff, mem_mulSupport, ne_eq, iff_def,
  not_imp_comm, and_comm, forall_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findSome?_toList (f : α → Option β) (v : Vector α n) :
    v.toList.findSome? f = v.findSome? f

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
v : Vector α n
⊢ List.findSome? f v.toList = findSome? f v

Tactic:
cases v

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    findSome? f { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Logic/Basic.lean
theorem ite_ne_right_iff : ite P a b ≠ b ↔ P ∧ a ≠ b :=
  dite_ne_right_iff.trans <| by rw [exists_prop]

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ P ∧ a ≠ b

Tactic:
rw [exists_prop]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_union_eq_left_of_ae_aux (ht_eq : ∀ᵐ x ∂μ.restrict t, f x = 0)
    (haux : StronglyMeasurable f) (H : IntegrableOn f (s ∪ t) μ) :
    ∫ x in s ∪ t, f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
case hst
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ μ (t \ k) = 0

Tactic:
rw [measure_zero_iff_ae_nmem]

Result:
case hst
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0
⊢ ∀ᵐ (a : X) ∂μ, a ∉ t \ k

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
let k := f ⁻¹' {0}

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : Array α} {l₂ : Array β} :
    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l₁' l₂' : Array γ
f : α → β → γ
l₁ : Array α
l₂ : Array β
⊢ zipWith f l₁ l₂ = l₁' ++ l₂' ↔
    ∃ w x y z, w.size = y.size ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
l₁' l₂' : Array γ
f : α → β → γ
l₂ : Array β
toList✝ : List α
⊢ zipWith f { toList := toList✝ } l₂ = l₁' ++ l₂' ↔
    ∃ w x y z,
      w.size = y.size ∧ { toList := toList✝ } = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
l₁' l₂' : Array γ
f : α → β → γ
l₂ : Array β
toList✝ : List α
⊢ zipWith f { toList := toList✝ } l₂ = l₁' ++ l₂' ↔
    ∃ w x y z,
      w.size = y.size ∧ { toList := toList✝ } = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
l₁' l₂' : Array γ
f : α → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ zipWith f { toList := toList✝¹ } { toList := toList✝ } = l₁' ++ l₂' ↔
    ∃ w x y z,
      w.size = y.size ∧
        { toList := toList✝¹ } = w ++ x ∧ { toList := toList✝ } = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z

Proof state:
case mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
l₂' : Array γ
f : α → β → γ
toList✝² : List α
toList✝¹ : List β
toList✝ : List γ
⊢ zipWith f { toList := toList✝² } { toList := toList✝¹ } = { toList := toList✝ } ++ l₂' ↔
    ∃ w x y z,
      w.size = y.size ∧
        { toList := toList✝² } = w ++ x ∧
          { toList := toList✝¹ } = y ++ z ∧ { toList := toList✝ } = zipWith f w y ∧ l₂' = zipWith f x z

Tactic:
cases l₂'

Result:
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝³ : List α
toList✝² : List β
toList✝¹ toList✝ : List γ
⊢ zipWith f { toList := toList✝³ } { toList := toList✝² } = { toList := toList✝¹ } ++ { toList := toList✝ } ↔
    ∃ w x y z,
      w.size = y.size ∧
        { toList := toList✝³ } = w ++ x ∧
          { toList := toList✝² } = y ++ z ∧
            { toList := toList✝¹ } = zipWith f w y ∧ { toList := toList✝ } = zipWith f x z

Proof state:
case mk.mk.mk.mk.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
w x : List α
y z : List β
h : w.length = y.length
⊢ ∃ w_1 x_1 y_1 z_1,
    w_1.size = y_1.size ∧
      w ++ x = w_1.toList ++ x_1.toList ∧
        y ++ z = y_1.toList ++ z_1.toList ∧
          { toList := List.zipWith f w y } = zipWith f w_1 y_1 ∧ { toList := List.zipWith f x z } = zipWith f x_1 z_1

Tactic:
exact ⟨w.toArray, x.toArray, y.toArray, z.toArray, by simp [h]⟩

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveRight_neg_symm' {x : PGame} (i) :
    x.moveRight i = -(-x).moveLeft (toLeftMovesNeg i)

Proof state:
x : PGame
i : x.RightMoves
⊢ x.moveRight i = -(-x).moveLeft (toLeftMovesNeg i)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atBot_zsmul_const {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x • r) l atBot

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x • r) l atBot

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢

Result:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x • r) l atTop

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto (fun x => -f x) l atTop
⊢ Tendsto (fun x => -f x • r) l atTop

Tactic:
exact hf.atTop_zsmul_const hr

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma nonempty_iInter_Iic_iff [Preorder α] {f : ι → α} :
    (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Proof state:
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
this : ⋂ i, Iic (f i) = lowerBounds (range f)
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Tactic:
simp [this, BddBelow]

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Tactic:
have : (⋂ (i : ι), Iic (f i)) = lowerBounds (range f) := by
  ext c; simp [lowerBounds]

Result:
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
this : ⋂ i, Iic (f i) = lowerBounds (range f)
⊢ (⋂ i, Iic (f i)).Nonempty ↔ BddBelow (range f)

Proof state:
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
⊢ ⋂ i, Iic (f i) = lowerBounds (range f)

Tactic:
ext c

Result:
case h
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
c : α
⊢ c ∈ ⋂ i, Iic (f i) ↔ c ∈ lowerBounds (range f)

Proof state:
case h
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
c : α
⊢ c ∈ ⋂ i, Iic (f i) ↔ c ∈ lowerBounds (range f)

Tactic:
simp [lowerBounds]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_true_of_true_le : ∀ {x : Bool}, true ≤ x → x = true

Proof state:
⊢ ∀ {x : Bool}, true ≤ x → x = true

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem Real.summable_pow_div_factorial (x : ℝ) : Summable (fun n ↦ x ^ n / n ! : ℕ → ℝ)

Proof state:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖

Tactic:
gcongr

Result:
no goals

Proof state:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
⊢ Summable fun n => x ^ n / ↑n !

Tactic:
have B : ‖x‖ / (⌊‖x‖⌋₊ + 1) < 1 := (div_lt_one A).2 (Nat.lt_floor_add_one _)

Result:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ Summable fun n => x ^ n / ↑n !

Proof state:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖

Tactic:
intro n hn

Result:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖

Proof state:
x : ℝ
⊢ Summable fun n => x ^ n / ↑n !

Tactic:
have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)

Result:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
⊢ Summable fun n => x ^ n / ↑n !

Proof state:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖

Tactic:
calc
  ‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
    rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
      norm_div, Real.norm_natCast, Nat.cast_succ]
  _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := by gcongr

Result:
no goals

Proof state:
x : ℝ
⊢ 1 ≤ ↑⌊‖x‖⌋₊ + 1

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / ↑(n + 1)!‖ = ‖x‖ / (↑n + 1) * ‖x ^ n / ↑n !‖

Tactic:
rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
  norm_div, Real.norm_natCast, Nat.cast_succ]

Result:
no goals

Proof state:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ Summable fun n => x ^ n / ↑n !

Tactic:
suffices ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / (n + 1)!‖ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖ from
  summable_of_ratio_norm_eventually_le B (eventually_atTop.2 ⟨⌊‖x‖⌋₊, this⟩)

Result:
x : ℝ
A : 0 < ↑⌊‖x‖⌋₊ + 1
B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1
⊢ ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
-- Mathlib/Data/Nat/Factors.lean
theorem four_dvd_or_exists_odd_prime_and_dvd_of_two_lt {n : ℕ} (n2 : 2 < n) :
    4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Proof state:
case inl.intro.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

Tactic:
contradiction

Result:
no goals

Proof state:
case inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
exact Or.inr ⟨p, hp, hdvd, hodd⟩

Result:
no goals

Proof state:
case inl.intro.zero
n2 : 2 < 2 ^ 0
⊢ 4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p

Tactic:
contradiction

Result:
no goals

Proof state:
case inl.intro.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

Tactic:
simp [Nat.pow_succ, mul_assoc]

Result:
no goals

Proof state:
n : ℕ
n2 : 2 < n
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
obtain ⟨_ | _ | k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd

Result:
case inl.intro.zero
n2 : 2 < 2 ^ 0
⊢ 4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p

case inl.intro.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

case inl.intro.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

case inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p