harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys

Proof state:
α : Type u_1
a b : α
xs ys : Array α
⊢ xs.push a = ys.push b ↔ a = b ∧ xs = ys

Tactic:
constructor

Result:
case mp
α : Type u_1
a b : α
xs ys : Array α
⊢ xs.push a = ys.push b → a = b ∧ xs = ys

case mpr
α : Type u_1
a b : α
xs ys : Array α
⊢ a = b ∧ xs = ys → xs.push a = ys.push b

Proof state:
case mp
α : Type u_1
a b : α
xs ys : Array α
h : xs.push a = ys.push b
⊢ a = b ∧ xs = ys

Tactic:
exact ⟨back_eq_of_push_eq h, pop_eq_of_push_eq h⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
a b : α
xs ys : Array α
⊢ xs.push a = ys.push b → a = b ∧ xs = ys

Tactic:
intro h

Result:
case mp
α : Type u_1
a b : α
xs ys : Array α
h : xs.push a = ys.push b
⊢ a = b ∧ xs = ys

Proof state:
case mpr
α : Type u_1
a b : α
xs ys : Array α
⊢ a = b ∧ xs = ys → xs.push a = ys.push b

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case mpr.intro
α : Type u_1
a : α
xs : Array α
⊢ xs.push a = xs.push a

Proof state:
case mpr.intro
α : Type u_1
a : α
xs : Array α
⊢ xs.push a = xs.push a

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_of_contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
    {v : β k} : (m.insertIfNew k v).contains a → (k == a) = false → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).contains a = true → (k == a) = false → m.contains a = true

Tactic:
simp_to_raw using Raw₀.contains_of_contains_insertIfNew

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
theorem rpow_neg_one_add_norm_sq_le {r : ℝ} (x : E) (hr : 0 < r) :
    ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2) ≤ (2 : ℝ) ^ (r / 2) * (1 + ‖x‖) ^ (-r) :=
  calc
    ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2)
      = (2 : ℝ) ^ (r / 2) * ((√2 * √((1 : ℝ) + ‖x‖ ^ 2)) ^ r)⁻¹

Proof state:
case h.hba.h₁
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)

Tactic:
apply one_add_norm_le_sqrt_two_mul_sqrt

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹ ≤ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹

Tactic:
gcongr

Result:
case h.hba.h₁
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 1 + ‖x‖ ≤ √2 * √(1 + ‖x‖ ^ 2)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ (1 + ‖x‖ ^ 2) ^ (-r / 2) = 2 ^ (r / 2) * ((√2 * √(1 + ‖x‖ ^ 2)) ^ r)⁻¹

Tactic:
rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg,
  mul_inv_cancel_left₀] <;> positivity

Result:
no goals

Proof state:
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)

Tactic:
rw [rpow_neg]

Result:
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem support_seq : (seq q p).support = ⋃ f ∈ q.support, f '' p.support :=
  Set.ext fun b => by simp [-mem_support_iff, seq, @eq_comm β b]

Proof state:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ b ∈ (q.seq p).support ↔ b ∈ ⋃ f ∈ q.support, f '' p.support

Tactic:
simp [-mem_support_iff, seq, @eq_comm β b]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem snd {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.snd α β) :=
  ((casesOn' zero
            ((casesOn' zero (Nat.Primrec.succ.comp right)).comp
              (pair right ((@Primcodable.prim β).comp left)))).comp
        (pair right ((@Primcodable.prim α).comp left))).of_eq
    fun n => by
    simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
    cases @decode α _ n.unpair.1 <;> simp
    cases @decode β _ n.unpair.2 <;> simp

Proof state:
case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => n + 1) (encode (decode (Nat.unpair n).2)) = encode (decode (Nat.unpair n).2)

Tactic:
cases @decode β _ n.unpair.2 <;> simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.unpaired
      (fun z n =>
        Nat.casesOn n 0 fun y =>
          Nat.unpaired (fun z n => Nat.casesOn n 0 fun y => (Nat.unpair (Nat.pair z y)).2.succ)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (encode (decode (Nat.unpair (Nat.pair z y)).1))))
      (Nat.pair (Nat.unpair n).2 (encode (decode (Nat.unpair n).1))) =
    encode (Option.map Prod.snd (decode n))

Tactic:
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => n.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.snd ((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih => Nat.rec 0 (fun n n_ih => n.succ) (encode (decode (Nat.unpair n).2)))
      (encode (decode (Nat.unpair n).1)) =
    encode
      (Option.map Prod.snd ((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2)))

Tactic:
cases @decode α _ n.unpair.1 <;> simp

Result:
case some
α : Type u_2
β : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n n_ih => n + 1) (encode (decode (Nat.unpair n).2)) = encode (decode (Nat.unpair n).2)
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma setLIntegral_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η]
    (a : α) {s : Set γ} (hs : MeasurableSet s) :
    ∫⁻ x in s, ENNReal.ofReal (rnDerivAux κ (κ + η) a x) ∂(κ + η) a = κ a s

