harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiable_apply (i : ι) :
    Differentiable (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
x : (i : ι) → F' i
⊢ DifferentiableAt 𝕜 (fun f => f i) x

Tactic:
apply differentiableAt_apply

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
⊢ Differentiable 𝕜 fun f => f i

Tactic:
intro x

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
x : (i : ι) → F' i
⊢ DifferentiableAt 𝕜 (fun f => f i) x
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
lemma antilipschitzWith_mul_left {a : α} (ha : a ≠ 0) : AntilipschitzWith (‖a‖₊⁻¹) (a * ·) :=
  AntilipschitzWith.of_le_mul_dist fun _ _ ↦ by simp [dist_eq_norm, ← _root_.mul_sub, ha]

Proof state:
α : Type u_1
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ ≤ ↑‖a‖₊⁻¹ * dist (a * x✝¹) (a * x✝)

Tactic:
simp [dist_eq_norm, ← _root_.mul_sub, ha]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- The gaussian pdf is positive when the variance is not zero. -/
lemma gaussianPDFReal_pos (μ : ℝ) (v : ℝ≥0) (x : ℝ) (hv : v ≠ 0) : 0 < gaussianPDFReal μ v x

Proof state:
μ : ℝ
v : ℝ≥0
x : ℝ
hv : v ≠ 0
⊢ 0 < gaussianPDFReal μ v x

Tactic:
rw [gaussianPDFReal]

Result:
μ : ℝ
v : ℝ≥0
x : ℝ
hv : v ≠ 0
⊢ 0 < (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))

Proof state:
μ : ℝ
v : ℝ≥0
x : ℝ
hv : v ≠ 0
⊢ 0 < (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))

Tactic:
positivity

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Ioi : x ∈ Ioi a ↔ a < x

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x

Tactic:
rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
    (cons a x) &&& (cons b y) = cons (a && b) (x &&& y)

Proof state:
case pred
w : Nat
x y : BitVec w
a b : Bool
i : Nat
a✝ : i < w + 1
⊢ (cons a x &&& cons b y).getLsbD i = (cons (a && b) (x &&& y)).getLsbD i

Tactic:
simp [cons]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
a b : Bool
⊢ cons a x &&& cons b y = cons (a && b) (x &&& y)

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
a b : Bool
i : Nat
a✝ : i < w + 1
⊢ (cons a x &&& cons b y).getLsbD i = (cons (a && b) (x &&& y)).getLsbD i
-- Mathlib/Analysis/NormedSpace/RieszLemma.lean
theorem Metric.closedBall_infDist_compl_subset_closure {x : F} {s : Set F} (hx : x ∈ s) :
    closedBall x (infDist x sᶜ) ⊆ closure s

Proof state:
case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure s

Tactic:
rw [h₀, closedBall_zero']

Result:
case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closure {x} ⊆ closure s

Proof state:
case inr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closure (ball x (infDist x sᶜ)) ⊆ closure s

Tactic:
exact closure_mono ball_infDist_compl_subset

Result:
no goals

Proof state:
case inr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure s

Tactic:
rw [← closure_ball x h₀]

Result:
case inr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closure (ball x (infDist x sᶜ)) ⊆ closure s

Proof state:
case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closure {x} ⊆ closure s

Tactic:
exact closure_mono (singleton_subset_iff.2 hx)

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x sᶜ) ⊆ closure s

Tactic:
rcases eq_or_ne (infDist x sᶜ) 0 with h₀ | h₀

Result:
case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure s

case inr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure s
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_pos_left_iff_sameRay (hx : x ≠ 0) (hy : y ≠ 0) :
    (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y

Proof state:
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)

Tactic:
exact SameRay.sameRay_pos_smul_right x hr

Result:
no goals

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ r, 0 < r ∧ r • x = y
⊢ SameRay R x y

Tactic:
rcases h with ⟨r, hr, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
hy : r • x ≠ 0
⊢ SameRay R x (r • x)

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y

