harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma StarOrderedRing.nonneg_iff_quasispectrum_nonneg [NonnegSpectrumClass R A] (a : A)
    (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.980659) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
⊢ 0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x

Tactic:
have := cfcₙ_nonneg_iff (id : R → R) a (by fun_prop)

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
this : 0 ≤ cfcₙ id a ↔ ∀ x ∈ σₙ R a, 0 ≤ id x
⊢ 0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
this : 0 ≤ cfcₙ id a ↔ ∀ x ∈ σₙ R a, 0 ≤ id x
⊢ 0 ≤ a ↔ ∀ x ∈ σₙ R a, 0 ≤ x

Tactic:
simpa [cfcₙ_id _ a ha] using this

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
⊢ ContinuousOn id (σₙ R a)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/CategoryTheory/Opposites.lean
theorem rightOp_leftOp_eq (F : Cᵒᵖ ⥤ D) : F.rightOp.leftOp = F

Proof state:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : Cᵒᵖ ⥤q D
map_id✝ : ∀ (X : Cᵒᵖ), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }.rightOp.leftOp =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
⊢ F.rightOp.leftOp = F

Tactic:
cases F

Result:
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : Cᵒᵖ ⥤q D
map_id✝ : ∀ (X : Cᵒᵖ), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }.rightOp.leftOp =
    { toPrefunctor := toPrefunctor✝, map_id := map_id✝, map_comp := map_comp✝ }
