harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem Gamma_mul_Gamma_add_half (s : ℝ) :
    Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * (2 : ℝ) ^ (1 - 2 * s) * √π

Proof state:
s : ℝ
⊢ ↑(Gamma s * Gamma (s + 1 / 2)) = ↑(Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π)

Tactic:
simpa only [← Gamma_ofReal, ofReal_cpow zero_le_two, ofReal_mul, ofReal_add, ofReal_div,
  ofReal_sub] using Complex.Gamma_mul_Gamma_add_half ↑s

Result:
no goals

Proof state:
s : ℝ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π

Tactic:
rw [← ofReal_inj]

Result:
s : ℝ
⊢ ↑(Gamma s * Gamma (s + 1 / 2)) = ↑(Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π)
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem exists_subordinate_pairwise_disjoint [Countable ι] {s : ι → Set α}
    (h : ∀ i, NullMeasurableSet (s i) μ) (hd : Pairwise (AEDisjoint μ on s)) :
    ∃ t : ι → Set α,
      (∀ i, t i ⊆ s i) ∧
        (∀ i, s i =ᵐ[μ] t i) ∧ (∀ i, MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Proof state:
case intro.intro.intro
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
u : ι → Set α
hum : ∀ (i : ι), MeasurableSet (u i)
hu₀ : ∀ (i : ι), μ (u i) = 0
hud : Pairwise (Disjoint on fun i => s i \ u i)
⊢ ∃ t,
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
exact
  ⟨fun i => t i \ u i, fun i => diff_subset.trans (ht_sub _), fun i =>
    (ht_eq _).symm.trans (diff_null_ae_eq_self (hu₀ i)).symm, fun i => (htm i).diff (hum i),
    hud.mono fun i j h =>
      h.mono (diff_subset_diff_left (ht_sub i)) (diff_subset_diff_left (ht_sub j))⟩

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
⊢ ∃ t,
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
rcases exists_null_pairwise_disjoint_diff hd with ⟨u, hum, hu₀, hud⟩

Result:
case intro.intro.intro
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
u : ι → Set α
hum : ∀ (i : ι), MeasurableSet (u i)
hu₀ : ∀ (i : ι), μ (u i) = 0
hud : Pairwise (Disjoint on fun i => s i \ u i)
⊢ ∃ t,
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Proof state:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ t,
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
choose t ht_sub htm ht_eq using fun i => exists_measurable_subset_ae_eq (h i)

Result:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : ι → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
⊢ ∃ t,
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
-- Mathlib/Order/Filter/Pointwise.lean
theorem isUnit_iff : IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a

Proof state:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a

Tactic:
rintro ⟨u, rfl⟩

Result:
case mp.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ∃ a, ↑u = pure a ∧ IsUnit a

Tactic:
refine ⟨a, ha, ⟨a, b, h, pure_injective ?_⟩, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure (b * a) = pure 1

Proof state:
case mpr.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (pure a)

Tactic:
exact ha.filter

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f

Tactic:
rintro ⟨a, rfl, ha⟩

Result:
case mpr.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
a : α
ha : IsUnit a
⊢ IsUnit (pure a)

Proof state:
case mp.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
⊢ ∃ a, ↑u = pure a ∧ IsUnit a

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := Filter.mul_eq_one_iff.1 u.mul_inv

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ∃ a, ↑u = pure a ∧ IsUnit a

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1

Tactic:
exact u.inv_mul

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure (b * a) = pure 1

Tactic:
rw [← pure_mul_pure, ← ha, ← hb]

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ ↑u⁻¹ * ↑u = pure 1

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a ∧ IsUnit a

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ IsUnit f → ∃ a, f = pure a ∧ IsUnit a

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
f : Filter α
⊢ (∃ a, f = pure a ∧ IsUnit a) → IsUnit f
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem iterate_derivative_at_0_ne_zero [CharZero R] (n ν : ℕ) (h : ν ≤ n) :
    (Polynomial.derivative^[ν] (bernsteinPolynomial R n ν)).eval 0 ≠ 0

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Tactic:
obtain rfl | h' := Nat.eq_zero_or_pos ν

Result:
case h.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n : ℕ
h : 0 ≤ n
⊢ 0 < eval (n - (0 - 1)) (ascPochhammer ℕ 0)

case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬↑(eval (n - (ν - 1)) (ascPochhammer ℕ ν)) = 0

Tactic:
norm_cast

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (n - (ν - 1)) (ascPochhammer ℕ ν) = 0

Proof state:
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν.pred.succ ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Tactic:
exact ascPochhammer_pos _ _ (tsub_pos_of_lt (Nat.lt_of_succ_le h))

Result:
no goals

Proof state:
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Tactic:
rw [← Nat.succ_pred_eq_of_pos h'] at h

Result:
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν.pred.succ ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Proof state:
case h.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n : ℕ
h : 0 ≤ n
⊢ 0 < eval (n - (0 - 1)) (ascPochhammer ℕ 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (n - (ν - 1)) (ascPochhammer ℕ ν) = 0

Tactic:
apply ne_of_gt

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ 0 < eval (n - (ν - 1)) (ascPochhammer ℕ ν)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((⇑derivative)^[ν] (bernsteinPolynomial R n ν)) ≠ 0

Tactic:
simp only [Int.natCast_eq_zero, bernsteinPolynomial.iterate_derivative_at_0, Ne, Nat.cast_eq_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑(n - (ν - 1))) (ascPochhammer R ν) = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑(n - (ν - 1))) (ascPochhammer R ν) = 0

Tactic:
simp only [← ascPochhammer_eval_cast]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬↑(eval (n - (ν - 1)) (ascPochhammer ℕ ν)) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_sub_one (h : m.1.WF) {k : α} {f : Option β → Option β}
    (h₁ : m.contains k) (h₂ : (f (Const.get? m k)).isNone) :
    (Const.alter m k f).1.size = m.1.size - 1

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
h₁ : m.contains k = true
h₂ : (f (get? m k)).isNone = true
⊢ (alter m k f).val.size = m.val.size - 1

Tactic:
simp [size_alter, h, h₁, h₂]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma toCycles_eq_zero [K.HasHomology j] (hij : ¬ c.Rel i j) :
    K.toCycles i j = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology j
hij : ¬c.Rel i j
⊢ K.toCycles i j = 0

Tactic:
rw [← cancel_mono (K.iCycles j), toCycles_i, zero_comp, K.shape _ _ hij]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
theorem tendsto_nearestPt {e : ℕ → α} {x : α} (hx : x ∈ closure (range e)) :
    Tendsto (fun N => nearestPt e N x) atTop (𝓝 x)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, (nearestPt e x_1) x ∈ ball x ε

Tactic:
exact ⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
⊢ Tendsto (fun N => (nearestPt e N) x) atTop (𝓝 x)

Tactic:
refine (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => ?_

Result:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, (nearestPt e x_1) x ∈ ball x ε

Proof state:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, (nearestPt e x_1) x ∈ ball x ε

Tactic:
rw [edist_comm] at hN

Result:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, (nearestPt e x_1) x ∈ ball x ε

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, (nearestPt e x_1) x ∈ ball x ε

Tactic:
rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure (Set.range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Set.Ici ia, (nearestPt e x_1) x ∈ ball x ε
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sSup_eq_bsup {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) :
    sSup (brange o f) = bsup.{_, v} o f

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ sSup (o.brange f) = o.bsup f

Tactic:
congr

Result:
case e_a
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.brange f = range (o.familyOfBFamily f)

Proof state:
case e_a
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ o.brange f = range (o.familyOfBFamily f)

Tactic:
rw [range_familyOfBFamily]

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem Function.Surjective.connectedSpace [ConnectedSpace α] [TopologicalSpace β]
    {f : α → β} (hf : Surjective f) (hf' : Continuous f) : ConnectedSpace β

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous f
⊢ ConnectedSpace β

Tactic:
rw [connectedSpace_iff_univ, ← hf.range_eq]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous f
⊢ IsConnected (range f)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Surjective f
hf' : Continuous f
⊢ IsConnected (range f)

Tactic:
exact isConnected_range hf'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_toArray (p : α → Bool) (v : Vector α n) :
    v.toArray.all p = v.all p

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.all p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.all p

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Bool
v : Vector α n
⊢ v.all p = v.all p

Tactic:
cases v

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.all p =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.all p
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_union_Ioi (h : c < max a b) : Ioo a b ∪ Ioi c = Ioi (min a c)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
rw [min_comm]

Result:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (c ⊓ a)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (c ⊓ a)

Tactic:
simp [*, min_eq_left_of_lt]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c < a ⊔ b
⊢ Ioo a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
rcases le_total a b with hab | hab <;> simp [hab] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (a ⊓ c)

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c < a
⊢ Ioo a b ∪ Ioi c = Ioi (a ⊓ c)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c < b
⊢ Ioo a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
exact Ioo_union_Ioi' h

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_neg : sin (-x) = -sin x

Proof state:
x : ℝ
⊢ sin (-x) = -sin x

Tactic:
simp [sin, exp_neg, (neg_div _ _).symm, add_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_fin_cons {n} {v : Fin n → V} :
    LinearIndependent K (Fin.cons x v : Fin (n + 1) → V) ↔
      LinearIndependent K v ∧ x ∉ Submodule.span K (range v)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some) ∧
      (Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) none ∉ span K (range ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some)) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]

Result:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some) ∧
      (Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) none ∉ span K (range ((Fin.cons x v ∘ ⇑(finSuccEquiv n).symm) ∘ some)) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertManyIfNewUnit_empty_list_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l) {h'} :
    getKey (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k' h' = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
h' : (insertManyIfNewUnit empty l).val.contains k' = true
⊢ (insertManyIfNewUnit empty l).val.getKey k' h' = k

Tactic:
exact getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem _ Raw.WF.empty₀ k_beq
  contains_empty distinct mem

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2

Proof state:
x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)

Tactic:
exact sqrt_le_left

Result:
no goals

Proof state:
x y : ℝ
⊢ √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2

Tactic:
rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]

Result:
x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ y ^ 2)
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_mul_mul_invMul (A B C : Finset G) :
    #(A * C) * #B ≤ #(A * B) * #(C⁻¹ * B)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A * B) * #(C⁻¹ * B)

