harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toSignedMeasure_sub_apply {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    {i : Set α} (hi : MeasurableSet i) :
    (μ.toSignedMeasure - ν.toSignedMeasure) i = (μ i).toReal - (ν i).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.toSignedMeasure - ν.toSignedMeasure) i = (μ i).toReal - (ν i).toReal

Tactic:
rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
  Measure.toSignedMeasure_apply_measurable hi]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem mul_cpow_ofReal_nonneg {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (r : ℂ) :
    ((a : ℂ) * (b : ℂ)) ^ r = (a : ℂ) ^ r * (b : ℂ) ^ r

Proof state:
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
have ha'' : (a : ℂ) ≠ 0 := ofReal_ne_zero.mpr ha'.ne'

Result:
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Proof state:
case inl
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (↑a * ↑b) ^ 0 = ↑a ^ 0 * ↑b ^ 0

Tactic:
simp only [cpow_zero, mul_one]

Result:
no goals

Proof state:
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
have hb'' : (b : ℂ) ≠ 0 := ofReal_ne_zero.mpr hb'.ne'

Result:
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Proof state:
case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
ha'' : ↑a ≠ 0
hb'' : ↑b ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
rw [cpow_def_of_ne_zero (mul_ne_zero ha'' hb''), log_ofReal_mul ha' hb'', ofReal_log ha,
  add_mul, exp_add, ← cpow_def_of_ne_zero ha'', ← cpow_def_of_ne_zero hb'']

Result:
no goals

Proof state:
case inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
rcases eq_or_lt_of_le ha with (rfl | ha')

Result:
case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ (↑0 * ↑b) ^ r = ↑0 ^ r * ↑b ^ r

case inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Proof state:
case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ (↑a * ↑0) ^ r = ↑a ^ r * ↑0 ^ r

Tactic:
rw [ofReal_zero, mul_zero, zero_cpow hr, mul_zero]

Result:
no goals

Proof state:
case inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
rcases eq_or_lt_of_le hb with (rfl | hb')

Result:
case inr.inr.inl
a : ℝ
ha : 0 ≤ a
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb : 0 ≤ 0
⊢ (↑a * ↑0) ^ r = ↑a ^ r * ↑0 ^ r

case inr.inr.inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha' : 0 < a
hb' : 0 < b
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Proof state:
case inr.inl
b : ℝ
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
ha : 0 ≤ 0
⊢ (↑0 * ↑b) ^ r = ↑0 ^ r * ↑b ^ r

Tactic:
rw [ofReal_zero, zero_mul, zero_cpow hr, zero_mul]

Result:
no goals

Proof state:
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Result:
case inl
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (↑a * ↑b) ^ 0 = ↑a ^ 0 * ↑b ^ 0

case inr
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
r : ℂ
hr : r ≠ 0
⊢ (↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianReal_absolutelyContinuous' (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) :
    volume ≪ gaussianReal μ v

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ gaussianReal μ v

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv]

Result:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ ℙ.withDensity (gaussianPDF μ v)

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ ℙ.withDensity (gaussianPDF μ v)

Tactic:
refine withDensity_absolutelyContinuous' ?_ ?_

Result:
case refine_1
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ AEMeasurable (gaussianPDF μ v) ℙ

case refine_2
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0

Proof state:
case refine_1
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ AEMeasurable (gaussianPDF μ v) ℙ

Tactic:
exact (measurable_gaussianPDF _ _).aemeasurable

Result:
no goals

Proof state:
case refine_2
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0

Tactic:
exact ae_of_all _ (fun _ ↦ (gaussianPDF_pos _ hv _).ne')

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
lemma le_log_one_add_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 2 * x / (x + 2) ≤ log (1 + x)

Proof state:
x : ℝ
hx : 0 ≤ x
j✝ : ℕ
a✝ : j✝ ≠ 0
⊢ 0 ≤ 2 * (1 / (2 * ↑j✝ + 1)) * (x / (x + 2)) ^ (2 * j✝ + 1)

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ ∀ (j : ℕ), j ≠ 0 → 0 ≤ 2 * (1 / (2 * ↑j + 1)) * (x / (x + 2)) ^ (2 * j + 1)

Tactic:
intros

Result:
x : ℝ
hx : 0 ≤ x
j✝ : ℕ
a✝ : j✝ ≠ 0
⊢ 0 ≤ 2 * (1 / (2 * ↑j✝ + 1)) * (x / (x + 2)) ^ (2 * j✝ + 1)

Proof state:
case h.e'_3
x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) = 2 * (1 / (2 * ↑0 + 1)) * (x / (x + 2)) ^ (2 * 0 + 1)

Tactic:
field_simp

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) ≤ log (1 + x)

Tactic:
convert le_hasSum (hasSum_log_one_add hx) 0 (by intros; positivity) using 1

Result:
case h.e'_3
x : ℝ
hx : 0 ≤ x
⊢ 2 * x / (x + 2) = 2 * (1 / (2 * ↑0 + 1)) * (x / (x + 2)) ^ (2 * 0 + 1)
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem mapForget_eq {X Y : T} (f : X ⟶ Y) :
    (map f) ⋙ (forget Y) = (forget X)

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ autoParam
    (∀ (X_1 Y_1 : Over X) (f_1 : X_1 ⟶ Y_1), (map f ⋙ forget Y).map f_1 = eqToHom ⋯ ≫ (forget X).map f_1 ≫ eqToHom ⋯)
    _auto✝

Tactic:
intros x y u

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x y : Over X
u : x ⟶ y
⊢ (map f ⋙ forget Y).map u = eqToHom ⋯ ≫ (forget X).map u ≫ eqToHom ⋯

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x y : Over X
u : x ⟶ y
⊢ (map f ⋙ forget Y).map u = eqToHom ⋯ ≫ (forget X).map u ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x : CostructuredArrow (𝟭 T) X
⊢ x.left = x.left

Tactic:
exact rfl

Result:
no goals

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X_1 : Over X), (map f ⋙ forget Y).obj X_1 = (forget X).obj X_1

Tactic:
dsimp [Over, Over.map]

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X_1 : CostructuredArrow (𝟭 T) X), X_1.left = X_1.left

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X_1 : CostructuredArrow (𝟭 T) X), X_1.left = X_1.left

