harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/MinMax.lean
theorem le_minimum_of_forall_le {b : WithTop α} (h : ∀ a ∈ l, b ≤ a) : b ≤ l.minimum

Proof state:
case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithTop α
h : ∀ (a : α), a ∈ [] → b ≤ ↑a
⊢ b ≤ [].minimum

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithTop α
h : ∀ (a : α), a ∈ l → b ≤ ↑a
⊢ b ≤ l.minimum

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp only [minimum_cons, le_min_iff]
  exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithTop α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → b ≤ ↑a) → b ≤ l.minimum
h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ ↑a_1
⊢ b ≤ (a :: l).minimum

Tactic:
simp only [minimum_cons, le_min_iff]

Result:
case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithTop α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → b ≤ ↑a) → b ≤ l.minimum
h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ ↑a_1
⊢ b ≤ ↑a ∧ b ≤ l.minimum

Proof state:
case cons
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithTop α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → b ≤ ↑a) → b ≤ l.minimum
h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ ↑a_1
⊢ b ≤ ↑a ∧ b ≤ l.minimum

Tactic:
exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l✝ : List α
b : WithTop α
a : α
l : List α
ih : (∀ (a : α), a ∈ l → b ≤ ↑a) → b ≤ l.minimum
h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ ↑a_1
⊢ a ∈ a :: l

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem sdiff_limsup [NeBot f] (a : α) : a \ limsup u f = liminf (fun b => a \ u b) f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ a \ limsup u f = liminf (fun b => a \ u b) f

Tactic:
rw [← compl_inj_iff]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (a \ limsup u f)ᶜ = (liminf (fun b => a \ u b) f)ᶜ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (a \ limsup u f)ᶜ = (liminf (fun b => a \ u b) f)ᶜ

Tactic:
simp only [sdiff_eq, liminf_compl, comp_def, compl_inf, compl_compl, sup_limsup]

Result:
no goals
-- Mathlib/Control/Basic.lean
theorem map_seq (f : β → γ) (x : F (α → β)) (y : F α) :
    f <$> (x <*> y) = (f ∘ ·) <$> x <*> y

Proof state:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ pure f <*> (x <*> y) = (pure fun x => f ∘ x) <*> x <*> y

Tactic:
simp [seq_assoc]

Result:
no goals

Proof state:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ f <$> (x <*> y) = (fun x => f ∘ x) <$> x <*> y

Tactic:
simp only [← pure_seq]

Result:
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ pure f <*> (x <*> y) = (pure fun x => f ∘ x) <*> x <*> y
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma coe_mul_eq_bind {a : α} (ha : a ≠ 0) : ∀ b, (a * b : WithBot α) = b.bind fun b ↦ ↑(a * b)
  | ⊥ => by simp only [ne_eq, coe_eq_zero, ha, not_false_eq_true, mul_bot]; rfl
  | (b : α) => rfl

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ↑a * ⊥ = Option.bind ⊥ fun b => Option.some (a * b)

Tactic:
simp only [ne_eq, coe_eq_zero, ha, not_false_eq_true, mul_bot]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊥ = Option.bind ⊥ fun b => Option.some (a * b)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : α
ha : a ≠ 0
⊢ ⊥ = Option.bind ⊥ fun b => Option.some (a * b)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem IsSuccPrelimit.add_natCast_lt [AddMonoidWithOne α] [SuccAddOrder α]
    (hx : IsSuccPrelimit x) (hy : y < x) : ∀ n : ℕ, y + n < x
  | 0 => by simpa
  | n + 1 => by
    rw [Nat.cast_add_one, ← add_assoc]
    exact hx.add_one_lt (hx.add_natCast_lt hy n)

Proof state:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + ↑(n + 1) < x

Tactic:
rw [Nat.cast_add_one, ← add_assoc]

Result:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + ↑n + 1 < x

Proof state:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + ↑0 < x

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + ↑n + 1 < x

