harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/TypeVec.lean
theorem dropFun_diag {α} : dropFun (@prod.diag (n + 1) α) = prod.diag

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 n
x✝ : α.drop i
⊢ dropFun prod.diag i x✝ = prod.diag i x✝

Tactic:
induction i <;> simp [dropFun, *] <;> rfl

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ dropFun prod.diag = prod.diag

Tactic:
ext i : 2

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 n
x✝ : α.drop i
⊢ dropFun prod.diag i x✝ = prod.diag i x✝
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
lemma Fin.addRothNumber_le_rothNumberNat (k n : ℕ) (hkn : k ≤ n) :
    addRothNumber (Iio k : Finset (Fin n.succ)) ≤ rothNumberNat k

Proof state:
case refine_1
k n : ℕ
hkn : k ≤ n
⊢ Set.MapsTo Nat.cast ↑(range k) ↑(Iio ↑k)

Tactic:
simpa using fun x ↦ natCast_strictMono hkn

Result:
no goals

Proof state:
case refine_2
k n : ℕ
hkn : k ≤ n
⊢ Set.SurjOn Nat.cast ↑(range k) ↑(Iio ↑k)

Tactic:
simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_iff_val_lt_val,
  val_cast_of_lt, Nat.lt_succ_iff.2 hkn, coe_range]

Result:
case refine_2
k n : ℕ
hkn : k ≤ n
⊢ ∀ (x : Fin n.succ), ↑x < k → ∃ x_1 < k, ↑x_1 = x

Proof state:
k n : ℕ
hkn : k ≤ n
⊢ addRothNumber (Iio ↑k) ≤ rothNumberNat k