Tactic:
intro x

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
x : CostructuredArrow (𝟭 T) X
⊢ x.left = x.left

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ map f ⋙ forget Y = forget X

Tactic:
fapply Functor.ext

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ ∀ (X_1 : Over X), (map f ⋙ forget Y).obj X_1 = (forget X).obj X_1

case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y : T
f : X ⟶ Y
⊢ autoParam
    (∀ (X_1 Y_1 : Over X) (f_1 : X_1 ⟶ Y_1), (map f ⋙ forget Y).map f_1 = eqToHom ⋯ ≫ (forget X).map f_1 ≫ eqToHom ⋯)
    _auto✝
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
lemma weightedVSub_vadd {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0) (p : ι → P) (v : V) :
    s.weightedVSub (v +ᵥ p) w = s.weightedVSub p w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
v : V
⊢ (s.weightedVSub (v +ᵥ p)) w = (s.weightedVSub p) w

Tactic:
rw [weightedVSub, weightedVSubOfPoint_vadd,
  weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero _ _ _ h]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem nonempty : (spectrum ℂ a).Nonempty

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
⊢ False

Tactic:
have H₁ : Differentiable ℂ fun z : ℂ => resolvent a z := fun z =>
  (hasDerivAt_resolvent (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)).differentiableAt

Result:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z => resolvent a z
⊢ False

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
⊢ False

Tactic:
have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h

Result:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
⊢ False

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z => resolvent a z
⊢ False

Tactic:
have H₃ := H₁.apply_eq_of_tendsto_cocompact 0 <| by
  simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)

Result:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z => resolvent a z
H₃ : resolvent a 0 = 0
⊢ False

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z => resolvent a z
H₃ : resolvent a 0 = 0
⊢ False

Tactic:
exact not_isUnit_zero <| H₃ ▸ (isUnit_resolvent.mp <| H₀.symm ▸ Set.mem_univ 0)

Result:
no goals

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
H₀ : resolventSet ℂ a = Set.univ
H₁ : Differentiable ℂ fun z => resolvent a z
⊢ Filter.Tendsto (fun z => resolvent a z) (Filter.cocompact ℂ) (𝓝 ?m.270875)

Tactic:
simpa [Metric.cobounded_eq_cocompact] using resolvent_tendsto_cobounded a (𝕜 := ℂ)

Result:
no goals

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
⊢ (spectrum ℂ a).Nonempty

Tactic:
by_contra! h

Result:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
⊢ False

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
h : spectrum ℂ a = ∅
⊢ resolventSet ℂ a = Set.univ

Tactic:
rwa [spectrum, Set.compl_empty_iff] at h

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem absNorm_eq_zero_iff [NoZeroDivisors K] {I : FractionalIdeal R⁰ K} :
    absNorm I = 0 ↔ I = 0

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Module.Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : NoZeroDivisors K
I : FractionalIdeal R⁰ K
⊢ absNorm I = 0 ↔ I = 0