Tactic:
exact hx.add_one_lt (hx.add_natCast_lt hy n)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.balance2 {l : RBNode α} {v : α} {r : RBNode α}
    (lv : l.All (cmpLT cmp · v)) (vr : r.All (cmpLT cmp v ·))
    (hl : l.Ordered cmp) (hr : r.Ordered cmp) : (balance2 l v r).Ordered cmp

Proof state:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (r.reverse.balance1 v l.reverse).reverse

Tactic:
exact .reverse <| hr.reverse.balance1
  ((All.reverse.2 vr).imp cmpLT.flip) ((All.reverse.2 lv).imp cmpLT.flip) hl.reverse

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (l.balance2 v r)

Tactic:
rw [← reverse_reverse (balance2 ..), reverse_balance2]

Result:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (r.reverse.balance1 v l.reverse).reverse
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem univ_eq_empty_iff : (univ : Finset α) = ∅ ↔ IsEmpty α

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ univ = ∅ ↔ IsEmpty α

Tactic:
rw [← not_nonempty_iff, ← univ_nonempty_iff, not_nonempty_iff_eq_empty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_append {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) :
    head (l₁ ++ l₂) w =
      if h : l₁.isEmpty then
        head l₂ (by simp_all [isEmpty_iff])
      else
        head l₁ (by simp_all [isEmpty_iff])

Proof state:
case isTrue
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h✝ : l₁.isEmpty = true
h : l₁ = []
⊢ (l₁ ++ l₂).head w = l₂.head ⋯

Tactic:
subst h

Result:
case isTrue
α : Type u_1
l₂ : List α
w : [] ++ l₂ ≠ []
h : [].isEmpty = true
⊢ ([] ++ l₂).head w = l₂.head ⋯

Proof state:
case isFalse
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : ¬l₁.isEmpty = true
⊢ (l₁ ++ l₂).head w = l₁.head ⋯

Tactic:
simp [isEmpty_iff] at h

Result:
case isFalse
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h✝ : ¬l₁.isEmpty = true
h : ¬l₁ = []
⊢ (l₁ ++ l₂).head w = l₁.head ⋯

Proof state:
α : Type ?u.200193
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : l₁.isEmpty = true
⊢ l₂ ≠ []

Tactic:
simp_all [isEmpty_iff]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : l₁.isEmpty = true
⊢ (l₁ ++ l₂).head w = l₂.head ⋯

Tactic:
simp [isEmpty_iff] at h

Result:
case isTrue
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h✝ : l₁.isEmpty = true
h : l₁ = []
⊢ (l₁ ++ l₂).head w = l₂.head ⋯

Proof state:
α : Type ?u.200193
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : ¬l₁.isEmpty = true
⊢ l₁ ≠ []

Tactic:
simp_all [isEmpty_iff]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h✝ : ¬l₁.isEmpty = true
h : ¬l₁ = []
⊢ (l₁ ++ l₂).head w = l₁.head ⋯

Tactic:
simp [h]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l₂ : List α
w : [] ++ l₂ ≠ []
h : [].isEmpty = true
⊢ ([] ++ l₂).head w = l₂.head ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
⊢ (l₁ ++ l₂).head w = if h : l₁.isEmpty = true then l₂.head ⋯ else l₁.head ⋯

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : l₁.isEmpty = true
⊢ (l₁ ++ l₂).head w = l₂.head ⋯

case isFalse
α : Type u_1
l₁ l₂ : List α
w : l₁ ++ l₂ ≠ []
h : ¬l₁.isEmpty = true
⊢ (l₁ ++ l₂).head w = l₁.head ⋯
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem Directed.inf_iSup_eq (h : Directed (· ≤ ·) f) :
    (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i

Proof state:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 => x1 ≤ x2) f
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
rw [iSup, h.directedOn_range.inf_sSup_eq, iSup_range]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem map_invUnitsSub (f : R →+* S) (u : Rˣ) :
    map f (invUnitsSub u) = invUnitsSub (Units.map (f : R →* S) u)

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ (coeff S n✝) ((map f) (invUnitsSub u)) = (coeff S n✝) (invUnitsSub ((Units.map ↑f) u))

Tactic:
simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ f ↑(u ^ (n✝ + 1))⁻¹ = ↑((Units.map ↑f) (u ^ (n✝ + 1)))⁻¹

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ f ↑(u ^ (n✝ + 1))⁻¹ = ↑((Units.map ↑f) (u ^ (n✝ + 1)))⁻¹

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
⊢ (map f) (invUnitsSub u) = invUnitsSub ((Units.map ↑f) u)

Tactic:
ext

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
u : Rˣ
n✝ : ℕ
⊢ (coeff S n✝) ((map f) (invUnitsSub u)) = (coeff S n✝) (invUnitsSub ((Units.map ↑f) u))
-- Mathlib/Tactic/Module.lean
theorem eq_const_cons [AddCommMonoid M] [Semiring R] [Module R M] {r : R} (m : M) {n : M}
    {l : NF R M} (h1 : 0 = r) (h2 : n = l.eval) :
    n = ((r, m) ::ᵣ l).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : 0 = r
h2 : n = l.eval
⊢ n = ((r, m) ::ᵣ l).eval

Tactic:
simp only [NF.eval, NF.cons] at *

Result:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : 0 = r
h2 : n = (map (fun x => x.1 • x.2) l).sum
⊢ n = (map (fun x => x.1 • x.2) ((r, m) :: l)).sum

Proof state:
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
r : R
m n : M
l : NF R M
h1 : 0 = r
h2 : n = (map (fun x => x.1 • x.2) l).sum
⊢ n = (map (fun x => x.1 • x.2) ((r, m) :: l)).sum

Tactic:
simp [← h1, h2]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma max_eq_left (h : b ≤ a) : max a b = a

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ a = max a b

Tactic:
apply eq_max (le_refl _) h

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ ∀ {d : α}, a ≤ d → b ≤ d → a ≤ d

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ max a b = a

Tactic:
apply Eq.symm

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ a = max a b

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ ∀ {d : α}, a ≤ d → b ≤ d → a ≤ d

Tactic:
intros

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
d✝ : α
a✝¹ : a ≤ d✝
a✝ : b ≤ d✝
⊢ a ≤ d✝

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
d✝ : α
a✝¹ : a ≤ d✝
a✝ : b ≤ d✝
⊢ a ≤ d✝

Tactic:
assumption

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem threeGPFree_smul_set₀ (ha : a ≠ 0) : ThreeGPFree (a • s) ↔ ThreeGPFree s :=
  ⟨fun hs b hb c hc d hd h ↦
    mul_left_cancel₀ ha
      (hs (Set.mem_image_of_mem _ hb) (Set.mem_image_of_mem _ hc) (Set.mem_image_of_mem _ hd) <| by
        rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]),
    fun hs => hs.smul_set₀ ha⟩