Tactic:
refine ⟨fun h => ?_, fun h => h.exists_pos_left hx hy⟩

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
h : ∃ r, 0 < r ∧ r • x = y
⊢ SameRay R x y
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem sphere_union_ball : sphere x ε ∪ ball x ε = closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ sphere x ε ∪ ball x ε = closedBall x ε

Tactic:
rw [union_comm, ball_union_sphere]

Result:
no goals
-- Mathlib/Algebra/Ring/Identities.lean
theorem sum_four_sq_mul_sum_four_sq :
    (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
      (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
          (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
        (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2

Proof state:
R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ y₁ y₂ y₃ y₄ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2) * (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄) ^ 2 + (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃) ^ 2 +
        (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂) ^ 2 +
      (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
/-- The derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `deriv` in that case is 0. -/
@[simp]
lemma deriv_klFun : deriv klFun = log

Proof state:
case pos
x : ℝ
h0 : x = 0
⊢ deriv klFun x = log x

Tactic:
simp only [h0, log_zero]

Result:
case pos
x : ℝ
h0 : x = 0
⊢ deriv klFun 0 = 0

Proof state:
case pos
x : ℝ
h0 : x = 0
⊢ deriv klFun 0 = 0

Tactic:
exact deriv_zero_of_not_differentiableAt not_differentiableAt_klFun_zero

Result:
no goals

Proof state:
case neg
x : ℝ
h0 : ¬x = 0
⊢ deriv klFun x = log x

Tactic:
exact (hasDerivAt_klFun h0).deriv

Result:
no goals

Proof state:
case h
x : ℝ
⊢ deriv klFun x = log x

Tactic:
by_cases h0 : x = 0

Result:
case pos
x : ℝ
h0 : x = 0
⊢ deriv klFun x = log x

case neg
x : ℝ
h0 : ¬x = 0
⊢ deriv klFun x = log x

Proof state:
⊢ deriv klFun = log

Tactic:
ext x

Result:
case h
x : ℝ
⊢ deriv klFun x = log x
-- Mathlib/Data/List/TakeDrop.lean
theorem span.loop_eq_take_drop :
    ∀ l₁ l₂ : List α, span.loop p l₁ l₂ = (l₂.reverse ++ takeWhile p l₁, dropWhile p l₁)
  | [], l₂ => by simp [span.loop, takeWhile, dropWhile]
  | (a :: l), l₂ => by
    cases hp : p a <;> simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

Proof state:
α : Type u
p : α → Bool
a : α
l l₂ : List α
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
cases hp : p a <;> simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

Result:
no goals

Proof state:
α : Type u
p : α → Bool
l₂ : List α
⊢ loop p [] l₂ = (l₂.reverse ++ takeWhile p [], dropWhile p [])

Tactic:
simp [span.loop, takeWhile, dropWhile]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n

Proof state:
case lt
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
⊢ 2 ^ n ≤ 2 ^ i

Tactic:
exact pow_le_pow_of_le_right Nat.zero_lt_two i_ge_n

Result:
no goals

Proof state:
x y n : Nat
right : y < 2 ^ n
⊢ x &&& y < 2 ^ n

Tactic:
apply lt_pow_two_of_testBit

Result:
case p
x y n : Nat
right : y < 2 ^ n
⊢ ∀ (i : Nat), i ≥ n → (x &&& y).testBit i = false

Proof state:
case p
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
yf : y.testBit i = false
⊢ (x &&& y).testBit i = false

Tactic:
simp [testBit_and, yf]

Result:
no goals

Proof state:
case p
x y n : Nat
right : y < 2 ^ n
⊢ ∀ (i : Nat), i ≥ n → (x &&& y).testBit i = false

Tactic:
intro i i_ge_n

Result:
case p
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
⊢ (x &&& y).testBit i = false

Proof state:
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
⊢ y.testBit i = false

Tactic:
apply Nat.testBit_lt_two_pow

Result:
case lt
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
⊢ y < 2 ^ i

Proof state:
case lt
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
⊢ y < 2 ^ i

Tactic:
apply Nat.lt_of_lt_of_le right

Result:
case lt
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
⊢ 2 ^ n ≤ 2 ^ i

Proof state:
case p
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
⊢ (x &&& y).testBit i = false

Tactic:
have yf : testBit y i = false := by
        apply Nat.testBit_lt_two_pow
        apply Nat.lt_of_lt_of_le right
        exact pow_le_pow_of_le_right Nat.zero_lt_two i_ge_n

Result:
case p
x y n : Nat
right : y < 2 ^ n
i : Nat
i_ge_n : i ≥ n
yf : y.testBit i = false
⊢ (x &&& y).testBit i = false
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.listProd {L : List ι} {f g : ι → α → β} (h : ∀ i ∈ L, f i ~[l] g i) :
    (fun x ↦ (L.map (f · x)).prod) ~[l] (fun x ↦ (L.map (g · x)).prod)

Proof state:
case cons
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i ~[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) ~[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
h : f i ~[l] g i ∧ ∀ x ∈ L, f x ~[l] g x
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) ~[l] fun x => g i x * (List.map (fun x_1 => g x_1 x) L).prod

Tactic:
exact h.1.mul (ihL h.2)

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
L : List ι
f g : ι → α → β
h : ∀ i ∈ L, f i ~[l] g i
⊢ (fun x => (List.map (fun x_1 => f x_1 x) L).prod) ~[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod

Tactic:
induction L with
| nil => simp [IsEquivalent.refl]
| cons i L ihL =>
  simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢
  exact h.1.mul (ihL h.2)

Result:
no goals

Proof state:
case nil
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
f g : ι → α → β
h : ∀ i ∈ [], f i ~[l] g i
⊢ (fun x => (List.map (fun x_1 => f x_1 x) []).prod) ~[l] fun x => (List.map (fun x_1 => g x_1 x) []).prod

Tactic:
simp [IsEquivalent.refl]

Result:
no goals

Proof state:
case cons
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i ~[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) ~[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
h : ∀ i_1 ∈ i :: L, f i_1 ~[l] g i_1
⊢ (fun x => (List.map (fun x_1 => f x_1 x) (i :: L)).prod) ~[l] fun x => (List.map (fun x_1 => g x_1 x) (i :: L)).prod

Tactic:
simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢

Result:
case cons
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i ~[l] g i) →
    (fun x => (List.map (fun x_1 => f x_1 x) L).prod) ~[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
h : f i ~[l] g i ∧ ∀ x ∈ L, f x ~[l] g x
⊢ (fun x => f i x * (List.map (fun x_1 => f x_1 x) L).prod) ~[l] fun x => g i x * (List.map (fun x_1 => g x_1 x) L).prod
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {fallback v : β} : getValueD a (insertEntryIfNew k v l) fallback =
      if k == a ∧ containsKey k l = false then v else getValueD a l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
fallback v : β
⊢ getValueD a (insertEntryIfNew k v l) fallback =
    if (k == a) = true ∧ containsKey k l = false then v else getValueD a l fallback

Tactic:
simp [getValueD_eq_getValue?, getValue?_insertEntryIfNew,
  apply_ite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem inseparable_pi {f g : ∀ i, π i} : (f ~ᵢ g) ↔ ∀ i, f i ~ᵢ g i

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
f g : (i : ι) → π i
⊢ (f ~ᵢ g) ↔ ∀ (i : ι), f i ~ᵢ g i

Tactic:
simp only [Inseparable, nhds_pi, funext_iff, pi_inj]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem interior_setOf_re_le (a : ℝ) : interior { z : ℂ | z.re ≤ a } = { z | z.re < a }

Proof state:
a : ℝ
⊢ interior {z | z.re ≤ a} = {z | z.re < a}

Tactic:
simpa only [interior_Iic] using interior_preimage_re (Iic a)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem DelProp.redred (h : DelProp c t n) : ∃ n', RedRed (c = black) t n'

Proof state:
c : RBColor
α✝ : Type u_1
t : RBNode α✝
n : Nat
h : DelProp c t n
⊢ ∃ n', RedRed (c = black) t n'

Tactic:
unfold DelProp at h

Result:
c : RBColor
α✝ : Type u_1
t : RBNode α✝
n : Nat
h :
  match c with
  | black => ∃ n', n = n' + 1 ∧ RedRed True t n'
  | red => ∃ c, t.Balanced c n
⊢ ∃ n', RedRed (c = black) t n'

Proof state:
c : RBColor
α✝ : Type u_1
t : RBNode α✝
n : Nat
h :
  match c with
  | black => ∃ n', n = n' + 1 ∧ RedRed True t n'
  | red => ∃ c, t.Balanced c n
⊢ ∃ n', RedRed (c = black) t n'

Tactic:
exact match c, h with
| red, ⟨_, h⟩ => ⟨_, .balanced h⟩
| black, ⟨_, _, h⟩ => ⟨_, h.imp fun _ => rfl⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_sub {A : M} (ha : IsUnit A.det) (z1 z2 : ℤ) : A ^ (z1 - z2) = A ^ z1 / A ^ z2

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
z1 z2 : ℤ
⊢ A ^ (z1 - z2) = A ^ z1 / A ^ z2

Tactic:
rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem eq_aleph_of_eq_card_ord {o : Ordinal} (ho : o.card.ord = o) (ho' : ω ≤ o) :
    ∃ a, (ℵ_ a).ord = o

Proof state:
case h
o : Ordinal.{u_1}
ho : o.card.ord = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : (aleph' a).ord = o
⊢ ω ≤ a

Tactic:
rwa [← aleph0_le_aleph', ← ord_le_ord, ha, ord_aleph0]

Result:
no goals

Proof state:
o : Ordinal.{u_1}
ho : o.card.ord = o
ho' : ω ≤ o
⊢ ∃ a, (ℵ_ a).ord = o

Tactic:
obtain ⟨a, ha⟩ := eq_aleph'_of_eq_card_ord ho

Result:
case intro
o : Ordinal.{u_1}
ho : o.card.ord = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : (aleph' a).ord = o
⊢ ∃ a, (ℵ_ a).ord = o

Proof state:
case intro
o : Ordinal.{u_1}
ho : o.card.ord = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : (aleph' a).ord = o
⊢ ∃ a, (ℵ_ a).ord = o

Tactic:
use a - ω

Result:
case h
o : Ordinal.{u_1}
ho : o.card.ord = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : (aleph' a).ord = o
⊢ (ℵ_ (a - ω)).ord = o

Proof state:
case h
o : Ordinal.{u_1}
ho : o.card.ord = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : (aleph' a).ord = o
⊢ (ℵ_ (a - ω)).ord = o

Tactic:
rwa [aleph_eq_aleph', Ordinal.add_sub_cancel_of_le]

Result:
case h
o : Ordinal.{u_1}
ho : o.card.ord = o
ho' : ω ≤ o
a : Ordinal.{u_1}
ha : (aleph' a).ord = o
⊢ ω ≤ a
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_insert [Preorder α] [IsTotal α (· ≤ ·)] [DecidableRel (α := α) (· ≤ ·)] (x : α) :
    ∀ t : Ordnode α, dual (Ordnode.insert x t) = @Ordnode.insert αᵒᵈ _ _ x (dual t)
  | nil => rfl
  | node _ l y r => by
    have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl
    rw [Ordnode.insert, dual, Ordnode.insert, this, ← cmpLE_swap x y]
    cases cmpLE x y <;>
      simp [Ordering.swap, Ordnode.insert, dual_balanceL, dual_balanceR, dual_insert]

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (Ordnode.insert x (node size✝ l y r)).dual = Ordnode.insert x (node size✝ l y r).dual

Tactic:
have : @cmpLE αᵒᵈ _ _ x y = cmpLE y x := rfl

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (Ordnode.insert x (node size✝ l y r)).dual = Ordnode.insert x (node size✝ l y r).dual

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)

Tactic:
cases cmpLE x y <;>
  simp [Ordering.swap, Ordnode.insert, dual_balanceL, dual_balanceR, dual_insert]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (Ordnode.insert x (node size✝ l y r)).dual = Ordnode.insert x (node size✝ l y r).dual

Tactic:
rw [Ordnode.insert, dual, Ordnode.insert, this, ← cmpLE_swap x y]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
this : cmpLE x y = cmpLE y x
⊢ (match cmpLE x y with
      | Ordering.lt => (Ordnode.insert x l).balanceL y r
      | Ordering.eq => node size✝ l x r
      | Ordering.gt => l.balanceR y (Ordnode.insert x r)).dual =
    match (cmpLE x y).swap with
    | Ordering.lt => (Ordnode.insert x r.dual).balanceL y l.dual
    | Ordering.eq => node size✝ r.dual x l.dual
    | Ordering.gt => r.dual.balanceR y (Ordnode.insert x l.dual)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_eq_size_of_false {p : α → Bool} {xs : Array α} (h : ∀ x ∈ xs, p x = false) :
    xs.findIdx p = xs.size

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
h : ∀ (x : α), x ∈ xs → p x = false
⊢ findIdx p xs = xs.size

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ { toList := xs } → p x = false
⊢ findIdx p { toList := xs } = { toList := xs }.size

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ { toList := xs } → p x = false
⊢ findIdx p { toList := xs } = { toList := xs }.size

Tactic:
simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem hom.inj_on_objects : Function.Injective (hom S).obj

Proof state:
case mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd : S.hom.obj ⟨c, hc⟩ = S.hom.obj ⟨d, hd⟩
⊢ c = d

Tactic:
exact hcd

Result:
no goals

Proof state:
case mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd : S.hom.obj ⟨c, hc⟩ = S.hom.obj ⟨d, hd⟩
⊢ ⟨c, hc⟩ = ⟨d, hd⟩

Tactic:
simp only [Subtype.mk_eq_mk]

Result:
case mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd : S.hom.obj ⟨c, hc⟩ = S.hom.obj ⟨d, hd⟩
⊢ c = d

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ Function.Injective S.hom.obj

Tactic:
rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd

Result:
case mk.mk
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
hc : c ∈ S.objs
d : C
hd : d ∈ S.objs
hcd : S.hom.obj ⟨c, hc⟩ = S.hom.obj ⟨d, hd⟩
⊢ ⟨c, hc⟩ = ⟨d, hd⟩
-- Mathlib/GroupTheory/Complement.lean
theorem rightQuotientEquiv_apply {f : Quotient (QuotientGroup.rightRel H) → G}
    (hf : ∀ q, Quotient.mk'' (f q) = q) (q : Quotient (QuotientGroup.rightRel H)) :
    (rightQuotientEquiv (isComplement_range_right hf) q : G) = f q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ ⋯.rightQuotientEquiv q = ⟨f q, ⋯⟩

Tactic:
exact (rightQuotientEquiv (isComplement_range_right hf)).apply_eq_iff_eq_symm_apply.2 (hf q).symm

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ ↑(⋯.rightQuotientEquiv q) = f q

Tactic:
refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : Quotient (QuotientGroup.rightRel H) → G
hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q
q : Quotient (QuotientGroup.rightRel H)
⊢ ⋯.rightQuotientEquiv q = ⟨f q, ⋯⟩
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_iff_forall_nat_le {n : ℕ∞} :
    ContDiff 𝕜 n f ↔ ∀ m : ℕ, ↑m ≤ n → ContDiff 𝕜 m f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiff 𝕜 (↑m) f

Tactic:
simp_rw [← contDiffOn_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiffOn 𝕜 (↑m) f univ

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiffOn 𝕜 (↑n) f univ ↔ ∀ (m : ℕ), ↑m ≤ n → ContDiffOn 𝕜 (↑m) f univ

Tactic:
exact contDiffOn_iff_forall_nat_le

Result:
no goals