Tactic:
refine ⟨fun h ↦ zero_of_num_eq_bot zero_not_mem_nonZeroDivisors ?_, fun h ↦ h ▸ absNorm_bot⟩

Result:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Module.Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : NoZeroDivisors K
I : FractionalIdeal R⁰ K
h : absNorm I = 0
⊢ I.num = ⊥

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Module.Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : NoZeroDivisors K
I : FractionalIdeal R⁰ K
h : ↑(Ideal.absNorm I.num) = 0 ∨ ↑|(Algebra.norm ℤ) ↑I.den| = 0
⊢ ¬↑|(Algebra.norm ℤ) ↑I.den| = 0

Tactic:
simp [Algebra.norm_eq_zero_iff]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Module.Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : NoZeroDivisors K
I : FractionalIdeal R⁰ K
h : ↑(Ideal.absNorm I.num) = 0 ∨ ↑|(Algebra.norm ℤ) ↑I.den| = 0
⊢ I.num = ⊥

Tactic:
refine Ideal.absNorm_eq_zero_iff.mp <| Nat.cast_eq_zero.mp <| h.resolve_right ?_

Result:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Module.Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : NoZeroDivisors K
I : FractionalIdeal R⁰ K
h : ↑(Ideal.absNorm I.num) = 0 ∨ ↑|(Algebra.norm ℤ) ↑I.den| = 0
⊢ ¬↑|(Algebra.norm ℤ) ↑I.den| = 0

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Module.Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : NoZeroDivisors K
I : FractionalIdeal R⁰ K
h : absNorm I = 0
⊢ I.num = ⊥

Tactic:
rw [absNorm_eq, div_eq_zero_iff] at h

Result:
R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsDedekindDomain R
inst✝⁵ : Module.Free ℤ R
inst✝⁴ : Module.Finite ℤ R
K : Type u_2
inst✝³ : CommRing K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : NoZeroDivisors K
I : FractionalIdeal R⁰ K
h : ↑(Ideal.absNorm I.num) = 0 ∨ ↑|(Algebra.norm ℤ) ↑I.den| = 0
⊢ I.num = ⊥
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_le_add_add_tsub : a + b ≤ a + c + (b - c)

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))

Tactic:
exact add_le_add_left le_add_tsub a

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + c + (b - c)

Tactic:
rw [add_assoc]

Result:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a + (c + (b - c))
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem pullback_id (x : Subobject X) : (pullback (𝟙 X)).obj x = x

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
x : Subobject X
⊢ (pullback (𝟙 X)).obj x = x