Proof state:
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NoZeroDivisors α
s : Set α
a : α
ha : a ≠ 0
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
⊢ a • b * a • d = a * c * (a * c)

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h, mul_mul_mul_comm]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isAtom_single {i : ι} [DecidableEq ι] [∀ i, PartialOrder (π i)] [∀ i, OrderBot (π i)]
    {a : π i} (h : IsAtom a) : IsAtom (Function.update (⊥ : ∀ i, π i) i a) :=
  isAtom_iff.2 ⟨i, by simpa, fun _ hji => Function.update_of_ne hji ..⟩

Proof state:
ι : Type u_4
π : ι → Type u
i : ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → PartialOrder (π i)
inst✝ : (i : ι) → OrderBot (π i)
a : π i
h : IsAtom a
⊢ IsAtom (Function.update ⊥ i a i)

Tactic:
simpa

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem oangle_eq_pi_sub_two_zsmul_oangle_center_right {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) : ∡ p₁ s.center p₂ = π - (2 : ℤ) • ∡ p₂ p₁ s.center

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ∡ p₁ s.center p₂ = ↑π - 2 • ∡ p₂ p₁ s.center

Tactic:
rw [oangle_eq_pi_sub_two_zsmul_oangle_center_left hp₁ hp₂ h,
  oangle_eq_oangle_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere' hp₂ hp₁)]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_of_iso (e : S₁ ≅ S₂) (h : S₁.Exact) : S₂.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.Exact
⊢ S₂.Exact

Tactic:
obtain ⟨⟨h, z⟩⟩ := h

Result:
case mk.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.HomologyData
z : IsZero h.left.H
⊢ S₂.Exact

Proof state:
case mk.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.HomologyData
z : IsZero h.left.H
⊢ S₂.Exact

Tactic:
exact ⟨⟨HomologyData.ofIso e h, z⟩⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lt_one_iff_zero {a : Ordinal} : a < 1 ↔ a = 0

Proof state:
a : Ordinal.{u_1}
⊢ a < 1 ↔ a = 0

Tactic:
simpa using @lt_succ_bot_iff _ _ _ a _ _

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma not_differentiableWithinAt_klFun_Iio_zero : ¬ DifferentiableWithinAt ℝ klFun (Iio 0) 0

Proof state:
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Iio 0)) atBot

