harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem reverse_infix : reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂

Proof state:
case refine_1
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁.reverse <:+: l₂.reverse
s t : List α✝
e : s ++ l₁.reverse ++ t = l₂.reverse
⊢ t.reverse ++ l₁ ++ s.reverse = l₂

Tactic:
rw [← reverse_reverse l₁, append_assoc, ← reverse_append, ← reverse_append, e,
  reverse_reverse]

Result:
no goals

Proof state:
case refine_2
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁ <:+: l₂
s t : List α✝
e : s ++ l₁ ++ t = l₂
⊢ t.reverse ++ l₁.reverse ++ s.reverse = l₂.reverse

Tactic:
rw [append_assoc, ← reverse_append, ← reverse_append, e]

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁.reverse <:+: l₂.reverse ↔ l₁ <:+: l₂

Tactic:
refine ⟨fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩, fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩⟩

Result:
case refine_1
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁.reverse <:+: l₂.reverse
s t : List α✝
e : s ++ l₁.reverse ++ t = l₂.reverse
⊢ t.reverse ++ l₁ ++ s.reverse = l₂

case refine_2
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁ <:+: l₂
s t : List α✝
e : s ++ l₁ ++ t = l₂
⊢ t.reverse ++ l₁.reverse ++ s.reverse = l₂.reverse
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem mul_lt_sin {x : ℝ} (hx : 0 < x) (hx' : x < π / 2) : 2 / π * x < sin x

Proof state:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < sin x

Tactic:
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using @lt_sin_mul ((π / 2)⁻¹ * x)
  (mul_pos (inv_pos.2 pi_div_two_pos) hx) (by rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos])

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ 2 / π * x < sin x

Tactic:
rw [← inv_div]

Result:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < sin x

Proof state:
x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < 1

Tactic:
rwa [← div_eq_inv_mul, div_lt_one pi_div_two_pos]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
protected lemma IsOfFinOrder.eq_neg_one (ha₀ : a ≤ 0) (ha : IsOfFinOrder a) : a = -1 :=
  (sq_eq_one_iff.1 <| ha.pow.eq_one <| sq_nonneg a).resolve_left <| by
    rintro rfl; exact one_pos.not_le ha₀

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
ha₀ : 1 ≤ 0
ha : IsOfFinOrder 1
⊢ False

Tactic:
exact one_pos.not_le ha₀

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LinearOrderedRing G
a : G
ha₀ : a ≤ 0
ha : IsOfFinOrder a
⊢ ¬a = 1

Tactic:
rintro rfl

Result:
G : Type u_1
inst✝ : LinearOrderedRing G
ha₀ : 1 ≤ 0
ha : IsOfFinOrder 1
⊢ False
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
lemma edgeFinset_eq_empty : G.edgeFinset = ∅ ↔ G = ⊥

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset = ∅ ↔ G = ⊥

Tactic:
rw [← edgeFinset_bot, edgeFinset_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem eq_natAbs_of_zero_le {a : Int} (h : 0 ≤ a) : a = natAbs a

Proof state:
a : Int
h : 0 ≤ a
⊢ a = ↑a.natAbs

Tactic:
let ⟨n, e⟩ := eq_ofNat_of_zero_le h

Result:
a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ a = ↑a.natAbs

Proof state:
a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ ↑n = ↑(↑n).natAbs

Tactic:
rfl

Result:
no goals

Proof state:
a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ a = ↑a.natAbs

Tactic:
rw [e]

Result:
a : Int
h : 0 ≤ a
n : Nat
e : a = ↑n
⊢ ↑n = ↑(↑n).natAbs
-- Mathlib/Algebra/CharP/Two.lean
theorem eq_add_iff_add_eq {a b c : R} : a = b + c ↔ a + c = b

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
a b c : R
⊢ a = b + c ↔ a + c = b

Tactic:
rw [← eq_sub_iff_add_eq, sub_eq_add]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_map_symm (e : α ≃ᵐ β) : (ν.map e.symm).map e = ν

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
ν : Measure β
e : α ≃ᵐ β
⊢ map (⇑e) (map (⇑e.symm) ν) = ν

Tactic:
simp [map_map e.measurable e.symm.measurable]

Result:
no goals
-- Mathlib/Order/Category/LinOrd.lean
lemma id_apply (X : LinOrd) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : LinOrd
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_mul_const (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) :
    s.indicator (f · * a) i = s.indicator f i * a

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f : ι → M₀
a : M₀
i : ι
⊢ s.indicator (fun x => f x * a) i = s.indicator f i * a

Tactic:
rw [indicator_mul_left]

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
theorem wEquiv.refl {α : TypeVec n} (x : q.P.W α) : WEquiv x x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : (P F).W α
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
    WEquiv ((P F).wMk a f' f) ((P F).wMk a f' f)

Tactic:
intro a f' f

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ WEquiv ((P F).wMk a f' f) ((P F).wMk a f' f)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : (P F).W α
⊢ WEquiv x x

Tactic:
apply q.P.w_cases _ x

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : (P F).W α
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f : (P F).last.B a → (P F).W α),
    WEquiv ((P F).wMk a f' f) ((P F).wMk a f' f)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ WEquiv ((P F).wMk a f' f) ((P F).wMk a f' f)