Tactic:
simpa using ruzsa_triangle_inequality_mulInv_mul_mul A B C⁻¹

Result:
no goals
-- Mathlib/Probability/StrongLaw.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.truncation (hf : AEStronglyMeasurable f μ)
    {A : ℝ} : AEStronglyMeasurable (truncation f A) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable ((Set.Ioc (-A) A).indicator id) (Measure.map f μ)

Tactic:
exact (stronglyMeasurable_id.indicator measurableSet_Ioc).aestronglyMeasurable

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable (ProbabilityTheory.truncation f A) μ

Tactic:
apply AEStronglyMeasurable.comp_aemeasurable _ hf.aemeasurable

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable ((Set.Ioc (-A) A).indicator id) (Measure.map f μ)
-- Mathlib/Data/Real/ConjExponents.lean
@[simp, norm_cast] lemma isConjExponent_coe {p q : ℝ≥0} :
    IsConjExponent p q ↔ p.IsConjExponent q

Proof state:
case refine_2
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
rw [← coe_inv, ← coe_inv] at h

Result:
case refine_2
p q : ℝ≥0
h : ↑p⁻¹ + ↑q⁻¹ = 1
⊢ p⁻¹ + q⁻¹ = 1

case refine_2
p q : ℝ≥0
h : ↑p⁻¹ + (↑q)⁻¹ = 1
⊢ q ≠ 0

