harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem neg_le_natAbs {a : Int} : -a ≤ a.natAbs

Proof state:
a : Int
t : -a ≤ ↑a.natAbs
⊢ -a ≤ ↑a.natAbs

Tactic:
exact t

Result:
no goals

Proof state:
a : Int
⊢ -a ≤ ↑a.natAbs

Tactic:
have t := Int.le_natAbs (a := -a)

Result:
a : Int
t : -a ≤ ↑(-a).natAbs
⊢ -a ≤ ↑a.natAbs

Proof state:
a : Int
t : -a ≤ ↑(-a).natAbs
⊢ -a ≤ ↑a.natAbs

Tactic:
simp at t

Result:
a : Int
t : -a ≤ ↑a.natAbs
⊢ -a ≤ ↑a.natAbs
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.const_smul [AddMonoid α] [Neg β] [Group γ] [DistribMulAction γ α]
    (h : Antiperiodic f c) (a : γ) : Antiperiodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
  simpa only [smul_add, smul_inv_smul] using h (a • x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = -(fun x => f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul] using h (a • x)

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
theorem filter_True {h} (s : Finset α) : @filter _ (fun _ => True) h s = s

Proof state:
α : Type u_1
h : DecidablePred fun x => True
s : Finset α
⊢ filter (fun x => True) s = s

Tactic:
ext

Result:
case h
α : Type u_1
h : DecidablePred fun x => True
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x => True) s ↔ a✝ ∈ s

Proof state:
case h
α : Type u_1
h : DecidablePred fun x => True
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x => True) s ↔ a✝ ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
theorem hasInitial_of_hasInitial_of_preservesColimit [PreservesColimit (Functor.empty.{0} C) G] :
    HasInitial D :=
  ⟨fun F => by
    haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
    apply hasColimitOfIso F.uniqueFromEmpty⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
this : HasColimit (Functor.empty D)
⊢ HasColimit F

Tactic:
apply hasColimitOfIso F.uniqueFromEmpty

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasColimit F

Tactic:
haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
this : HasColimit (Functor.empty D)
⊢ HasColimit F
-- Mathlib/Order/WithBot.lean
lemma unbot_lt_iff (hx : x ≠ ⊥) : unbot x hx < b ↔ x < b

Proof state:
case intro
α : Type u_1
b : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx < b ↔ ↑x < ↑b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
b : α
inst✝ : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx < b ↔ x < ↑b

Tactic:
lift x to α using id hx

Result:
case intro
α : Type u_1
b : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊥
⊢ (↑x).unbot hx < b ↔ ↑x < ↑b
-- Mathlib/NumberTheory/Divisors.lean
@[simp]
lemma sup_divisors_id (n : ℕ) : n.divisors.sup id = n

Proof state:
case inl

⊢ 0 ≤ (divisors 0).sup id

Tactic:
apply zero_le

Result:
no goals

Proof state:
case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id

Tactic:
exact Finset.le_sup (f := id) <| mem_divisors_self n hn

Result:
no goals

Proof state:
n : ℕ
⊢ n.divisors.sup id = n

Tactic:
refine le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_

Result:
n : ℕ
⊢ n ≤ n.divisors.sup id

Proof state:
n : ℕ
⊢ n ≤ n.divisors.sup id

Tactic:
rcases Decidable.eq_or_ne n 0 with rfl | hn

Result:
case inl

⊢ 0 ≤ (divisors 0).sup id

case inr
n : ℕ
hn : n ≠ 0
⊢ n ≤ n.divisors.sup id
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_counitInv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
    (g' : X' ⟶ Y) : f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