Tactic:
exact WEquiv.abs a f' f a f' f rfl

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem coe_pair {a b : α} : (({a, b} : Finset α) : Set α) = {a, b}

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a b x✝ : α
⊢ x✝ ∈ ↑{a, b} ↔ x✝ ∈ {a, b}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
⊢ ↑{a, b} = {a, b}

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a b x✝ : α
⊢ x✝ ∈ ↑{a, b} ↔ x✝ ∈ {a, b}
-- Mathlib/Data/Bool/Basic.lean
theorem and_le_left : ∀ x y : Bool, (x && y) ≤ x

Proof state:
⊢ ∀ (x y : Bool), (x && y) ≤ x

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem Filter.EventuallyEq.hasFDerivAtFilter_iff (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x)
    (h₁ : ∀ x, f₀' x = f₁' x) : HasFDerivAtFilter f₀ f₀' x L ↔ HasFDerivAtFilter f₁ f₁' x L

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
L : Filter E
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : ∀ (x : E), f₀' x = f₁' x
y : E
hy : f₀ y = f₁ y
⊢ (fun x' => f₀ x' - f₀ x - f₀' (x' - x)) y = (fun x' => f₁ x' - f₁ x - f₁' (x' - x)) y

Tactic:
simp only [hy, h₁, hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
L : Filter E
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : ∀ (x : E), f₀' x = f₁' x
⊢ ((fun x' => f₀ x' - f₀ x - f₀' (x' - x)) =o[𝕜;L] fun x' => x' - x) ↔
    (fun x' => f₁ x' - f₁ x - f₁' (x' - x)) =o[𝕜;L] fun x' => x' - x

Tactic:
exact isLittleOTVS_congr (h₀.mono fun y hy => by simp only [hy, h₁, hx]) .rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
L : Filter E
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : ∀ (x : E), f₀' x = f₁' x
⊢ HasFDerivAtFilter f₀ f₀' x L ↔ HasFDerivAtFilter f₁ f₁' x L

Tactic:
simp only [hasFDerivAtFilter_iff_isLittleOTVS]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₀ f₁ : E → F
f₀' f₁' : E →L[𝕜] F
x : E
L : Filter E
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : ∀ (x : E), f₀' x = f₁' x
⊢ ((fun x' => f₀ x' - f₀ x - f₀' (x' - x)) =o[𝕜;L] fun x' => x' - x) ↔
    (fun x' => f₁ x' - f₁ x - f₁' (x' - x)) =o[𝕜;L] fun x' => x' - x
-- Mathlib/Data/List/Duplicate.lean
theorem duplicate_iff_two_le_count [DecidableEq α] : x ∈+ l ↔ 2 ≤ count x l

Proof state:
α : Type u_1
l : List α
x : α
inst✝ : DecidableEq α
⊢ x ∈+ l ↔ 2 ≤ count x l

Tactic:
simp [replicate_succ, duplicate_iff_sublist, le_count_iff_replicate_sublist]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem Measure.MeasureDense.nonempty (h𝒜 : μ.MeasureDense 𝒜) : 𝒜.Nonempty

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ μ ∅ ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ 0 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
⊢ 𝒜.Nonempty