Tactic:
suffices h : Set.BijOn (Nat.cast : ℕ → Fin n.succ) (range k) (Iio k : Finset (Fin n.succ)) by
  exact (AddMonoidHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h

Result:
k n : ℕ
hkn : k ≤ n
⊢ Set.BijOn Nat.cast ↑(range k) ↑(Iio ↑k)

Proof state:
k n : ℕ
hkn : k ≤ n
h : Set.BijOn Nat.cast ↑(range k) ↑(Iio ↑k)
⊢ addRothNumber (Iio ↑k) ≤ rothNumberNat k

Tactic:
exact (AddMonoidHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h

Result:
no goals

Proof state:
case refine_2
k n : ℕ
hkn : k ≤ n
⊢ ∀ (x : Fin n.succ), ↑x < k → ∃ x_1 < k, ↑x_1 = x

Tactic:
exact fun x hx ↦ ⟨x, hx, by simp⟩

Result:
no goals

Proof state:
k n : ℕ
hkn : k ≤ n
x : Fin n.succ
hx : ↑x < k
⊢ ↑↑x = x

Tactic:
simp

Result:
no goals

Proof state:
k n : ℕ
hkn : k ≤ n
⊢ ↑(range k) ⊆ Set.Iio n.succ

Tactic:
simp

Result:
k n : ℕ
hkn : k ≤ n
⊢ k ≤ n + 1

Proof state:
k n : ℕ
hkn : k ≤ n
⊢ k ≤ n + 1

Tactic:
omega

Result:
no goals

Proof state:
k n : ℕ
hkn : k ≤ n
⊢ Set.BijOn Nat.cast ↑(range k) ↑(Iio ↑k)

Tactic:
refine ⟨?_, (CharP.natCast_injOn_Iio _ n.succ).mono (by simp; omega), ?_⟩

Result:
case refine_1
k n : ℕ
hkn : k ≤ n
⊢ Set.MapsTo Nat.cast ↑(range k) ↑(Iio ↑k)

case refine_2
k n : ℕ
hkn : k ≤ n
⊢ Set.SurjOn Nat.cast ↑(range k) ↑(Iio ↑k)
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_congr {β : Type v} (e : α ≃ β) : toNat #α = toNat #β

Proof state:
α : Type u
β : Type v
e : α ≃ β
⊢ toNat #α = toNat #β

Tactic:
rw [← toNat_lift, (lift_mk_eq.{_,_,v}).mpr ⟨e⟩, toNat_lift]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
@[to_additive tsum_setProd_singleton_right]
lemma tprod_setProd_singleton_right (s : Set β) (c : γ) (f : β × γ → α) :
    (∏' x : s ×ˢ {c}, f x) = ∏' b : s, f (b, c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
c : γ
f : β × γ → α
⊢ ∏' (x : ↑(s ×ˢ {c})), f ↑x = ∏' (b : ↑s), f (↑b, c)

Tactic:
rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ (Prod.mk.inj_right c).injOn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {i : Nat} (hi : i < l₁.length) :
    l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.length hi)

Proof state:
α : Type ?u.184179
l₂ l₁ : List α
i : Nat
hi : i < l₁.length
⊢ i < (l₁ ++ l₂).length

Tactic:
simpa using Nat.lt_add_right l₂.length hi

Result:
no goals

Proof state:
α : Type u_1
l₂ l₁ : List α
i : Nat
hi : i < l₁.length
⊢ l₁[i] = (l₁ ++ l₂)[i]

Tactic:
rw [getElem_append_left] <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
lemma minSmoothness_add {n m : WithTop ℕ∞} : minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : WithTop ℕ∞
⊢ minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m

Tactic:
simp only [minSmoothness]

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : WithTop ℕ∞
⊢ (if IsRCLikeNormedField 𝕜 then n + m else ω) = (if IsRCLikeNormedField 𝕜 then n else ω) + m

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n m : WithTop ℕ∞
⊢ (if IsRCLikeNormedField 𝕜 then n + m else ω) = (if IsRCLikeNormedField 𝕜 then n else ω) + m

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_abs_int_rpow {b : ℝ} (hb : 1 < b) :
    Summable fun n : ℤ => |(n : ℝ)| ^ (-b)

Proof state:
case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑(-↑n)| ^ (-b)

Tactic:
on_goal 2 => simp_rw [Int.cast_neg, abs_neg]

Result:
case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

Proof state:
case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

Tactic:
all_goals
  simp_rw [Int.cast_natCast, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]
  rwa [summable_nat_rpow, neg_lt_neg_iff]

Result:
no goals

Proof state:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => ↑n ^ (-b)

Tactic:
rwa [summable_nat_rpow, neg_lt_neg_iff]

Result:
no goals

Proof state:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑(-↑n)| ^ (-b)

Tactic:
simp_rw [Int.cast_neg, abs_neg]

Result:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

Proof state:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

Tactic:
simp_rw [Int.cast_natCast, fun n : ℕ => abs_of_nonneg (n.cast_nonneg : 0 ≤ (n : ℝ))]

Result:
case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => ↑n ^ (-b)

Proof state:
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑n| ^ (-b)

Tactic:
apply Summable.of_nat_of_neg

Result:
case hf₁
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑↑n| ^ (-b)

case hf₂
b : ℝ
hb : 1 < b
⊢ Summable fun n => |↑(-↑n)| ^ (-b)
-- Mathlib/Topology/JacobsonSpace.lean
lemma isClosed_singleton_of_isLocallyClosed_singleton [JacobsonSpace X] {x : X}
    (hx : IsLocallyClosed {x}) : IsClosed {x}

Proof state:
case intro.intro.refl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
x : X
hx : IsLocallyClosed {x}
hy' : x ∈ closedPoints X
⊢ IsClosed {x}

Tactic:
exact hy'

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
x : X
hx : IsLocallyClosed {x}
⊢ IsClosed {x}

Tactic:
obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ :=
  nonempty_inter_closedPoints (Set.singleton_nonempty x) hx

Result:
case intro.intro.refl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
x : X
hx : IsLocallyClosed {x}
hy' : x ∈ closedPoints X
⊢ IsClosed {x}
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem mod_four_ne_three_of_sq_eq_neg_sq' {x y : ZMod p} (hy : y ≠ 0) (hxy : x ^ 2 = -y ^ 2) :
    p % 4 ≠ 3 :=
  @mod_four_ne_three_of_sq_eq_neg_one p _ (x / y)
    (by
      apply_fun fun z => z / y ^ 2 at hxy
      rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 / y ^ 2 = -y ^ 2 / y ^ 2
⊢ (x / y) ^ 2 = -1

Tactic:
rwa [neg_div, ← div_pow, ← div_pow, div_self hy, one_pow] at hxy

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 = -y ^ 2
⊢ (x / y) ^ 2 = -1

Tactic:
apply_fun fun z => z / y ^ 2 at hxy

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ZMod p
hy : y ≠ 0
hxy : x ^ 2 / y ^ 2 = -y ^ 2 / y ^ 2
⊢ (x / y) ^ 2 = -1
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_sub : ghostFun (x - y) = ghostFun x - ghostFun y

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ WittVector.ghostFun (x - y) = WittVector.ghostFun x - WittVector.ghostFun y

Tactic:
ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.nsmul_sub_eq [AddCommGroup α] [AddGroup β] (h : Antiperiodic f c) (n : ℕ) :
    f (n • c - x) = (-1) ^ n • f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℕ
⊢ f (n • c - x) = (-1) ^ n • f (-x)

Tactic:
simpa only [Int.reduceNeg, natCast_zsmul] using h.zsmul_sub_eq n

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/NormedValued.lean
theorem norm_eq_zero {x : L} (hx : norm x = 0) : x = 0

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x : L
hx : norm x = 0
⊢ x = 0

Tactic:
simpa [norm, NNReal.coe_eq_zero, RankOne.hom_eq_zero_iff, zero_iff] using hx

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.iInter [Countable ι] {f : ι → Set α} (h : ∀ b, MeasurableSet (f b)) :
    MeasurableSet (⋂ b, f b) :=
  .of_compl <| by rw [compl_iInter]; exact .iUnion fun b => (h b).compl

Proof state:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋂ b, f b)ᶜ

Tactic:
rw [compl_iInter]

Result:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ i, (f i)ᶜ)

Proof state:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ i, (f i)ᶜ)

Tactic:
exact .iUnion fun b => (h b).compl

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_affine_Ioo {a : α} (h : 0 < a) (b c d : α) :
    (a * · + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
this : (fun x => x + b) '' ((fun x => a * x) '' Ioo c d) = Ioo (a * c + b) (a * d + b)
⊢ (fun x => a * x + b) '' Ioo c d = Ioo (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
⊢ (fun x => x + b) '' ((fun x => a * x) '' Ioo c d) = Ioo (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Ioo h, image_add_const_Ioo]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_self {a : Int} : a % a = 0

Proof state:
a : Int
this : 1 * a % a = 0
⊢ a % a = 0

Tactic:
rwa [Int.one_mul] at this

Result:
no goals

Proof state:
a : Int
⊢ a % a = 0

Tactic:
have := mul_emod_left 1 a

Result:
a : Int
this : 1 * a % a = 0
⊢ a % a = 0
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem inv_invApp (U : Opens X) :
    inv (H.invApp _ U) =
      f.c.app (op (opensFunctor f |>.obj U)) ≫
        X.presheaf.map
          (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op U)) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U)))) ≫
      f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