Tactic:
rw [deriv_klFun]

Result:
⊢ Tendsto log (nhdsWithin 0 (Iio 0)) atBot

Proof state:
⊢ Tendsto log (nhdsWithin 0 (Iio 0)) atBot

Tactic:
exact tendsto_log_nhdsWithin_zero_left

Result:
no goals

Proof state:
⊢ ¬DifferentiableWithinAt ℝ klFun (Iio 0) 0

Tactic:
refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio _ ?_

Result:
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Iio 0)) atBot
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma even_finrank_of_not_isUnramified [IsGalois k K]
    (hw : ¬ IsUnramified k w) : Even (finrank k K)

Proof state:
case neg
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
h✝ : ¬FiniteDimensional k K
⊢ Even (finrank k K)

Tactic:
exact finrank_of_not_finite ‹_› ▸ Even.zero

Result:
no goals

Proof state:
case pos
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
h✝ : FiniteDimensional k K
⊢ Even (finrank k K)

Tactic:
exact IsGalois.card_aut_eq_finrank k K ▸ even_card_aut_of_not_isUnramified hw

Result:
no goals

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
⊢ Even (finrank k K)

Tactic:
by_cases FiniteDimensional k K

Result:
case pos
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
h✝ : FiniteDimensional k K
⊢ Even (finrank k K)

case neg
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
hw : ¬IsUnramified k w
h✝ : ¬FiniteDimensional k K
⊢ Even (finrank k K)
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma integrable_const_iff_isFiniteMeasure {c : β} (hc : c ≠ 0) :
    Integrable (fun _ ↦ c) μ ↔ IsFiniteMeasure μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
hc : c ≠ 0
⊢ Integrable (fun x => c) μ ↔ IsFiniteMeasure μ

Tactic:
simp [integrable_const_iff, hc, isFiniteMeasure_iff]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Ioo_mem_nhdsLT (H : a < b) : Ioo a b ∈ 𝓝[<] b

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a b : α
H : a < b
⊢ Ioo a b ∈ 𝓝[<] b

Tactic:
simpa only [← Iio_inter_Ioi] using inter_mem_nhdsWithin _ (Ioi_mem_nhds H)

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_single (a : G) (b : k) [DecidableEq G] :
    coeff (single a b) = Pi.single a b

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
a : G
b : k
inst✝ : DecidableEq G
⊢ (single a b).coeff = Pi.single a b