Tactic:
exact ⟨t, ht⟩

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ 𝒜.Nonempty

Tactic:
rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by norm_num) with ⟨t, ht, -⟩

Result:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
⊢ 𝒜.Nonempty
-- Mathlib/GroupTheory/GroupAction/Hom.lean
lemma _root_.FaithfulSMul.of_injective
    [FaithfulSMul M' X] [MulActionHomClass F M' X Y] (f : F)
    (hf : Function.Injective f) :
    FaithfulSMul M' Y where
  eq_of_smul_eq_smul {_ _} h := eq_of_smul_eq_smul fun m ↦ hf <| by simp_rw [map_smul, h]

Proof state:
M' : Type u_1
X : Type u_5
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul M' Y
F : Type u_8
inst✝² : FunLike F X Y
inst✝¹ : FaithfulSMul M' X
inst✝ : MulActionHomClass F M' X Y
f : F
hf : Function.Injective ⇑f
x✝¹ x✝ : M'
h : ∀ (a : Y), x✝¹ • a = x✝ • a
m : X
⊢ f (x✝¹ • m) = f (x✝ • m)

Tactic:
simp_rw [map_smul, h]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem inter_filter (s t : Finset α) : s ∩ filter p t = filter p (s ∩ t)

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∩ filter p t = filter p (s ∩ t)