simp [← Functor.map_comp]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op U)) = invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
delta invApp

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op U)) =
    (X.presheaf.map (eqToHom ⋯) ≫ inv (f.c.app (op ((opensFunctor f).obj U)))) ≫
      f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ inv (invApp f U) = f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
rw [← cancel_epi (H.invApp _ U), IsIso.hom_inv_id]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ 𝟙 (X.presheaf.obj (op U)) = invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
simp [Opens.map, Set.preimage_image_eq _ H.base_open.injective]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_X [CommRing S] [IsDomain S] [Algebra T S] :
    aroots (X : T[X]) S = {0}

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ X.aroots S = {0}

Tactic:
rw [aroots_def, map_X, roots_X]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem smul_map_diagonal_volume_pi [DecidableEq ι] {D : ι → ℝ} (h : det (diagonal D) ≠ 0) :
    ENNReal.ofReal (abs (det (diagonal D))) • Measure.map (toLin' (diagonal D)) volume =
      volume

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i => s i) = univ.pi fun i => (fun x => D i * x) ⁻¹' s i
i : ι
A : D i ≠ 0
⊢ ofReal |D i| * volume ((fun x => D i * x) ⁻¹' s i) = volume (s i)

Tactic:
rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul,
  mul_inv_cancel₀ A, abs_one, ENNReal.ofReal_one, one_mul]

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (ofReal |(Matrix.diagonal D).det| • Measure.map (⇑(toLin' (Matrix.diagonal D))) volume) (univ.pi s) =
    ∏ i : ι, volume (s i)

Tactic:
simp only [det_diagonal, Measure.coe_smul, Algebra.id.smul_eq_mul, Pi.smul_apply]

Result:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ofReal |∏ i : ι, D i| * (Measure.map (⇑(toLin' (Matrix.diagonal D))) volume) (univ.pi s) = ∏ x : ι, volume (s x)
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem generateFrom_Ico_mem_le_borel {α : Type*} [TopologicalSpace α] [LinearOrder α]
    [OrderClosedTopology α] (s t : Set α) :
    MeasurableSpace.generateFrom { S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S }
      ≤ borel α

Proof state:
case h
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ ∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S}, MeasurableSet t_1

Tactic:
borelize α

Result:
case h
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ ∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S}, MeasurableSet t_1

Proof state:
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S} ≤ borel α

Tactic:
apply generateFrom_le

Result:
case h
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
⊢ ∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S}, MeasurableSet t_1

Proof state:
case h.intro.intro.intro.intro.intro
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
a b : α
⊢ MeasurableSet (Ico a b)

Tactic:
exact measurableSet_Ico

Result:
no goals

Proof state:
case h
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ ∀ t_1 ∈ {S | ∃ l ∈ s, ∃ u ∈ t, l < u ∧ Ico l u = S}, MeasurableSet t_1

Tactic:
rintro _ ⟨a, -, b, -, -, rfl⟩

Result:
case h.intro.intro.intro.intro.intro
α : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
s t : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
a b : α
⊢ MeasurableSet (Ico a b)
-- Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
theorem sq_sum_div_le_sum_sq_div [LinearOrderedSemifield R] [ExistsAddOfLE R] (s : Finset ι)
    (f : ι → R) {g : ι → R} (hg : ∀ i ∈ s, 0 < g i) :
    (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Tactic:
have H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i := fun i hi ↦ div_nonneg (sq_nonneg _) (hg' i hi)

Result:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Tactic:
refine div_le_of_le_mul₀ (sum_nonneg hg') (sum_nonneg H)
  (sum_sq_le_sum_mul_sum_of_sq_eq_mul _ H hg' fun i hi ↦ ?_)

Result:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ f i ^ 2 = f i ^ 2 / g i * g i

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ f i ^ 2 = f i ^ 2 / g i * g i

Tactic:
rw [div_mul_cancel₀]

Result:
case h
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ g i ≠ 0

Proof state:
case h
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i
i : ι
hi : i ∈ s
⊢ g i ≠ 0

Tactic:
exact (hg i hi).ne'

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i

Tactic:
have hg' : ∀ i ∈ s, 0 ≤ g i := fun i hi ↦ (hg i hi).le

Result:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemifield R
inst✝ : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
⊢ (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i
-- Mathlib/Data/Part.lean
theorem ofOption_eq_get {α} (o : Option α) : ofOption o = ⟨_, @Option.get _ o⟩ :=
  Part.ext' (ofOption_dom o) fun h₁ h₂ => by
    cases o
    · simp at h₂
    · rfl

Proof state:
α : Type u_4
o : Option α
h₁ : (↑o).Dom
h₂ : { Dom := o.isSome = true, get := o.get }.Dom
⊢ (↑o).get h₁ = { Dom := o.isSome = true, get := o.get }.get h₂

Tactic:
cases o

Result:
case none
α : Type u_4
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.none.isSome = true, get := Option.none.get }.Dom
⊢ (↑Option.none).get h₁ = { Dom := Option.none.isSome = true, get := Option.none.get }.get h₂

case some
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.Dom
⊢ (↑(Option.some val✝)).get h₁ = { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.get h₂

Proof state:
case some
α : Type u_4
val✝ : α
h₁ : (↑(Option.some val✝)).Dom
h₂ : { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.Dom
⊢ (↑(Option.some val✝)).get h₁ = { Dom := (Option.some val✝).isSome = true, get := (Option.some val✝).get }.get h₂

Tactic:
rfl

Result:
no goals

Proof state:
case none
α : Type u_4
h₁ : (↑Option.none).Dom
h₂ : { Dom := Option.none.isSome = true, get := Option.none.get }.Dom
⊢ (↑Option.none).get h₁ = { Dom := Option.none.isSome = true, get := Option.none.get }.get h₂

Tactic:
simp at h₂

Result:
no goals
-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem tsum_of_nnnorm_bounded {f : ι → E} {g : ι → ℝ≥0} {a : ℝ≥0} (hg : HasSum g a)
    (h : ∀ i, ‖f i‖₊ ≤ g i) : ‖∑' i : ι, f i‖₊ ≤ a

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum (fun a => ↑(g a)) ↑a
h : ∀ (i : ι), ‖f i‖ ≤ ↑(g i)
⊢ ‖∑' (i : ι), f i‖ ≤ ↑a

Tactic:
exact tsum_of_norm_bounded hg h

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
⊢ ‖∑' (i : ι), f i‖₊ ≤ a

Tactic:
simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *

Result:
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum (fun a => ↑(g a)) ↑a
h : ∀ (i : ι), ‖f i‖ ≤ ↑(g i)
⊢ ‖∑' (i : ι), f i‖ ≤ ↑a
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- A map out of a delta-generated space is continuous iff it is continuous with respect
  to the delta-generated topology on the codomain. -/
lemma continuous_to_deltaGenerated [DeltaGeneratedSpace X] {f : X → Y} :
    Continuous[_, deltaGenerated Y] f ↔ Continuous f

Proof state:
X : Type u_1
Y : Type u_2
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
f : X → Y
⊢ Continuous f ↔ Continuous f

Tactic:
simp_rw [DeltaGeneratedSpace.continuous_iff, continuous_euclidean_to_deltaGenerated]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem ofPermHomFun_apply_of_mem_fixedPoints {x : α} (hx : x ∈ Function.fixedPoints g) :
    ofPermHomFun a τ x = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ x = x

Tactic:
rw [ofPermHomFun, dif_neg]

Result:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ g.cycleOf x ∉ g.cycleFactorsFinset

Proof state:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ g.cycleOf x ∉ g.cycleFactorsFinset

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, not_mem_support]

Result:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ g x = x

Proof state:
case hnc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ g x = x

Tactic:
exact hx

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_neg (f : α → F) (q : ℝ) (μ : Measure α) : eLpNorm' (-f) q μ = eLpNorm' f q μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
q : ℝ
μ : Measure α
⊢ eLpNorm' (-f) q μ = eLpNorm' f q μ

Tactic:
simp [eLpNorm'_eq_lintegral_enorm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem apply_norm_eq_sqrt_inner_adjoint_left (A : E →L[𝕜] F) (x : E) :
    ‖A x‖ = √(re ⟪(A† ∘L A) x, x⟫)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ‖A x‖ = √(re ⟪((adjoint A).comp A) x, x⟫_𝕜)

Tactic:
rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]

Result:
no goals