-- Mathlib/LinearAlgebra/Dual.lean
theorem ker_dualMap_eq_dualCoannihilator_range (f : M →ₗ[R] M') :
    LinearMap.ker f.dualMap = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ker f.dualMap = (range (Dual.eval R M' ∘ₗ f)).dualCoannihilator

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x : Dual R M'
⊢ x ∈ ker f.dualMap ↔ x ∈ (range (Dual.eval R M' ∘ₗ f)).dualCoannihilator

Proof state:
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x : Dual R M'
⊢ x ∈ ker f.dualMap ↔ x ∈ (range (Dual.eval R M' ∘ₗ f)).dualCoannihilator

Tactic:
simp [LinearMap.ext_iff (f := dualMap f x)]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp) zsmul_singleton]
lemma singleton_zpow (a : α) (n : ℤ) : ({a} : Set α) ^ n = {a ^ n}

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ {a} ^ n = {a ^ n}

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem dvd_iff_dvd_ofDigits (b b' : ℕ) (c : ℤ) (h : (b : ℤ) ∣ (b' : ℤ) - c) (n : ℕ) :
    b ∣ n ↔ (b : ℤ) ∣ ofDigits c (digits b' n)

Proof state:
b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ ↑b ∣ ↑n ↔ ↑b ∣ ofDigits c (b'.digits n)

Tactic:
exact
  dvd_iff_dvd_of_dvd_sub (zmodeq_ofDigits_digits b b' c (Int.modEq_iff_dvd.2 h).symm _).symm.dvd

Result:
no goals

Proof state:
b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ b ∣ n ↔ ↑b ∣ ofDigits c (b'.digits n)

Tactic:
rw [← Int.natCast_dvd_natCast]

Result:
b b' : ℕ
c : ℤ
h : ↑b ∣ ↑b' - c
n : ℕ
⊢ ↑b ∣ ↑n ↔ ↑b ∣ ofDigits c (b'.digits n)
-- Mathlib/Algebra/Field/Periodic.lean
theorem Periodic.mul_const' [DivisionSemiring α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (x * a)) (c / a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic (fun x => f (x * a)) (c / a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const a

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem bound_aux (hd : d ≠ 0) (hn : 2 ≤ n) :
    (d ^ (n - 2 :) / n : ℝ) ≤ rothNumberNat ((2 * d - 1) ^ n)

Proof state:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))

Tactic:
convert bound_aux' n d using 1

Result:
case h.e'_3
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n = ↑(d ^ n) / ↑(n * d ^ 2)

Proof state:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ≠ 0

Tactic:
rwa [cast_ne_zero]

Result:
no goals

Proof state:
case h.e'_3
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n = ↑(d ^ n) / ↑(n * d ^ 2)

Tactic:
rw [cast_mul, cast_pow, mul_comm, ← div_div, pow_sub₀ _ _ hn, ← div_eq_mul_inv, cast_pow]

Result:
n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_succ' {m n : Nat} : m ^ n.succ = m * m ^ n

Proof state:
m n : Nat
⊢ m ^ n.succ = m * m ^ n

Tactic:
rw [Nat.pow_succ, Nat.mul_comm]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_sin_oangle_add_left_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖x‖ / Real.Angle.sin (o.oangle (x + y) y) = ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (y + x)).sin = ‖y + x‖

Tactic:
exact (-o).norm_div_sin_oangle_add_right_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (x + y)).sin = ‖x + y‖

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (y + x)).sin = ‖y + x‖

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

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle y (x + y)).sin = ‖x + y‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_eq_some [DecidablePred p] : guard p a = some b ↔ a = b ∧ p a :=
  if h : p a then by simp [Option.guard, h] else by simp [Option.guard, h]

Proof state:
α✝ : Type u_1
p : α✝ → Prop
a b : α✝
inst✝ : DecidablePred p
h : ¬p a
⊢ guard p a = some b ↔ a = b ∧ p a

Tactic:
simp [Option.guard, h]

Result:
no goals

Proof state:
α✝ : Type u_1
p : α✝ → Prop
a b : α✝
inst✝ : DecidablePred p
h : p a
⊢ guard p a = some b ↔ a = b ∧ p a

Tactic:
simp [Option.guard, h]

Result:
no goals
-- Mathlib/Data/PNat/Find.lean
theorem one_le_find : 1 < PNat.find h ↔ ¬p 1 :=
  not_iff_not.mp <| by simp

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ ¬1 < PNat.find h ↔ ¬¬p 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Exposed.lean
theorem subset (hAB : IsExposed 𝕜 A B) : B ⊆ A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
⊢ x ∈ A

Tactic:
obtain ⟨_, rfl⟩ := hAB ⟨x, hx⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
w✝ : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}
hx : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}
⊢ x ∈ A

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
⊢ B ⊆ A

Tactic:
rintro x hx

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hAB : IsExposed 𝕜 A B
x : E
hx : x ∈ B
⊢ x ∈ A

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x : E
w✝ : E →L[𝕜] 𝕜
hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}
hx : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, w✝ y ≤ w✝ x}
⊢ x ∈ A

Tactic:
exact hx.1

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
theorem ConcreteCategory.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x = g x) : f = g

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), f x = g x
⊢ (forget C).map f = (forget C).map g

Tactic:
dsimp [forget]

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), f x = g x
⊢ HasForget.forget.map f = HasForget.forget.map g

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), f x = g x
⊢ HasForget.forget.map f = HasForget.forget.map g

Tactic:
funext x

Result:
case a.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), f x = g x
x : HasForget.forget.obj X
⊢ HasForget.forget.map f x = HasForget.forget.map g x

Proof state:
case a.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), f x = g x
x : HasForget.forget.obj X
⊢ HasForget.forget.map f x = HasForget.forget.map g x

Tactic:
exact w x

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), f x = g x
⊢ f = g

Tactic:
apply (forget C).map_injective

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), f x = g x
⊢ (forget C).map f = (forget C).map g
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.secondInter_neg (s : Sphere P) (p : P) (v : V) :
    s.secondInter p (-v) = s.secondInter p v

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ s.secondInter p (-v) = s.secondInter p v