W X X' Y : D
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma antivary_inv₀ (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Antivary f⁻¹ g⁻¹ ↔ Antivary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
f : ι → α
g : ι → β
hf : StrongLT 0 f
hg : StrongLT 0 g
⊢ Antivary f⁻¹ g⁻¹ ↔ Antivary f g

Tactic:
rw [antivary_inv_left₀ hf, monovary_inv_right₀ hg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_alter [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')]
    {f : Option (β k) → Option (β k)} (h : m.WF) : (m.alter k f).get! k' =
      if heq : k == k' then
        (f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get!
      else
        m.get! k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
hi : Inhabited (β k')
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).get! k' = if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).get! else m.get! k'

Tactic:
simp_to_raw using Raw₀.get!_alter

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_compl [DecidableEq ι] (s : Finset ι) [∀ i, Decidable (i ∈ s)]
    [∀ i, Decidable (i ∈ sᶜ)] (f g : ∀ i, π i) :
    sᶜ.piecewise f g = s.piecewise g f

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
s : Finset ι
inst✝¹ : (i : ι) → Decidable (i ∈ s)
inst✝ : (i : ι) → Decidable (i ∈ sᶜ)
f g : (i : ι) → π i
i : ι
⊢ sᶜ.piecewise f g i = s.piecewise g f i

Tactic:
simp [piecewise]

Result:
no goals

Proof state:
ι : Type u_1
π : ι → Sort u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
s : Finset ι
inst✝¹ : (i : ι) → Decidable (i ∈ s)
inst✝ : (i : ι) → Decidable (i ∈ sᶜ)
f g : (i : ι) → π i
⊢ sᶜ.piecewise f g = s.piecewise g f

Tactic:
ext i

Result:
case h
ι : Type u_1
π : ι → Sort u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
s : Finset ι
inst✝¹ : (i : ι) → Decidable (i ∈ s)
inst✝ : (i : ι) → Decidable (i ∈ sᶜ)
f g : (i : ι) → π i
i : ι
⊢ sᶜ.piecewise f g i = s.piecewise g f i
-- Mathlib/Data/Nat/Sqrt.lean
/-- There are no perfect squares strictly between m² and (m+1)² -/
lemma not_exists_sq (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ t, t * t = n

Proof state:
m n : ℕ
hl : m * m < n
hr : n < (m + 1) * (m + 1)
⊢ ¬∃ t, t * t = n

Tactic:
rintro ⟨t, rfl⟩

Result:
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False

Proof state:
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False

Tactic:
have h1 : m < t := Nat.mul_self_lt_mul_self_iff.1 hl

Result:
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False

Proof state:
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
⊢ False

Tactic:
have h2 : t < m + 1 := Nat.mul_self_lt_mul_self_iff.1 hr

Result:
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False

Proof state:
case intro
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
h1 : m < t
h2 : t < m + 1
⊢ False

Tactic:
exact (not_lt_of_ge <| le_of_lt_succ h2) h1

Result:
no goals
-- Mathlib/Order/Interval/Basic.lean
theorem dual_map (f : α →o β) (s : Interval α) : dual (s.map f) = s.dual.map f.dual

Proof state:
case bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ dual (map f ⊥) = map (OrderHom.dual f) (dual ⊥)

Tactic:
rfl

Result:
no goals

Proof state:
case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
a✝ : NonemptyInterval α
⊢ dual (map f ↑a✝) = map (OrderHom.dual f) (dual ↑a✝)

Tactic:
exact WithBot.map_comm rfl _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
s : Interval α
⊢ dual (map f s) = map (OrderHom.dual f) (dual s)

Tactic:
cases s

Result:
case bot
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ dual (map f ⊥) = map (OrderHom.dual f) (dual ⊥)

case coe
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
a✝ : NonemptyInterval α
⊢ dual (map f ↑a✝) = map (OrderHom.dual f) (dual ↑a✝)
-- Mathlib/Probability/Kernel/RadonNikodym.lean
@[fun_prop]
lemma measurable_rnDeriv (κ η : Kernel α γ) :
    Measurable (fun p : α × γ ↦ rnDeriv κ η p.1 p.2)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p => κ.rnDeriv η p.1 p.2

Tactic:
simp_rw [rnDeriv_def]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p => ENNReal.ofReal (κ.rnDerivAux (κ + η) p.1 p.2) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) p.1 p.2)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
⊢ Measurable fun p => ENNReal.ofReal (κ.rnDerivAux (κ + η) p.1 p.2) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) p.1 p.2)

Tactic:
exact (measurable_rnDerivAux κ _).ennreal_ofReal.div
  (measurable_const.sub (measurable_rnDerivAux κ _)).ennreal_ofReal

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
theorem pointwise_vadd_bot (v : V) : v +ᵥ (⊥ : AffineSubspace k P) = ⊥

Proof state:
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
⊢ v +ᵥ ⊥ = ⊥

Tactic:
ext

Result:
case h
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥

Proof state:
case h
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
x✝ : P
⊢ x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥

Tactic:
simp [pointwise_vadd_eq_map, map_bot]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_nonneg : 0 ≤ (q : K) ↔ 0 ≤ q

Proof state:
q : ℚ
K : Type u_5
inst✝ : LinearOrderedField K
⊢ 0 ≤ ↑q ↔ 0 ≤ q

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
lemma log_netMaxcard_nonneg (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) (n : ℕ) :
    0 ≤ log (netMaxcard T F U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 0 ≤ (↑(netMaxcard T F U n)).log

Tactic:
apply zero_le_log_iff.2

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ ↑(netMaxcard T F U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ ↑(netMaxcard T F U n)

Tactic:
rw [← ENat.toENNReal_one, ENat.toENNReal_le]

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ netMaxcard T F U n

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ netMaxcard T F U n

Tactic:
exact (one_le_netMaxcard_iff T F U n).2 h

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem toReal_div (a b : ℝ≥0∞) : (a / b).toReal = a.toReal / b.toReal

Proof state:
a b : ℝ≥0∞
⊢ (a / b).toReal = a.toReal / b.toReal

Tactic:
rw [div_eq_mul_inv, toReal_mul, toReal_inv, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma InfClosed.image [FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) :
    InfClosed (f '' s)

Proof state:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a ⊓ f b ∈ ⇑f '' s

Tactic:
rw [← map_inf]

Result:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f (a ⊓ b) ∈ ⇑f '' s

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
hs : InfClosed s
f : F
⊢ InfClosed (⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩

Result:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a ⊓ f b ∈ ⇑f '' s

Proof state:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
hs : InfClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f (a ⊓ b) ∈ ⇑f '' s

Tactic:
exact Set.mem_image_of_mem _ <| hs ha hb

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem coeff_single_same (a : Γ) (r : R) : (single a r).coeff a = r

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).coeff a = r

Tactic:
classical exact Pi.single_eq_same (f := fun _ => R) a r

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a : Γ
r : R
⊢ ((single a) r).coeff a = r

Tactic:
exact Pi.single_eq_same (f := fun _ => R) a r

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem ne_bot_iff (p : Submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ (0 : M)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0

Tactic:
simp only [ne_eq, p.eq_bot_iff, not_forall, exists_prop]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem le_of_mem_S_compl {f : C(I, ℝ)} {ε : ℝ} {h : 0 < ε} {n : ℕ} {x : I} {k : Fin (n + 1)}
    (m : k ∈ (S f ε h n x)ᶜ) : (1 : ℝ) ≤ δ f ε h ^ (-2 : ℤ) * ((x : ℝ) - k/ₙ) ^ 2

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : δ f ε h ≤ dist k/ₙ x
⊢ 1 ≤ δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2

Tactic:
rw [zpow_neg, ← div_eq_inv_mul, zpow_two, ← pow_two, one_le_div (pow_pos δ_pos 2), sq_le_sq,
  abs_of_pos δ_pos]

Result:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : δ f ε h ≤ dist k/ₙ x
⊢ δ f ε h ≤ |↑x - ↑k/ₙ|

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ (S f ε h n x)ᶜ
⊢ 1 ≤ δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2

Tactic:
simp only [Finset.mem_compl, not_lt, Set.mem_toFinset, Set.mem_setOf_eq, S] at m

Result:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : δ f ε h ≤ dist k/ₙ x
⊢ 1 ≤ δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : δ f ε h ≤ dist k/ₙ x
⊢ δ f ε h ≤ |↑x - ↑k/ₙ|

Tactic:
rwa [dist_comm] at m

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma chainLength_zero_right [Nontrivial L] (hα : α.IsNonZero) : chainLength α 0 = 2

Proof state:
K : Type u_1
L : Type u_2
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra K L
inst✝⁴ : IsKilling K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst✝ : Nontrivial L
hα : α.IsNonZero
⊢ chainLength α 0 = 2

Tactic:
rw [← chainBotCoeff_add_chainTopCoeff, chainTopCoeff_zero_right α hα,
  chainBotCoeff_zero_right α hα]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem exists_rat_eq_nth_den : ∃ q : ℚ, (of v).dens n = (q : K)

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a✝, b := b }
⊢ (of v).dens n = ↑b

Tactic:
simp [den_eq_conts_b, nth_cont_eq]

Result:
no goals

Proof state:
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a✝, b := b }
⊢ ∃ q, (of v).dens n = ↑q

Tactic:
use b

Result:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a✝, b := b }
⊢ (of v).dens n = ↑b

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, (of v).dens n = ↑q

Tactic:
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨_, b⟩, nth_cont_eq⟩

Result:
case intro.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
a✝ b : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a✝, b := b }
⊢ ∃ q, (of v).dens n = ↑q
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_sum {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι → 𝕜)
    (s : Finset ι) : ⟪∑ i ∈ s, l₁ i • v i, ∑ i ∈ s, l₂ i • v i⟫ = ∑ i ∈ s, conj (l₁ i) * l₂ i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ ∑ x ∈ s, (starRingEnd 𝕜) (l₁ x) * inner (v x) (∑ i ∈ s, l₂ i • v i) = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i

Tactic:
refine Finset.sum_congr rfl fun i hi => ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ (starRingEnd 𝕜) (l₁ i) * inner (v i) (∑ i ∈ s, l₂ i • v i) = (starRingEnd 𝕜) (l₁ i) * l₂ i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ (starRingEnd 𝕜) (l₁ i) * inner (v i) (∑ i ∈ s, l₂ i • v i) = (starRingEnd 𝕜) (l₁ i) * l₂ i

Tactic:
rw [hv.inner_right_sum l₂ hi]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ inner (∑ i ∈ s, l₁ i • v i) (∑ i ∈ s, l₂ i • v i) = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i

Tactic:
simp_rw [sum_inner, inner_smul_left]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι → 𝕜
s : Finset ι
⊢ ∑ x ∈ s, (starRingEnd 𝕜) (l₁ x) * inner (v x) (∑ i ∈ s, l₂ i • v i) = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma inv_hom_apply {R S : RingCat} (e : R ≅ S) (r : R) : e.inv (e.hom r) = r

Proof state:
R S : RingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_one' : a / b ≤ 1 ↔ a ≤ b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem measurable_const_smul_iff (c : G) : (Measurable fun x => c • f x) ↔ Measurable f :=
  ⟨fun h => by simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹, fun h => h.const_smul c⟩

Proof state:
β : Type u_3
α : Type u_4
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace α
f : α → β
G : Type u_5
inst✝³ : Group G
inst✝² : MeasurableSpace G
inst✝¹ : MulAction G β
inst✝ : MeasurableSMul G β
c : G
h : Measurable fun x => c • f x
⊢ Measurable f

Tactic:
simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem iSup_rayleigh_eq_iSup_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
    ⨆ x : { x : E // x ≠ 0 }, rayleighQuotient T x =
      ⨆ x : sphere (0 : E) r, rayleighQuotient T x :=
  show ⨆ x : ({0}ᶜ : Set E), rayleighQuotient T x = _ by
    simp only [← @sSup_image' _ _ _ _ (rayleighQuotient T),
      T.image_rayleigh_eq_image_rayleigh_sphere hr]

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
⊢ ⨆ x, T.rayleighQuotient ↑x = ⨆ x, T.rayleighQuotient ↑x

Tactic:
simp only [← @sSup_image' _ _ _ _ (rayleighQuotient T),
  T.image_rayleigh_eq_image_rayleigh_sphere hr]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma self_add_sub_one : ∀ n, n + (n - 1) = 2 * n - 1
  | 0 => rfl
  | n + 1 => by rw [Nat.two_mul]; exact (add_succ_sub_one (Nat.succ _) _).symm

Proof state:
n : ℕ
⊢ n + 1 + (n + 1 - 1) = 2 * (n + 1) - 1

Tactic:
rw [Nat.two_mul]

Result:
n : ℕ
⊢ n + 1 + (n + 1 - 1) = n + 1 + (n + 1) - 1

Proof state:
n : ℕ
⊢ n + 1 + (n + 1 - 1) = n + 1 + (n + 1) - 1

Tactic:
exact (add_succ_sub_one (Nat.succ _) _).symm

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_apply_right (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = g.sum fun a b => f (x * a⁻¹) * b :=
  calc
    (f * g) x = sum g fun a b => (f * single a b) x

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Group G
f g : MonoidAlgebra k G
x : G
⊢ (f * g) x = sum g fun a b => (f * single a b) x

Tactic:
rw [← Finsupp.sum_apply, ← Finsupp.mul_sum f g, g.sum_single]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Group G
f g : MonoidAlgebra k G
x : G
⊢ (sum g fun a b => (f * single a b) x) = sum g fun a b => f (x * a⁻¹) * b

Tactic:
simp only [mul_single_apply, Finsupp.sum]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Ici_of_neg (a : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ici a = Iic (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a c : α
h : c < 0
⊢ (fun x => c * x) ⁻¹' Ici a = Iic (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ici_of_neg a h

Result:
no goals
-- Mathlib/Topology/Constructible.lean
@[simp] lemma IsRetrocompact.univ : IsRetrocompact (univ : Set X)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
⊢ IsRetrocompact Set.univ

Tactic:
simp +contextual [IsRetrocompact]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_zero (x : BitVec n) : x - 0#n = x

Proof state:
case a
n : Nat
x : BitVec n
⊢ (x - 0#n).toNat = x.toNat

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
x : BitVec n
⊢ x - 0#n = x

Tactic:
apply eq_of_toNat_eq

Result:
case a
n : Nat
x : BitVec n
⊢ (x - 0#n).toNat = x.toNat
-- Mathlib/Data/PNat/Interval.lean
theorem card_Ioo : #(Ioo a b) = b - a - 1

Proof state:
a b : ℕ+
⊢ #(Ioo a b) = ↑b - ↑a - 1

Tactic:
rw [← Nat.card_Ioo, ← map_subtype_embedding_Ioo, card_map]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem pow_eq_one_iff_dvd (h : IsPrimitiveRoot ζ k) (l : ℕ) : ζ ^ l = 1 ↔ k ∣ l :=
  ⟨h.dvd_of_pow_eq_one l, by
    rintro ⟨i, rfl⟩; simp only [pow_mul, h.pow_eq_one, one_pow]⟩

Proof state:
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
l : ℕ
⊢ k ∣ l → ζ ^ l = 1

Tactic:
rintro ⟨i, rfl⟩

Result:
case intro
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ζ ^ (k * i) = 1

Proof state:
case intro
M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : M
h : IsPrimitiveRoot ζ k
i : ℕ
⊢ ζ ^ (k * i) = 1

Tactic:
simp only [pow_mul, h.pow_eq_one, one_pow]

Result:
no goals