Proof state:
case neg.h.e_6.h.h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
x : γ
⊢ x ∈ (fun a => (a, ())) ⁻¹' s ×ˢ univ ↔ x ∈ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a = (κ a) s

Tactic:
have h_le : κ ≤ κ + η := le_add_of_nonneg_right bot_le

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a = (κ a) s

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a = (κ a) s

Tactic:
simp_rw [rnDerivAux]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
⊢ ∫⁻ (x : γ) in s,
      ENNReal.ofReal
        (if hα : Countable α then ((∂κ a/∂(κ + η) a) x).toReal
        else (κ.map fun a => (a, ())).density (κ + η) a x univ) ∂(κ + η) a =
    (κ a) s

Proof state:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
⊢ ∫⁻ (x : γ) in s, ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal ∂(κ + η) a =
    ∫⁻ (x : γ) in s, (∂κ a/∂(κ + η) a) x ∂(κ + η) a

Tactic:
refine setLIntegral_congr_fun hs ?_

Result:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : Countable α
h_ac : κ a ≪ (κ + η) a
⊢ ∀ᵐ (x : γ) ∂(κ + η) a, x ∈ s → ENNReal.ofReal ((∂κ a/∂(κ + η) a) x).toReal = (∂κ a/∂(κ + η) a) x
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicatorAux_zero {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) {x : α}
    (x_out : x ∉ thickening δ E) : thickenedIndicatorAux δ E x = 0

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥

Tactic:
have key := tsub_le_tsub
  (@rfl _ (1 : ℝ≥0∞)).le (ENNReal.div_le_div x_out (@rfl _ (ENNReal.ofReal δ : ℝ≥0∞)).le)

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ thickenedIndicatorAux δ E x = 0

Tactic:
unfold thickenedIndicatorAux

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ = 0

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥

Tactic:
simpa [tsub_self] using key

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥

Tactic:
rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ = 0

Tactic:
apply le_antisymm _ bot_le

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ thickenedIndicatorAux δ E x = 0

Tactic:
rw [thickening, mem_setOf_eq, not_lt] at x_out

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ thickenedIndicatorAux δ E x = 0
-- Mathlib/Data/Bool/Count.lean
theorem count_not_add_count (l : List Bool) (b : Bool) : count (!b) l + count b l = length l

Proof state:
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true

Tactic:
ext x

Result:
case h
l : List Bool
b x : Bool
⊢ (x == b) = decide ¬(x == !b) = true

Proof state:
l : List Bool
b : Bool
this : (fun x => x == b) = fun a => decide ¬(a == !b) = true
⊢ countP (fun x => x == b) l = countP (fun a => decide ¬(a == !b) = true) l

Tactic:
rw [this]

Result:
no goals

Proof state:
case h
l : List Bool
b x : Bool
⊢ (x == b) = decide ¬(x == !b) = true

Tactic:
cases x <;> cases b <;> rfl

Result:
no goals

Proof state:
l : List Bool
b : Bool
⊢ countP (fun x => x == b) l = countP (fun a => decide ¬(a == !b) = true) l

Tactic:
suffices (fun x => x == b) = (fun a => decide ¬(a == !b) = true) by rw [this]

Result:
l : List Bool
b : Bool
⊢ (fun x => x == b) = fun a => decide ¬(a == !b) = true
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem xInTermsOfW_eq [Invertible (p : R)] {n : ℕ} : xInTermsOfW p R n =
    (X n - ∑ i ∈ range n, C ((p : R) ^ i) *
      xInTermsOfW p R i ^ p ^ (n - i)) * C ((⅟p : R) ^ n)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n = (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n)

Tactic:
rw [xInTermsOfW, ← Fin.sum_univ_eq_sum_range]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
lemma addOppositeEquiv_symm_leadingCoeff (x : (HahnSeries Γ R)ᵃᵒᵖ) :
    (addOppositeEquiv.symm x).leadingCoeff = .op x.unop.leadingCoeff

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : (HahnSeries Γ R)ᵃᵒᵖ
⊢ (addOppositeEquiv.symm x).leadingCoeff = AddOpposite.op (AddOpposite.unop x).leadingCoeff

Tactic:
apply AddOpposite.unop_injective

Result:
case a
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : (HahnSeries Γ R)ᵃᵒᵖ
⊢ AddOpposite.unop (addOppositeEquiv.symm x).leadingCoeff =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)

Proof state:
case a
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : (HahnSeries Γ R)ᵃᵒᵖ
⊢ AddOpposite.unop (addOppositeEquiv.symm x).leadingCoeff =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)

Tactic:
rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_div_iff_of_neg' (hc : c < 0) : a ≤ b / c ↔ b ≤ c * a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ c * a