Tactic:
induction' x using Quotient.inductionOn' with f

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
f : MonoOver X
⊢ (pullback (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
inst✝ : HasPullbacks C
f : MonoOver X
⊢ (pullback (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
exact Quotient.sound ⟨MonoOver.pullbackId.app f⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem get_append_left {a b : ByteArray} (hlt : i < a.size)
    (h : i < (a ++ b).size := size_append .. ▸ Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)) :
    (a ++ b)[i] = a[i]

Proof state:
i : Nat
a b : ByteArray
hlt : i < a.size
h : optParam (i < (a ++ b).size) ⋯
⊢ (a.data ++ b.data)[i] = a.data[i]

Tactic:
exact Array.getElem_append_left hlt

Result:
no goals

Proof state:
i : Nat
a b : ByteArray
hlt : i < a.size
h : optParam (i < (a ++ b).size) ⋯
⊢ (a ++ b)[i] = a[i]

Tactic:
simp [getElem_eq_data_getElem]

Result:
i : Nat
a b : ByteArray
hlt : i < a.size
h : optParam (i < (a ++ b).size) ⋯
⊢ (a.data ++ b.data)[i] = a.data[i]
-- Mathlib/Algebra/Module/Defs.lean
theorem Convex.combo_self {a b : R} (h : a + b = 1) (x : M) : a • x + b • x = x

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a b : R
h : a + b = 1
x : M
⊢ a • x + b • x = x

Tactic:
rw [← add_smul, h, one_smul]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_sphere_one_iff_norm : a ∈ sphere (1 : E) r ↔ ‖a‖ = r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ sphere 1 r ↔ ‖a‖ = r

Tactic:
simp [dist_eq_norm_div]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_eq_singleton_iff : Icc a b = {c} ↔ a = c ∧ b = c

Proof state:
case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case refine_2.intro
α : Type u_1
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}

Proof state:
case refine_2.intro
α : Type u_1
inst✝ : PartialOrder α
b : α
⊢ Icc b b = {b}

Tactic:
exact Icc_self _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c

Tactic:
have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)

Result:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c

Proof state:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
hab : a ≤ b
⊢ a = c ∧ b = c

Tactic:
exact
  ⟨eq_of_mem_singleton <| h ▸ left_mem_Icc.2 hab,
    eq_of_mem_singleton <| h ▸ right_mem_Icc.2 hab⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c

case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem id_eq_sum_orthogonalProjection_self_orthogonalComplement [HasOrthogonalProjection K] :
    ContinuousLinearMap.id 𝕜 E =
      K.subtypeL.comp (orthogonalProjection K) + Kᗮ.subtypeL.comp (orthogonalProjection Kᗮ)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ ContinuousLinearMap.id 𝕜 E = K.subtypeL.comp (orthogonalProjection K) + Kᗮ.subtypeL.comp (orthogonalProjection Kᗮ)

Tactic:
ext w

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
w : E
⊢ (ContinuousLinearMap.id 𝕜 E) w =
    (K.subtypeL.comp (orthogonalProjection K) + Kᗮ.subtypeL.comp (orthogonalProjection Kᗮ)) w

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
w : E
⊢ (ContinuousLinearMap.id 𝕜 E) w =
    (K.subtypeL.comp (orthogonalProjection K) + Kᗮ.subtypeL.comp (orthogonalProjection Kᗮ)) w

Tactic:
exact (orthogonalProjection_add_orthogonalProjection_orthogonal K w).symm

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_star : normSq (star a) = normSq a

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ normSq (star a) = normSq a

Tactic:
simp [normSq_def']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
/-- If `forget C` preserves and reflects initials, then `X` is initial if and only if
`ToType X` is empty. -/
lemma initial_iff_empty_of_preserves_of_reflects [PreservesColimit (Functor.empty.{0} C) (forget C)]
    [ReflectsColimit (Functor.empty.{0} C) (forget C)] (X : C) :
    Nonempty (IsInitial X) ↔ IsEmpty (ToType X)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial ((forget C).obj X)) ↔ Nonempty (IsInitial (ToType X))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial X) ↔ IsEmpty (ToType X)

Tactic:
rw [← Types.initial_iff_empty, (IsInitial.isInitialIffObj (forget C) X).nonempty_congr]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial ((forget C).obj X)) ↔ Nonempty (IsInitial (ToType X))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem head_range (n : Nat) (h) : (range n).head h = 0

Proof state:
case succ
n : Nat
h : range (n + 1) ≠ []
⊢ (range (n + 1)).head h = 0

Tactic:
simp [head?_range, head_eq_iff_head?_eq_some]

Result:
no goals

Proof state:
n : Nat
h : range n ≠ []
⊢ (range n).head h = 0

Tactic:
cases n with
| zero => simp at h
| succ n => simp [head?_range, head_eq_iff_head?_eq_some]

Result:
no goals

Proof state:
case zero
h : range 0 ≠ []
⊢ (range 0).head h = 0

Tactic:
simp at h

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem inv_Ioo_0_left {a : α} (ha : 0 < a) : (Ioo 0 a)⁻¹ = Ioi a⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : 0 < a
⊢ (Ioo 0 a)⁻¹ = Ioi a⁻¹

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : 0 < a
x : α
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : 0 < a
x : α
⊢ x ∈ (Ioo 0 a)⁻¹ ↔ x ∈ Ioi a⁻¹

Tactic:
exact ⟨fun h ↦ inv_lt_of_inv_lt₀ (inv_pos.1 h.1) h.2,
       fun h ↦ ⟨inv_pos.2 <| (inv_pos.2 ha).trans h, inv_lt_of_inv_lt₀ ha h⟩⟩

Result:
no goals
-- Mathlib/Topology/Instances/Sign.lean
theorem continuousAt_sign_of_ne_zero {a : α} (h : a ≠ 0) : ContinuousAt SignType.sign a

Proof state:
case inr
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
exact continuousAt_sign_of_pos h_pos

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
rcases h.lt_or_lt with (h_neg | h_pos)

Result:
case inl
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (⇑SignType.sign) a

case inr
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_pos : 0 < a
⊢ ContinuousAt (⇑SignType.sign) a

Proof state:
case inl
α : Type u_1
inst✝³ : Zero α
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
h : a ≠ 0
h_neg : a < 0
⊢ ContinuousAt (⇑SignType.sign) a

Tactic:
exact continuousAt_sign_of_neg h_neg

Result:
no goals