harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Segment.lean
lemma segment_inter_eq_endpoint_of_linearIndependent_sub
    {c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) :
    [c -[𝕜] x] ∩ [c -[𝕜] y] = {c}

Proof state:
case h₁
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
⊢ [c-[𝕜]x] ∩ [c-[𝕜]y] ⊆ {c}

Tactic:
intro z ⟨hzt, hzs⟩

Result:
case h₁
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : z ∈ [c-[𝕜]x]
hzs : z ∈ [c-[𝕜]y]
⊢ z ∈ {c}

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
⊢ x = x - c + c

Tactic:
abel

Result:
no goals

Proof state:
case h₁
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : z ∈ [c-[𝕜]x]
hzs : z ∈ [c-[𝕜]y]
⊢ z ∈ {c}

Tactic:
rw [segment_eq_image, mem_image] at hzt hzs

Result:
case h₁
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
z : E
hzt : ∃ x_1 ∈ Icc 0 1, (1 - x_1) • c + x_1 • x = z
hzs : ∃ x ∈ Icc 0 1, (1 - x) • c + x • y = z
⊢ z ∈ {c}

Proof state:
case h₁.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + q • y = (1 - p) • c + p • x
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ (1 - p) • c + p • x ∈ {c}

Tactic:
rw [Hx, Hy, smul_add, smul_add] at H

Result:
case h₁.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c x y : E
h : LinearIndependent 𝕜 ![x - c, y - c]
p : 𝕜
p0 : 0 ≤ p
p1 : p ≤ 1
q : 𝕜
H : (1 - q) • c + (q • (y - c) + q • c) = (1 - p) • c + (p • (x - c) + p • c)
q0 : 0 ≤ q
q1 : q ≤ 1
Hx : x = x - c + c
Hy : y = y - c + c
⊢ (1 - p) • c + p • x ∈ {c}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem set_eq_setTR : @set = @setTR

Proof state:
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ l.set n a = setTR.go l a l n #[]