Tactic:
rw [mul_comm, le_div_iff_of_neg hc]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_Ioc (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
    Ioc a b ∪ Ioc c d = Ioc (min a c) (max b d)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ⊓ b ≤ c ⊔ d
h₂ : c ⊓ d ≤ a ⊔ b
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

Tactic:
rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;> simp [*] at h₁ h₂

Result:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

Tactic:
simp [*]

Result:
no goals

Proof state:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

Tactic:
exact Ioc_union_Ioc' h₂ h₁

Result:
no goals

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ioc a b ∪ Ioc c d = Ioc (a ⊓ c) (b ⊔ d)

Tactic:
all_goals simp [*]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_eval (p : R[X]) (x : R) :
    p.derivative.eval x = p.sum fun n a => a * n * x ^ (n - 1)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (derivative p) = p.sum fun n a => a * ↑n * x ^ (n - 1)

Tactic:
simp_rw [derivative_apply, eval_sum, eval_mul_X_pow, eval_C]

Result:
no goals
-- Mathlib/Topology/Order/IsLUB.lean
theorem exists_seq_strictMono_tendsto' {α : Type*} [LinearOrder α] [TopologicalSpace α]
    [DenselyOrdered α] [OrderTopology α] [FirstCountableTopology α] {x y : α} (hy : y < x) :
    ∃ u : ℕ → α, StrictMono u ∧ (∀ n, u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Proof state:
α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim

Result:
α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Proof state:
α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
rcases (isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_not_mem hx ht with ⟨u, hu⟩

Result:
case intro
α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Proof state:
α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy

Result:
α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Proof state:
case intro
α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
exact ⟨u, hu.1, hu.2.2.symm⟩

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
lemma measurable_uniqueElim_cylinderEvents [Unique ι] :
    Measurable (uniqueElim : π (default : ι) → ∀ i, π i)

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
inst✝ : Unique ι
⊢ Measurable fun x => x

Tactic:
exact measurable_id

Result:
no goals

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
inst✝ : Unique ι
⊢ Measurable uniqueElim

Tactic:
simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]

Result:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
inst✝ : Unique ι
⊢ Measurable fun x => x
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_succ_apply' (n : ℕ) (x : α) : f^[n.succ] x = f (f^[n] x)

Proof state:
α : Type u
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f (f^[n] x)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
f : α → α
n : ℕ
x : α
⊢ f^[n.succ] x = f (f^[n] x)

Tactic:
rw [iterate_succ']

Result:
α : Type u
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f (f^[n] x)
-- Mathlib/Data/Int/WithZero.lean
theorem toNNReal_strictMono {e : ℝ≥0} (he : 1 < e) :
    StrictMono (toNNReal (ne_zero_of_lt he))

Proof state:
case pos
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : ¬x = 0
hy : y = 0
⊢ e ^ toAdd (unzero hx) < 0

Tactic:
simp only [hy, not_lt_zero'] at hxy

Result:
no goals

Proof state:
case neg
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : ¬x = 0
hy : ¬y = 0
⊢ e ^ toAdd (unzero hx) < e ^ toAdd (unzero hy)

Tactic:
rw [zpow_lt_zpow_iff_right₀ he, Multiplicative.toAdd_lt, ← coe_lt_coe, coe_unzero hx,
  WithZero.coe_unzero hy]

Result:
case neg
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : ¬x = 0
hy : ¬y = 0
⊢ x < y

Proof state:
case neg
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : ¬x = 0
hy : ¬y = 0
⊢ x < y

Tactic:
exact hxy

Result:
no goals

Proof state:
case neg
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : x = 0
hy : ¬y = 0
⊢ 0 < e ^ toAdd (unzero hy)

Tactic:
exact zpow_pos he.bot_lt _

Result:
no goals

Proof state:
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
⊢ (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) < if hx : y = 0 then 0 else e ^ toAdd (unzero hx)

Tactic:
split_ifs with hx hy hy

Result:
case pos
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : x = 0
hy : y = 0
⊢ 0 < 0

case neg
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : x = 0
hy : ¬y = 0
⊢ 0 < e ^ toAdd (unzero hy)

case pos
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : ¬x = 0
hy : y = 0
⊢ e ^ toAdd (unzero hx) < 0

case neg
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : ¬x = 0
hy : ¬y = 0
⊢ e ^ toAdd (unzero hx) < e ^ toAdd (unzero hy)

Proof state:
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
⊢ (toNNReal ⋯) x < (toNNReal ⋯) y

Tactic:
simp only [toNNReal, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
⊢ (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) < if hx : y = 0 then 0 else e ^ toAdd (unzero hx)

Proof state:
case pos
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
hx : x = 0
hy : y = 0
⊢ 0 < 0

Tactic:
simp only [hy, not_lt_zero'] at hxy

Result:
no goals

Proof state:
e : ℝ≥0
he : 1 < e
⊢ StrictMono ⇑(toNNReal ⋯)

Tactic:
intro x y hxy

Result:
e : ℝ≥0
he : 1 < e
x y : ℤₘ₀
hxy : x < y
⊢ (toNNReal ⋯) x < (toNNReal ⋯) y