Tactic:
rw [inter_comm, filter_inter, inter_comm]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem card_nsmul_lt_card_nsmul_of_le_of_lt [∀ a b, Decidable (r a b)] (ht : t.Nonempty)
    (hm : ∀ a ∈ s, m ≤ #(t.bipartiteAbove r a))
    (hn : ∀ b ∈ t, #(s.bipartiteBelow r b) < n) : #s • m < #t • n :=
  calc
    _ ≤ ∑ a ∈ s, (#(t.bipartiteAbove r a) : R) := s.card_nsmul_le_sum _ _ hm
    _ = ∑ b ∈ t, (#(s.bipartiteBelow r b) : R)

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : StrictOrderedSemiring R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast

Result:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : StrictOrderedSemiring R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : StrictOrderedSemiring R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
@[reassoc (attr := simp)]
lemma extendHomologyIso_inv_homologyι :
    (K.extendHomologyIso e hj').inv ≫ (K.extend e).homologyι j' =
      K.homologyι j ≫ (K.extendOpcyclesIso e hj').inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extendHomologyIso e hj').inv ≫ (K.extend e).homologyι j' = K.homologyι j ≫ (K.extendOpcyclesIso e hj').inv

Tactic:
simp only [← cancel_epi (K.extendHomologyIso e hj').hom,
  Iso.hom_inv_id_assoc, extendHomologyIso_hom_homologyι_assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem to_ofList (l : List (Lists α)) : toList (ofList l) = l

Proof state:
α : Type u_1
l : List (Lists α)
⊢ (ofList l).toList = l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma μIso_inv_freeMk {X Y : Type u} (z : X ⊗ Y) :
    (μIso R X Y).inv (freeMk z) = freeMk z.1 ⊗ₜ freeMk z.2

Proof state:
R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ (ConcreteCategory.hom (μIso R X Y).inv) (freeMk z) = freeMk z.1 ⊗ₜ[R] freeMk z.2

Tactic:
dsimp [μIso, freeMk]

Result:
R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ ↑(finsuppTensorFinsupp' R X Y).symm (Finsupp.single z 1) = Finsupp.single z.1 1 ⊗ₜ[R] Finsupp.single z.2 1

Proof state:
R : Type u
inst✝ : CommRing R
X Y : Type u
z : X ⊗ Y
⊢ ↑(finsuppTensorFinsupp' R X Y).symm (Finsupp.single z 1) = Finsupp.single z.1 1 ⊗ₜ[R] Finsupp.single z.2 1

Tactic:
erw [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem one_nadd : 1 ♯ a = succ a

Proof state:
a : Ordinal.{u}
⊢ 1 ♯ a = succ a

Tactic:
rw [nadd_comm, nadd_one]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem aemeasurable_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E}
    (X : Ω → E) (h : ¬pdf X ℙ μ =ᵐ[μ] 0) : AEMeasurable X ℙ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬pdf X ℙ μ =ᶠ[ae μ] 0
⊢ AEMeasurable X ℙ

Tactic:
contrapose! h

Result:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬AEMeasurable X ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬AEMeasurable X ℙ
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
exact pdf_of_not_aemeasurable h

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
lemma frequently_iff_neBot {l : Filter α} {p : α → Prop} :
    (∃ᶠ x in l, p x) ↔ NeBot (l ⊓ 𝓟 {x | p x})

Proof state:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x | p x}).NeBot

Tactic:
rw [neBot_iff, Ne, inf_principal_eq_bot]

Result:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ {x | p x}ᶜ ∉ l

Proof state:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ {x | p x}ᶜ ∉ l

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem not_countable_univ_iff : ¬ (univ : Set α).Countable ↔ Uncountable α

Proof state:
α : Type u
⊢ ¬univ.Countable ↔ Uncountable α

Tactic:
rw [countable_univ_iff, not_countable_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem dist_le_tsum_of_dist_le_of_tendsto (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n)
    (hd : Summable d) {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ ∑' m, d (n + m)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ Summable fun k => d (n + k)

Tactic:
exact hd.comp_injective (add_right_injective n)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k ∈ range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ Summable fun k => d (n + k)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i ∈ Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i ∈ Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)

Tactic:
rw [sum_Ico_eq_sum_range]

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k ∈ range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
-- Mathlib/Topology/Constructions.lean
theorem discreteTopology_subtype_iff {S : Set X} :
    DiscreteTopology S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set X
⊢ DiscreteTopology ↑S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Tactic:
simp_rw [discreteTopology_iff_nhds_ne, SetCoe.forall', nhds_ne_subtype_eq_bot_iff]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Defs.lean
theorem Algebra.isAlgebraic_iff : Algebra.IsAlgebraic R A ↔ (⊤ : Subalgebra R A).IsAlgebraic

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ Algebra.IsAlgebraic R A ↔ ∀ x ∈ ⊤, IsAlgebraic R x

Tactic:
simp only [Algebra.isAlgebraic_def, Algebra.mem_top, forall_prop_of_true]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ Algebra.IsAlgebraic R A ↔ ⊤.IsAlgebraic

Tactic:
delta Subalgebra.IsAlgebraic

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ Algebra.IsAlgebraic R A ↔ ∀ x ∈ ⊤, IsAlgebraic R x
-- Mathlib/Order/Filter/Map.lean
theorem principal_subtype {α : Type*} (s : Set α) (t : Set s) :
    𝓟 t = comap (↑) (𝓟 (((↑) : s → α) '' t))

Proof state:
α : Type u_6
s : Set α
t : Set ↑s
⊢ 𝓟 t = comap Subtype.val (𝓟 (Subtype.val '' t))

Tactic:
rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem inner_rev_eq_zero_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) :
    ⟪y, x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ inner y x = 0

Tactic:
rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_pi_div_two h]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- One direction of `le_mul_inv_iff₀` where `c` is allowed to be `0` (but `b` must be nonnegative).
-/
lemma mul_le_of_le_mul_inv₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ b * c⁻¹) : a * c ≤ b

Proof state:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ b * 0⁻¹
⊢ a * 0 ≤ b

Tactic:
simpa using hb

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c⁻¹
⊢ a * c ≤ b

Tactic:
obtain rfl | hc := hc.eq_or_lt

Result:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ b * 0⁻¹
⊢ a * 0 ≤ b

case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
⊢ a * c ≤ b

Proof state:
case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
⊢ a * c ≤ b

Tactic:
rwa [le_mul_inv_iff₀ hc] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem add_nil (xs : IntList) : xs + [] = xs

Proof state:
xs : IntList
⊢ xs + [] = xs

Tactic:
simp [add_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem nthRoots_two_eq_zero_iff {r : R} : nthRoots 2 r = 0 ↔ ¬IsSquare r

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ nthRoots 2 r = 0 ↔ ¬IsSquare r

Tactic:
simp_rw [isSquare_iff_exists_sq, eq_zero_iff_forall_not_mem, mem_nthRoots (by norm_num : 0 < 2),
  ← not_exists, eq_comm]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a

Proof state:
a b : Prop
h : b = True
⊢ (a = b) = a

Tactic:
simp [h]

Result:
no goals