Tactic:
simp [coeff, Finsupp.single_eq_pi_single]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.tprod_vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 1) :
    ∃ s : Finset α, ∀ t : Set α, Disjoint t s → (∏' b : t, f b) ∈ e

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this✝ : UniformSpace G := IsTopologicalGroup.toUniformSpace G
this : UniformGroup G
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he

Result:
no goals

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
classical
letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
have : UniformGroup G := uniformGroup_of_commGroup
exact cauchySeq_finset_iff_tprod_vanishing.1 hf.hasProd.cauchySeq e he

Result:
no goals

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this : UniformSpace G := IsTopologicalGroup.toUniformSpace G
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
have : UniformGroup G := uniformGroup_of_commGroup

Result:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this✝ : UniformSpace G := IsTopologicalGroup.toUniformSpace G
this : UniformGroup G
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G

Result:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this : UniformSpace G := IsTopologicalGroup.toUniformSpace G
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
-- Mathlib/CategoryTheory/Sites/Canonical.lean
theorem le_finestTopology (Ps : Set (Cᵒᵖ ⥤ Type v)) (J : GrothendieckTopology C)
    (hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P) : J ≤ finestTopology Ps

Proof state:
case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows

Tactic:
exact hJ P hP (S.pullback f) (J.pullback_stable f hS)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
⊢ J ≤ finestTopology Ps

Tactic:
rintro X S hS _ ⟨⟨_, _, ⟨P, hP, rfl⟩, rfl⟩, rfl⟩

Result:
case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
⊢ S ∈ (fun f => ↑f X) ⟨(finestTopologySingle P).sieves, ⋯⟩

Proof state:
case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
⊢ S ∈ (fun f => ↑f X) ⟨(finestTopologySingle P).sieves, ⋯⟩

Tactic:
intro Y f

Result:
case intro.mk.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type v)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
P : Cᵒᵖ ⥤ Type v
hP : P ∈ Ps
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f S).arrows
-- Mathlib/Algebra/Order/Module/Algebra.lean
@[simp] lemma algebraMap_lt_algebraMap : algebraMap α β a₁ < algebraMap α β a₂ ↔ a₁ < a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : OrderedCommSemiring α
inst✝³ : StrictOrderedSemiring β
inst✝² : Algebra α β
inst✝¹ : SMulPosStrictMono α β
a₁ a₂ : α
inst✝ : SMulPosReflectLT α β
⊢ (algebraMap α β) a₁ < (algebraMap α β) a₂ ↔ a₁ < a₂

Tactic:
simp [Algebra.algebraMap_eq_smul_one]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem catalan_two : catalan 2 = 2

Proof state:
⊢ catalan 2 = 2

Tactic:
norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_insert_left (h : a < b) : insert a (Ioo a b) = Ico a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
rw [insert_eq, union_comm, Ioo_union_left h]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem inverse_mul_eq_iff_eq_mul (x y z : M₀) (h : IsUnit x) : inverse x * y = z ↔ y = x * z :=
  ⟨fun h1 => by rw [← h1, mul_inverse_cancel_left _ _ h],
  fun h1 => by rw [h1, inverse_mul_cancel_left _ _ h]⟩

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : inverse x * y = z
⊢ y = x * z

Tactic:
rw [← h1, mul_inverse_cancel_left _ _ h]

Result:
no goals

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y z : M₀
h : IsUnit x
h1 : y = x * z
⊢ inverse x * y = z

Tactic:
rw [h1, inverse_mul_cancel_left _ _ h]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Basic.lean
theorem toPrimeSpectrum_injective : (@toPrimeSpectrum R _).Injective := fun ⟨_, _⟩ ⟨_, _⟩ h => by
  simpa only [MaximalSpectrum.mk.injEq] using PrimeSpectrum.ext_iff.mp h

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x✝¹ x✝ : MaximalSpectrum R
asIdeal✝¹ : Ideal R
isMaximal✝¹ : asIdeal✝¹.IsMaximal
asIdeal✝ : Ideal R
isMaximal✝ : asIdeal✝.IsMaximal
h :
  { asIdeal := asIdeal✝¹, isMaximal := isMaximal✝¹ }.toPrimeSpectrum =
    { asIdeal := asIdeal✝, isMaximal := isMaximal✝ }.toPrimeSpectrum
⊢ { asIdeal := asIdeal✝¹, isMaximal := isMaximal✝¹ } = { asIdeal := asIdeal✝, isMaximal := isMaximal✝ }

Tactic:
simpa only [MaximalSpectrum.mk.injEq] using PrimeSpectrum.ext_iff.mp h

Result:
no goals