Tactic:
rw [← neg_one_smul ℝ v, s.secondInter_smul p v (by norm_num : (-1 : ℝ) ≠ 0)]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
⊢ -1 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@[simp]
lemma span_eq_toSubmodule {R} [CommSemiring R] [Module R A] (s : NonUnitalStarSubalgebra R A) :
    Submodule.span R (s : Set A) = s.toSubmodule

Proof state:
A : Type v
inst✝³ : NonUnitalSemiring A
inst✝² : StarRing A
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R A
s : NonUnitalStarSubalgebra R A
⊢ Submodule.span R ↑s = s.toSubmodule

Tactic:
simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convolution.lean
/-- If we consider an arithmetic function just as a function and turn it back into an
arithmetic function, it is the same as before. -/
@[simp]
lemma ArithmeticFunction.toArithmeticFunction_eq_self {R : Type*} [Zero R]
    (f : ArithmeticFunction R) :
    toArithmeticFunction f = f

Proof state:
case h
R : Type u_1
inst✝ : Zero R
f : ArithmeticFunction R
n : ℕ
⊢ (toArithmeticFunction ⇑f) n = f n

Tactic:
simp +contextual [toArithmeticFunction]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Zero R
f : ArithmeticFunction R
⊢ toArithmeticFunction ⇑f = f

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : Zero R
f : ArithmeticFunction R
n : ℕ
⊢ (toArithmeticFunction ⇑f) n = f n
-- Mathlib/Data/Int/Lemmas.lean
theorem natAbs_lt_iff_sq_lt {a b : ℤ} : a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2

Proof state:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a ^ 2 < b ^ 2

Tactic:
rw [sq, sq]

Result:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Proof state:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b

Tactic:
exact natAbs_lt_iff_mul_self_lt

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem divInt_mul_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :
    (n₁ /. d₁) * (n₂ /. d₂) = (n₁ * n₂) /. (d₁ * d₂)

Proof state:
n₁ n₂ d₁ d₂ : Int
z₁ : d₁ ≠ 0
z₂ : d₂ ≠ 0
⊢ n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)

Tactic:
rcases Int.eq_nat_or_neg d₁ with ⟨_, rfl | rfl⟩ <;>
rcases Int.eq_nat_or_neg d₂ with ⟨_, rfl | rfl⟩ <;>
simp_all [-Int.natCast_mul, divInt_neg', Int.mul_neg, Int.ofNat_mul_ofNat,  Int.neg_mul,
  mkRat_mul_mkRat]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem isEmpty_iff_toList_eq_nil {t : RBSet α cmp} :
    t.isEmpty ↔ t.toList = []

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBSet α cmp
⊢ t.isEmpty = true ↔ t.toList = []

Tactic:
obtain ⟨⟨⟩, _⟩ := t <;> simp [toList, isEmpty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> y = x >>= fun _ => y

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ x *> y = do
    let _ ← x
    y

Tactic:
rw [seqRight_eq]

Result:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ const α id <$> x <*> y = do
    let _ ← x
    y

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ const α id <$> x <*> y = do
    let _ ← x
    y

Tactic:
simp only [map_eq_pure_bind, const, seq_eq_bind_map, bind_assoc, pure_bind, id_eq, bind_pure]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem finrank_euclideanSpace_fin {n : ℕ} :
    Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n

Proof state:
𝕜 : Type u_3
inst✝ : RCLike 𝕜
n : ℕ
⊢ Module.finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) = n

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem comp_whiskerRight_bimod {X Y Z : Mon_ C} {M N P : Bimod X Y} (f : M ⟶ N) (g : N ⟶ P)
    (Q : Bimod Y Z) : whiskerRight (f ≫ g) Q = whiskerRight f Q ≫ whiskerRight g Q

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N P : Bimod X Y
f : M ⟶ N
g : N ⟶ P
Q : Bimod Y Z
⊢ whiskerRight (f ≫ g) Q = whiskerRight f Q ≫ whiskerRight g Q

Tactic:
ext