Tactic:
exact (go #[] _ _ rfl).symm

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs → setTR.go l a (x :: xs) 0 acc = acc.toList ++ (x :: xs).set 0 a

Tactic:
simp [setTR.go, set]

Result:
no goals

Proof state:
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ setTR.go l a (x :: xs) (n + 1) acc = acc.toList ++ (x :: xs).set (n + 1) a

Tactic:
simp only [setTR.go, set]

Result:
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ setTR.go l a xs n (acc.push x) = acc.toList ++ x :: xs.set n a

Proof state:
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ l.set n a = l.setTR n a

Tactic:
simp [setTR]

Result:
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ l.set n a = setTR.go l a l n #[]

Proof state:
⊢ @set = @setTR

Tactic:
funext α l n a

Result:
case h.h.h.h
α : Type u_1
l : List α
n : Nat
a : α
⊢ l.set n a = l.setTR n a

Proof state:
α : Type u_1
l : List α
n✝ : Nat
a : α
acc : Array α
x : α
xs : List α
n : Nat
h : l = acc.toList ++ x :: xs
⊢ setTR.go l a xs n (acc.push x) = acc.toList ++ x :: xs.set n a

Tactic:
rw [go _ xs] <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
a : α
acc : Array α
x✝ : Nat
h : l = acc.toList ++ []
⊢ setTR.go l a [] x✝ acc = acc.toList ++ [].set x✝ a

Tactic:
simp [setTR.go, set, h]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
/-- If `s : Set R` is absorbing under multiplication, then its `TwoSidedIdeal.span` coincides with
its `AddSubgroup.closure`, as sets. -/
lemma mem_span_iff_mem_addSubgroup_closure_absorbing {s : Set R}
    (h_left : ∀ x y, y ∈ s → x * y ∈ s) (h_right : ∀ y x, y ∈ s → y * x ∈ s) {z : R} :
    z ∈ span s ↔ z ∈ closure s

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
⊢ z ∈ span s ↔ z ∈ closure s

Tactic:
have h_left' {x y} (hy : y ∈ closure s) : x * y ∈ closure s := by
  have := (AddMonoidHom.mulLeft x).map_closure s ▸ mem_map_of_mem _ hy
  refine closure_mono ?_ this
  rintro - ⟨y, hy, rfl⟩
  exact h_left x y hy

Result:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
⊢ z ∈ span s ↔ z ∈ closure s

Proof state:
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y : R
hy : y ∈ closure s
this : (AddMonoidHom.mulLeft x) y ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
⊢ ⇑(AddMonoidHom.mulLeft x) '' s ⊆ s

Tactic:
rintro - ⟨y, hy, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z x y✝ : R
hy✝ : y✝ ∈ closure s
this : (AddMonoidHom.mulLeft x) y✝ ∈ closure (⇑(AddMonoidHom.mulLeft x) '' s)
y : R
hy : y ∈ s
⊢ (AddMonoidHom.mulLeft x) y ∈ s
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_zero (hx : x ∈ s) :
    ContDiffWithinAt 𝕜 0 f s x ↔ ∃ u ∈ 𝓝[s] x, ContinuousOn f (s ∩ u)

Proof state:
case mpr.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hx : x ∈ s
u : Set E
H : u ∈ 𝓝[s] x
hu : ContinuousOn f (s ∩ u)
⊢ ContDiffWithinAt 𝕜 0 f (s ∩ u) x

Tactic:
have h' : x ∈ s ∩ u := ⟨hx, mem_of_mem_nhdsWithin hx H⟩

Result:
case mpr.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hx : x ∈ s
u : Set E
H : u ∈ 𝓝[s] x
hu : ContinuousOn f (s ∩ u)
h' : x ∈ s ∩ u
⊢ ContDiffWithinAt 𝕜 0 f (s ∩ u) x
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) : 0 < sin x :=
  calc 0 < x - x ^ 3 / 6 - |x| ^ 4 * (5 / 96) :=
      sub_pos.2 <| lt_sub_iff_add_lt.2
          (calc
            |x| ^ 4 * (5 / 96) + x ^ 3 / 6 ≤ x * (5 / 96) + x / 6

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ |x| ^ 1 = x

Tactic:
simp [abs_of_nonneg (le_of_lt hx0)]

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ x * (5 / 96) + x / 6 < x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 1 ≤ 4

Tactic:
decide

Result:
no goals

Proof state:
case h₁.h
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ |x| ^ 4 ≤ x

Tactic:
calc
  |x| ^ 4 ≤ |x| ^ 1 :=
    pow_le_pow_of_le_one (abs_nonneg _)
      (by rwa [abs_of_nonneg (le_of_lt hx0)]) (by decide)
  _ = x := by simp [abs_of_nonneg (le_of_lt hx0)]

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ |x| ≤ 1

Tactic:
rwa [abs_of_nonneg (le_of_lt hx0)]

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ |x| ^ 4 * (5 / 96) + x ^ 3 / 6 ≤ x * (5 / 96) + x / 6

Tactic:
gcongr

Result:
case h₁.h
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ |x| ^ 4 ≤ x

case h₂.hab
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ x ^ 3 ≤ x

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 1 ≤ 3

Tactic:
decide

Result:
no goals

Proof state:
case h₂.hab
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ x ^ 3 ≤ x

Tactic:
calc
  x ^ 3 ≤ x ^ 1 := pow_le_pow_of_le_one (le_of_lt hx0) hx (by decide)
  _ = x := pow_one _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
    (l.drop n).head h = l[n]'(by simp_all)

Proof state:
α : Type u_1
l : List α
n : Nat
h : drop n l ≠ []
w : n < l.length
⊢ (drop n l).head h = l[n]

Tactic:
simp [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some]

Result:
no goals

Proof state:
α : Type ?u.29606
l : List α
n : Nat
h : drop n l ≠ []
⊢ n < l.length

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
h : drop n l ≠ []
⊢ (drop n l).head h = l[n]

Tactic:
have w : n < l.length := length_lt_of_drop_ne_nil h

Result:
α : Type u_1
l : List α
n : Nat
h : drop n l ≠ []
w : n < l.length
⊢ (drop n l).head h = l[n]
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
theorem completedLFunction_one_sub {χ : DirichletCharacter ℂ N} (hχ : IsPrimitive χ) (s : ℂ) :
    completedLFunction χ (1 - s) = N ^ (s - 1 / 2) * rootNumber χ * completedLFunction χ⁻¹ s

Proof state:
case pos
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Even
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1) * χ (-1) / I ^ 0 * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
rw [pow_zero, div_one, h, mul_one, completedLFunction,
  completedLFunction_one_sub_even h.to_fun _ (.inr h_sum) (.inr <| χ.map_zero' hN)]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
rcases eq_or_ne N 1 with rfl | hN

Result:
case inl
s : ℂ
inst✝ : NeZero 1
χ : DirichletCharacter ℂ 1
hχ : χ.IsPrimitive
⊢ completedLFunction χ (1 - s) = ↑1 ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Proof state:
case e_a.e_Φ.h
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j : ZMod N, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
j : ZMod N
⊢ 𝓕 (⇑χ) j = χ⁻¹ (-1) * gaussSum χ stdAddChar * χ⁻¹ j

Tactic:
rw [hχ.fourierTransform_eq_inv_mul_gaussSum, ← neg_one_mul j, map_mul, mul_right_comm]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mod_eq_zero_of_dvd {a b : Ordinal} (H : b ∣ a) : a % b = 0

Proof state:
a b : Ordinal.{u_4}
H : b ∣ a
⊢ a % b = 0

Tactic:
rcases H with ⟨c, rfl⟩

Result:
case intro
b c : Ordinal.{u_4}
⊢ b * c % b = 0

Proof state:
case intro.inl
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case intro.inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0

Tactic:
simp [mod_def, hb]

Result:
no goals

Proof state:
case intro
b c : Ordinal.{u_4}
⊢ b * c % b = 0

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Result:
case intro.inl
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0

case intro.inr
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
    (le_refl : ∀ a : α, a ≤ a)
    (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
    xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
x : α
xs : List α
h₁ : a ∈ x :: xs
h₂ : ∀ (b : α), b ∈ x :: xs → a ≤ b
⊢ (x :: xs).min? = some a

Tactic:
exact congrArg some <| anti.1 _ _
  ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
  (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
h₁ : a ∈ []
h₂ : ∀ (b : α), b ∈ [] → a ≤ b
⊢ [].min? = some a

Tactic:
simp at h₁

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
xs : List α
⊢ (a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b) → xs.min? = some a

Tactic:
intro ⟨h₁, h₂⟩

Result:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
xs : List α
h₁ : a ∈ xs
h₂ : ∀ (b : α), b ∈ xs → a ≤ b
⊢ xs.min? = some a

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
xs : List α
h₁ : a ∈ xs
h₂ : ∀ (b : α), b ∈ xs → a ≤ b
⊢ xs.min? = some a

Tactic:
cases xs with
| nil => simp at h₁
| cons x xs =>
  exact congrArg some <| anti.1 _ _
    ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
    (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
xs : List α
⊢ xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b

Tactic:
refine ⟨fun h => ⟨min?_mem min_eq_or h, (le_min?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩

Result:
α : Type u_1
a : α
inst✝¹ : Min α
inst✝ : LE α
anti : Std.Antisymm fun x1 x2 => x1 ≤ x2
le_refl : ∀ (a : α), a ≤ a
min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b
le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c
xs : List α
⊢ (a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b) → xs.min? = some a
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_iInf {ι} (f : ι → Cardinal) : lift.{u, v} (iInf f) = ⨅ i, lift.{u, v} (f i)

Proof state:
case h.e'_3.h.e'_3
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i => lift.{u, v} (f i)) = lift.{u, v} '' range f

Tactic:
simp_rw [← comp_apply (f := lift), range_comp]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (sInf (range f)) = sInf (range fun i => lift.{u, v} (f i))

Tactic:
convert lift_sInf (range f)

Result:
case h.e'_3.h.e'_3
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i => lift.{u, v} (f i)) = lift.{u, v} '' range f

Proof state:
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (iInf f) = ⨅ i, lift.{u, v} (f i)

Tactic:
unfold iInf

Result:
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (sInf (range f)) = sInf (range fun i => lift.{u, v} (f i))
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem funext [Infinite R] {p q : R[X]} (ext : ∀ r : R, p.eval r = q.eval r) : p = q

Proof state:
case h
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
⊢ eval x (p - q) = 0

Tactic:
rw [eval_sub, sub_eq_zero, ext]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ p - q = 0

Tactic:
apply zero_of_eval_zero

Result:
case h
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ ∀ (x : R), eval x (p - q) = 0

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ p = q

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ p - q = 0

Proof state:
case h
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
⊢ ∀ (x : R), eval x (p - q) = 0

Tactic:
intro x

Result:
case h
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p q : R[X]
ext : ∀ (r : R), eval r p = eval r q
x : R
⊢ eval x (p - q) = 0
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_rotateL (l : Ordnode α) (x : α) (r : Ordnode α) :
    dual (rotateL l x r) = rotateR (dual r) x (dual l)

Proof state:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).dual =
    if l✝.size < ratio * r✝.size then r✝.dual.node3R x✝ l✝.dual x l.dual else r✝.dual.node4R x✝ l✝.dual x l.dual

Tactic:
split_ifs <;>
simp [dual_node3L, dual_node4L, node3R, add_comm]

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

Tactic:
cases r <;> simp [rotateL, rotateR, dual_node']

Result:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).dual =
    if l✝.size < ratio * r✝.size then r✝.dual.node3R x✝ l✝.dual x l.dual else r✝.dual.node4R x✝ l✝.dual x l.dual
-- Mathlib/Order/Disjoint.lean
lemma Codisjoint.ne_bot_of_ne_top' (h : Codisjoint a b) (hb : b ≠ ⊤) : a ≠ ⊥

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a b : α
h : Codisjoint a b
hb : b ≠ ⊤
⊢ a ≠ ⊥

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
b : α
hb : b ≠ ⊤
h : Codisjoint ⊥ b
⊢ False

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
b : α
hb : b ≠ ⊤
h : Codisjoint ⊥ b
⊢ False

Tactic:
exact hb <| by simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
b : α
hb : b ≠ ⊤
h : Codisjoint ⊥ b
⊢ b = ⊤

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/List/SplitOn.lean
theorem splitOn_intercalate [DecidableEq α] (x : α) (hx : ∀ l ∈ ls, x ∉ l) (hls : ls ≠ []) :
    ([x].intercalate ls).splitOn x = ls

Proof state:
case cons.cons.specialize_1
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
⊢ ∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l

Tactic:
intro l hl

Result:
case cons.cons.specialize_1
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l ∈ head✝ :: tail✝
⊢ ¬x ∈ l

Proof state:
case cons.cons.specialize_1
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l ∈ head✝ :: tail✝
⊢ ¬x ∈ l

Tactic:
apply hx l

Result:
case cons.cons.specialize_1
α : Type u_1
ls : List (List α)
inst✝ : DecidableEq α
x : α
hd head✝ : List α
tail✝ : List (List α)
ih :
  (∀ (l : List α), l ∈ head✝ :: tail✝ → ¬x ∈ l) →
    head✝ :: tail✝ ≠ [] → splitOn x (intersperse [x] (head✝ :: tail✝)).flatten = head✝ :: tail✝
hx : ∀ (l : List α), l ∈ hd :: head✝ :: tail✝ → ¬x ∈ l
hls : hd :: head✝ :: tail✝ ≠ []
l : List α
hl : l ∈ head✝ :: tail✝
⊢ l ∈ hd :: head✝ :: tail✝
-- Mathlib/LinearAlgebra/Prod.lean
theorem span_inl_union_inr {s : Set M} {t : Set M₂} :
    span R (inl R M M₂ '' s ∪ inr R M M₂ '' t) = (span R s).prod (span R t)

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
s : Set M
t : Set M₂
⊢ span R (⇑(inl R M M₂) '' s ∪ ⇑(inr R M M₂) '' t) = (span R s).prod (span R t)

Tactic:
rw [span_union, prod_eq_sup_map, ← span_image, ← span_image]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem exists_lt_of_limsup_le [AddMonoid α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α}
    (hu_bdd : IsBoundedUnder LE.le atTop u) (hu : Filter.limsup u atTop ≤ x) (hε : 0 < ε) :
    ∃ n : PNat, u n < x + ε

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∀ᶠ (n : ℕ) in atTop, u n < x + ε
⊢ ∃ n, u ↑n < x + ε

Tactic:
simp only [eventually_atTop] at h

Result:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∃ a, ∀ b ≥ a, u b < x + ε
⊢ ∃ n, u ↑n < x + ε

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∃ a, ∀ b ≥ a, u b < x + ε
⊢ ∃ n, u ↑n < x + ε

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
n : ℕ
hn : ∀ b ≥ n, u b < x + ε
⊢ ∃ n, u ↑n < x + ε

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
⊢ ∃ n, u ↑n < x + ε

Tactic:
have h : ∀ᶠ n : ℕ in atTop, u n < x + ε := eventually_lt_add_pos_of_limsup_le hu_bdd hu hε

Result:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
h : ∀ᶠ (n : ℕ) in atTop, u n < x + ε
⊢ ∃ n, u ↑n < x + ε

Proof state:
case intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder LE.le atTop u
hu : limsup u atTop ≤ x
hε : 0 < ε
n : ℕ
hn : ∀ b ≥ n, u b < x + ε
⊢ ∃ n, u ↑n < x + ε

Tactic:
exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

Result:
no goals