case refine_2
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ p ≠ 0

Proof state:
p q : ℝ≥0
⊢ (↑p).IsConjExponent ↑q ↔ p.IsConjExponent q

Tactic:
simp only [isConjExponent_iff, NNReal.isConjExponent_iff]

Result:
p q : ℝ≥0
⊢ (↑p)⁻¹ + (↑q)⁻¹ = 1 ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Proof state:
case refine_3.intro
p : ℝ≥0
hp : 1 < p
h : p⁻¹ + 0⁻¹ = 1
⊢ False

Tactic:
simp [hp.ne'] at h

Result:
no goals

Proof state:
case refine_2
q : ℝ≥0
h : (↑0)⁻¹ + (↑q)⁻¹ = 1
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case refine_3.intro
p q : ℝ≥0
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
⊢ (↑p)⁻¹ + (↑q)⁻¹ = 1

Tactic:
rw [← coe_inv (zero_lt_one.trans hp).ne', ← coe_inv, ← coe_add, h, coe_one]

Result:
case refine_3.intro
p q : ℝ≥0
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
⊢ q ≠ 0

Proof state:
case refine_2
p q : ℝ≥0
h : ↑p⁻¹ + (↑q)⁻¹ = 1
⊢ q ≠ 0

case refine_2
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ p ≠ 0

Tactic:
all_goals rintro rfl; simp at h

Result:
no goals

Proof state:
case refine_3.intro
p q : ℝ≥0
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
⊢ q ≠ 0

Tactic:
rintro rfl

Result:
case refine_3.intro
p : ℝ≥0
hp : 1 < p
h : p⁻¹ + 0⁻¹ = 1
⊢ False

Proof state:
case refine_3
p q : ℝ≥0
⊢ 1 < p ∧ p⁻¹ + q⁻¹ = 1 → (↑p)⁻¹ + (↑q)⁻¹ = 1

Tactic:
rintro ⟨hp, h⟩

Result:
case refine_3.intro
p q : ℝ≥0
hp : 1 < p
h : p⁻¹ + q⁻¹ = 1
⊢ (↑p)⁻¹ + (↑q)⁻¹ = 1

Proof state:
p q : ℝ≥0
⊢ (↑p)⁻¹ + (↑q)⁻¹ = 1 ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩

Result:
case refine_1
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ 1 < p

case refine_2
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ p⁻¹ + q⁻¹ = 1

case refine_3
p q : ℝ≥0
⊢ 1 < p ∧ p⁻¹ + q⁻¹ = 1 → (↑p)⁻¹ + (↑q)⁻¹ = 1

Proof state:
case refine_2
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
case refine_2
q : ℝ≥0
h : (↑0)⁻¹ + (↑q)⁻¹ = 1
⊢ False

Proof state:
case refine_1
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ 1 < p

Tactic:
simpa using (ENNReal.lt_add_right (fun hp ↦ by simp [hp] at h) <| by simp).trans_eq h

Result:
no goals

Proof state:
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
hp : (↑p)⁻¹ = ⊤
⊢ False

Tactic:
simp [hp] at h

Result:
no goals

Proof state:
case refine_2
p q : ℝ≥0
h : ↑p⁻¹ + ↑q⁻¹ = 1
⊢ p⁻¹ + q⁻¹ = 1

Tactic:
norm_cast at h

Result:
no goals

Proof state:
p q : ℝ≥0
h : (↑p)⁻¹ + (↑q)⁻¹ = 1
⊢ (↑q)⁻¹ ≠ 0

Tactic:
simp

Result:
no goals