Result:
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N P : Bimod X Y
f : M ⟶ N
g : N ⟶ P
Q : Bimod Y Z
⊢ (whiskerRight (f ≫ g) Q).hom = (whiskerRight f Q ≫ whiskerRight g Q).hom

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N P : Bimod X Y
f : M ⟶ N
g : N ⟶ P
Q : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫ (whiskerRight (f ≫ g) Q).hom =
    coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫
      (whiskerRight f Q ≫ whiskerRight g Q).hom

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N P : Bimod X Y
f : M ⟶ N
g : N ⟶ P
Q : Bimod Y Z
⊢ (whiskerRight (f ≫ g) Q).hom = (whiskerRight f Q ≫ whiskerRight g Q).hom

Tactic:
apply Limits.coequalizer.hom_ext

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M N P : Bimod X Y
f : M ⟶ N
g : N ⟶ P
Q : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫ (whiskerRight (f ≫ g) Q).hom =
    coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫
      (whiskerRight f Q ≫ whiskerRight g Q).hom
-- Mathlib/Data/Finsupp/AList.lean
theorem lookupFinsupp_eq_zero_iff [DecidableEq α] {l : AList fun _x : α => M} {a : α} :
    l.lookupFinsupp a = 0 ↔ a ∉ l ∨ (0 : M) ∈ l.lookup a

Proof state:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ lookup a l

Tactic:
rw [lookupFinsupp_apply, ← lookup_eq_none]

Result:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ (lookup a l).getD 0 = 0 ↔ lookup a l = none ∨ 0 ∈ lookup a l

Proof state:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ (lookup a l).getD 0 = 0 ↔ lookup a l = none ∨ 0 ∈ lookup a l

Tactic:
rcases lookup a l with - | m <;> simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma sub_iSup [Nonempty ι] (ha : a ≠ ∞) : a - ⨆ i, f i = ⨅ i, a - f i

Proof state:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ f i ≤ a - ⨅ i, a - f i

Tactic:
rw [← sub_sub_cancel ha (h _)]

Result:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ i, a - f i

Proof state:
case inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ ∀ b > ⊥, ∃ i, a - f i < b

Tactic:
exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩

Result:
no goals

Proof state:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
refine le_antisymm (le_iInf fun i ↦ tsub_le_tsub_left (le_iSup ..) _) <|
  ENNReal.le_sub_of_add_le_left (ne_top_of_le_ne_top ha <| iSup_le h) <|
  add_le_of_le_tsub_right_of_le (iInf_le_of_le (Classical.arbitrary _) tsub_le_self) <|
  iSup_le fun i ↦ ?_

Result:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ f i ≤ a - ⨅ i, a - f i

Proof state:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
simp_rw [not_exists, not_lt] at h

Result:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)

Result:
case inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
x : ℝ≥0∞
hx : x > ⊥
⊢ a - f i < x

Tactic:
simpa [hi.le, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
case inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
rw [tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le, (iInf_eq_bot _).2, bot_eq_zero]

Result:
case inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ ∀ b > ⊥, ∃ i, a - f i < b
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem ι_sndSigmaMap (b) : Sigma.ι I.left b ≫ I.sndSigmaMap = I.snd b ≫ Sigma.ι I.right _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.L
⊢ Sigma.ι I.left b ≫ I.sndSigmaMap = I.snd b ≫ Sigma.ι I.right (J.snd b)

Tactic:
simp [sndSigmaMap]

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem map_sub (a b : R) : abv (a - b) = abv (b - a)

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a b : R
⊢ abv (a - b) = abv (b - a)

Tactic:
rw [← neg_sub, abv.map_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_lo_1 (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w + k₂ ≤ v → u ≤ v + (k₁ - k₂)

Proof state:
u w v k₁ k₂ : Nat
⊢ u ≤ w + k₁ → w + k₂ ≤ v → u ≤ v + (k₁ - k₂)

Tactic:
omega

Result:
no goals