harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/Irrational.lean
theorem dense_irrational : Dense { x : ℝ | Irrational x }

Proof state:
a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ ({x | Irrational x} ∩ Ioo ↑a ↑b).Nonempty

Tactic:
exact exists_irrational_btwn (Rat.cast_lt.2 hlt)

Result:
no goals

Proof state:
⊢ Dense {x | Irrational x}

Tactic:
refine Real.isTopologicalBasis_Ioo_rat.dense_iff.2 ?_

Result:
⊢ ∀ o ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}, o.Nonempty → (o ∩ {x | Irrational x}).Nonempty

Proof state:
a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ (Ioo ↑a ↑b ∩ {x | Irrational x}).Nonempty

Tactic:
rw [inter_comm]

Result:
a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ ({x | Irrational x} ∩ Ioo ↑a ↑b).Nonempty

Proof state:
⊢ ∀ o ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}, o.Nonempty → (o ∩ {x | Irrational x}).Nonempty

Tactic:
simp only [mem_iUnion, mem_singleton_iff, exists_prop, forall_exists_index, and_imp]

Result:
⊢ ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → o.Nonempty → (o ∩ {x | Irrational x}).Nonempty

Proof state:
⊢ ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → o.Nonempty → (o ∩ {x | Irrational x}).Nonempty

Tactic:
rintro _ a b hlt rfl _

Result:
a b : ℚ
hlt : a < b
a✝ : (Ioo ↑a ↑b).Nonempty
⊢ (Ioo ↑a ↑b ∩ {x | Irrational x}).Nonempty
-- Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
lemma projectiveFamilyContent_iUnion_le (hP : IsProjectiveMeasureFamily P)
    {s : ℕ → Set (Π i : ι, α i)} (hs : ∀ n, s n ∈ measurableCylinders α) (n : ℕ) :
    projectiveFamilyContent hP (⋃ i ≤ n, s i)
      ≤ ∑ i ∈ range (n + 1), projectiveFamilyContent hP (s i) :=
  calc projectiveFamilyContent hP (⋃ i ≤ n, s i)
  _ = projectiveFamilyContent hP (⋃ i ∈ range (n + 1), s i)

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
hP : IsProjectiveMeasureFamily P
s : ℕ → Set ((i : ι) → α i)
hs : ∀ (n : ℕ), s n ∈ measurableCylinders α
n : ℕ
⊢ (projectiveFamilyContent hP) (⋃ i, ⋃ (_ : i ≤ n), s i) = (projectiveFamilyContent hP) (⋃ i ∈ range (n + 1), s i)

Tactic:
simp only [mem_range_succ_iff]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Filter.Eventually.curry_nhds {p : X × Y → Prop} {x : X} {y : Y}
    (h : ∀ᶠ x in 𝓝 (x, y), p x) : ∀ᶠ x' in 𝓝 x, ∀ᶠ y' in 𝓝 y, p (x', y')

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')

Tactic:
exact h.curry

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 (x, y), p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')

Tactic:
rw [nhds_prod_eq] at h

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
p : X × Y → Prop
x : X
y : Y
h : ∀ᶠ (x : X × Y) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : X) in 𝓝 x, ∀ᶠ (y' : Y) in 𝓝 y, p (x', y')
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem mul_leftUnitor {M : Mon_ C} :
    (tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ ((λ_ (𝟙_ C)).hom ⊗ M.mul)) ≫ (λ_ M.X).hom =
      ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ ((λ_ (𝟙_ C)).hom ⊗ M.mul)) ≫ (λ_ M.X).hom = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul

Tactic:
rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp M.mul, tensor_comp]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (M.X ⊗ M.X)) ≫ (𝟙 (𝟙_ C) ⊗ M.mul)) ≫ (λ_ M.X).hom =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (M.X ⊗ M.X)) ≫ (𝟙 (𝟙_ C) ⊗ M.mul)) ≫ (λ_ M.X).hom =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
simp only [tensorHom_id, id_tensorHom]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ (λ_ (𝟙_ C)).hom ▷ (M.X ⊗ M.X) ≫ 𝟙_ C ◁ M.mul) ≫ (λ_ M.X).hom =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ (tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ (λ_ (𝟙_ C)).hom ▷ (M.X ⊗ M.X) ≫ 𝟙_ C ◁ M.mul) ≫ (λ_ M.X).hom =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
slice_lhs 3 4 => rw [leftUnitor_naturality]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ (λ_ (𝟙_ C)).hom ▷ (M.X ⊗ M.X) ≫ (λ_ (M.X ⊗ M.X)).hom ≫ M.mul =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
simp only [Category.assoc, Category.id_comp]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ tensorμ (𝟙_ C) M.X (𝟙_ C) M.X ≫ (λ_ (𝟙_ C)).hom ▷ (M.X ⊗ M.X) ≫ (λ_ (M.X ⊗ M.X)).hom ≫ M.mul =
    ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul

Tactic:
slice_lhs 1 3 => rw [← leftUnitor_monoidal]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Mon_ C
⊢ ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ M.mul = ((λ_ M.X).hom ⊗ (λ_ M.X).hom) ≫ 𝟙 (M.X ⊗ M.X) ≫ M.mul
-- Mathlib/FieldTheory/KummerPolynomial.lean
lemma ne_zero_of_irreducible_X_pow_sub_C {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
    n ≠ 0

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
K : Type u
inst✝ : Field K
a : K
H : Irreducible (X ^ 0 - C a)
⊢ False

Proof state:
K : Type u
inst✝ : Field K
a : K
H : Irreducible (X ^ 0 - C a)
⊢ False

Tactic:
rw [pow_zero, ← C.map_one, ← map_sub] at H

Result:
K : Type u
inst✝ : Field K
a : K
H : Irreducible (C (1 - a))
⊢ False

Proof state:
K : Type u
inst✝ : Field K
a : K
H : Irreducible (C (1 - a))
⊢ False

Tactic:
exact not_irreducible_C _ H

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_ite_eq' (i : ι) (f : ι → M) :
    𝔼 j, (if j = i then f j else 0) = f i /ℚ card ι

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j : ι, if j = i then f j else 0) = (↑(card ι))⁻¹ • f i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_ite_eq_false_eq_false {p : Prop} [h : Decidable p] {b c : Bool} :
  ¬(ite p (b = false) (c = false)) ↔ (ite p (b = true) (c = true))

Proof state:
p : Prop
h : Decidable p
b c : Bool
⊢ (¬if p then b = false else c = false) ↔ if p then b = true else c = true

Tactic:
cases h with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ : Prop
b c : Bool
p : p✝
⊢ (¬if p✝ then b = false else c = false) ↔ if p✝ then b = true else c = true

Tactic:
simp [p]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem inv_map_inv_app (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) :
    inv ((F.map e.inv).app Z) = (F.map e.hom).app Z

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D ⥤ E
X Y : C
e : X ≅ Y
Z : D
⊢ inv ((F.map e.inv).app Z) = (F.map e.hom).app Z

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma isComplex₀ (S : ComposableArrows C 0) : S.IsComplex where
  -- See https://github.com/leanprover/lean4/issues/2862
  -- Without `decide := true`, simp gets stuck at `hi : autoParam False _auto✝`
  zero i hi

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 0
i : ℕ
hi : autoParam (i + 2 ≤ 0) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
simp +decide at hi

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_def (n : ℕ) :
    bernoulli' n = 1 - ∑ k ∈ range n, n.choose k / (n - k + 1) * bernoulli' k

Proof state:
n : ℕ
⊢ bernoulli' n = 1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k

Tactic:
rw [bernoulli'_def', ← Fin.sum_univ_eq_sum_range]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_self {X : C} (P : Subobject X) (h) : P.factorThru P.arrow h = 𝟙 (P : C)

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
h : P.Factors P.arrow
⊢ P.factorThru P.arrow h ≫ P.arrow = 𝟙 (underlying.obj P) ≫ P.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
h : P.Factors P.arrow
⊢ P.factorThru P.arrow h = 𝟙 (underlying.obj P)

Tactic:
ext

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
h : P.Factors P.arrow
⊢ P.factorThru P.arrow h ≫ P.arrow = 𝟙 (underlying.obj P) ≫ P.arrow
-- Mathlib/Combinatorics/Quiver/Prefunctor.lean
theorem congr_obj {U V : Type*} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) (X : U) :
    F.obj X = G.obj X

Proof state:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X : U
⊢ F.obj X = G.obj X

Tactic:
cases e

Result:
case refl
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X : U
⊢ F.obj X = F.obj X

Proof state:
case refl
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X : U
⊢ F.obj X = F.obj X

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_mul_prod_eq_prod_zipWith_of_length_eq (l l' : List M) (h : l.length = l'.length) :
    l.prod * l'.prod = (zipWith (· * ·) l l').prod

Proof state:
M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ l.prod * l'.prod = (zipWith (fun x1 x2 => x1 * x2) l l').prod

Tactic:
apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans

Result:
M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ (zipWith (fun x1 x2 => x1 * x2) l l').prod * (drop l'.length l).prod * (drop l.length l').prod =
    (zipWith (fun x1 x2 => x1 * x2) l l').prod

Proof state:
M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ (zipWith (fun x1 x2 => x1 * x2) l l').prod * (drop l'.length l).prod * (drop l.length l').prod =
    (zipWith (fun x1 x2 => x1 * x2) l l').prod

Tactic:
rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem invAux_not_mem_invSet (a : Nimber) : invAux a ∉ invSet a

Proof state:
a : Nimber
⊢ a.invAux ∉ a.invSet

Tactic:
rw [invAux]

Result:
a : Nimber
⊢ sInf a.invSetᶜ ∉ a.invSet

Proof state:
a : Nimber
⊢ sInf a.invSetᶜ ∉ a.invSet

Tactic:
exact csInf_mem (invSet_nonempty a)

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem Equiv.symm {l₁ l₂ : Lists α} (h : l₁ ~ l₂) : l₂ ~ l₁

Proof state:
α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁

Tactic:
obtain - | ⟨h₁, h₂⟩ := h <;> [rfl; exact Equiv.antisymm h₂ h₁]

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem continuous_vComp : Continuous f.vComp

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
this : Continuous ((fun x => (↑x, f.toFun x)) ∘ v.proj)
⊢ Continuous f.vComp

Tactic:
refine ContinuousOn.comp_continuous v.continuousOn this fun x => ?_

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
this : Continuous ((fun x => (↑x, f.toFun x)) ∘ v.proj)
x : ℝ
⊢ ((fun x => (↑x, f.toFun x)) ∘ v.proj) x ∈ Icc v.tMin v.tMax ×ˢ closedBall v.x₀ ↑v.R

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
⊢ Continuous f.vComp

Tactic:
have := (continuous_subtype_val.prod_mk f.continuous).comp v.continuous_proj

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
this : Continuous ((fun x => (↑x, f.toFun x)) ∘ v.proj)
⊢ Continuous f.vComp

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : v.FunSpace
this : Continuous ((fun x => (↑x, f.toFun x)) ∘ v.proj)
x : ℝ
⊢ ((fun x => (↑x, f.toFun x)) ∘ v.proj) x ∈ Icc v.tMin v.tMax ×ˢ closedBall v.x₀ ↑v.R

Tactic:
exact ⟨(v.proj x).2, f.mem_closedBall _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_append_left {as bs : Array α} {i : Nat} (hn : i < as.size) :
    (as ++ bs)[i]? = as[i]?

Proof state:
α : Type u_1
as bs : Array α
i : Nat
hn : i < as.size
⊢ (as ++ bs)[i]? = as[i]?

Tactic:
have hn' : i < (as ++ bs).size := Nat.lt_of_lt_of_le hn <|
  size_append .. ▸ Nat.le_add_right ..

Result:
α : Type u_1
as bs : Array α
i : Nat
hn : i < as.size
hn' : i < (as ++ bs).size
⊢ (as ++ bs)[i]? = as[i]?

Proof state:
α : Type u_1
as bs : Array α
i : Nat
hn : i < as.size
hn' : i < (as ++ bs).size
⊢ (as ++ bs)[i]? = as[i]?

Tactic:
simp_all [getElem?_eq_getElem, getElem_append]

Result:
no goals
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem factorThruImageSubobject_comp_imageToKernel (w : f ≫ g = 0) :
    factorThruImageSubobject f ≫ imageToKernel f g w = factorThruKernelSubobject g f w

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ (factorThruImageSubobject f ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow =
    factorThruKernelSubobject g f w ≫ (kernelSubobject g).arrow

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ imageToKernel f g w = factorThruKernelSubobject g f w

Tactic:
ext

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ (factorThruImageSubobject f ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow =
    factorThruKernelSubobject g f w ≫ (kernelSubobject g).arrow
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} :
    (alterKey k f l).length =
      if h : containsKey k l then
        if f (getValueCast k l h) |>.isSome then l.length else l.length - 1
      else
        if f none |>.isSome then l.length + 1 else l.length

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if h : containsKey k l = true then if (f (some (getValueCast k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length

Tactic:
cases h : getValueCast? k l <;> split <;> simp_all [length_eraseKey, length_insertEntry,
  containsKey_eq_isSome_getValueCast?, ← getValueCast?_eq_some_getValueCast]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (alterKey k f l).length =
    if h : containsKey k l = true then if (f (some (getValueCast k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length

Tactic:
rw [alterKey]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match f (getValueCast? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).length =
    if h : containsKey k l = true then if (f (some (getValueCast k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length
-- Mathlib/NumberTheory/Fermat.lean
theorem coprime_fermatNumber_fermatNumber {m n : ℕ} (hmn : m ≠ n) :
    Coprime (fermatNumber m) (fermatNumber n)

Proof state:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
have h_n : d ∣ fermatNumber n := gcd_dvd_right ..

Result:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber

Proof state:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
h_two : d = 2
⊢ False

Tactic:
exact (odd_fermatNumber _).not_two_dvd_nat (h_two ▸ h_n)

Result:
no goals

Proof state:
m n : ℕ
hmn : m ≠ n
this : ∀ {m n : ℕ}, m ≠ n → m < n → m.fermatNumber.Coprime n.fermatNumber
hmn' : ¬m < n
⊢ n < m

Tactic:
omega

Result:
no goals

Proof state:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
have h_m : d ∣ 2 := (Nat.dvd_add_right <| (gcd_dvd_left _ _).trans <| dvd_prod_of_mem _
  <| mem_range.mpr hmn').mp <| fermatNumber_eq_prod_add_two _ ▸ h_n

Result:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
⊢ m.fermatNumber.Coprime n.fermatNumber

Proof state:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
let d := (fermatNumber m).gcd (fermatNumber n)

Result:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
⊢ m.fermatNumber.Coprime n.fermatNumber

Proof state:
case inr
m n : ℕ
hmn : m ≠ n
this : ∀ {m n : ℕ}, m ≠ n → m < n → m.fermatNumber.Coprime n.fermatNumber
hmn' : ¬m < n
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
simpa only [coprime_comm] using this hmn.symm (by omega)

Result:
no goals

Proof state:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
refine ((dvd_prime prime_two).mp h_m).resolve_right fun h_two ↦ ?_

Result:
m n : ℕ
hmn : m ≠ n
hmn' : m < n
d : ℕ := m.fermatNumber.gcd n.fermatNumber
h_n : d ∣ n.fermatNumber
h_m : d ∣ 2
h_two : d = 2
⊢ False

Proof state:
m n : ℕ
hmn : m ≠ n
⊢ m.fermatNumber.Coprime n.fermatNumber

Tactic:
wlog hmn' : m < n

Result:
case inr
m n : ℕ
hmn : m ≠ n
this : ∀ {m n : ℕ}, m ≠ n → m < n → m.fermatNumber.Coprime n.fermatNumber
hmn' : ¬m < n
⊢ m.fermatNumber.Coprime n.fermatNumber

m n : ℕ
hmn : m ≠ n
hmn' : m < n
⊢ m.fermatNumber.Coprime n.fermatNumber
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem measurable_measure_condCDF (ρ : Measure (α × ℝ)) :
    Measurable fun a => (condCDF ρ a).measure :=
  .measure_of_isPiSystem_of_isProbabilityMeasure (borel_eq_generateFrom_Iic ℝ) isPiSystem_Iic <| by
    simp_rw [forall_mem_range, measure_condCDF_Iic]
    exact fun u ↦ (measurable_condCDF ρ u).ennreal_ofReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (i : ℝ), Measurable fun a => ENNReal.ofReal (↑(condCDF ρ a) i)

Tactic:
exact fun u ↦ (measurable_condCDF ρ u).ennreal_ofReal

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ s ∈ range Iic, Measurable fun a => (condCDF ρ a).measure s

Tactic:
simp_rw [forall_mem_range, measure_condCDF_Iic]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (i : ℝ), Measurable fun a => ENNReal.ofReal (↑(condCDF ρ a) i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem?_modifyHead {l : List α} {f : α → α} {n} :
    (l.modifyHead f)[n]? = if n = 0 then l[n]?.map f else l[n]?

Proof state:
α : Type u_1
l : List α
f : α → α
n : Nat
⊢ (modifyHead f l)[n]? = if n = 0 then Option.map f l[n]? else l[n]?

Tactic:
cases l with
| nil => simp
| cons hd tl => cases n <;> simp

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → α
n : Nat
⊢ (modifyHead f [])[n]? = if n = 0 then Option.map f [][n]? else [][n]?

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
n : Nat
hd : α
tl : List α
⊢ (modifyHead f (hd :: tl))[n]? = if n = 0 then Option.map f (hd :: tl)[n]? else (hd :: tl)[n]?

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_isSome {xs : Vector α n} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true ↔
    ∃ x, x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ p x = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type
n : Nat
xs : Vector α n
p : α → Bool
⊢ (find? p xs).isSome = true ↔ ∃ x, x ∈ xs ∧ p x = true

Tactic:
cases xs

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true ↔
    ∃ x, x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } ∧ p x = true
-- Mathlib/Algebra/Order/Floor.lean
theorem natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : α) = ⌊a⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ↑⌊a⌋

Tactic:
rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma range_succ (n : ℕ) : Set.range (Fin.succ : Fin n → Fin (n + 1)) = {0}ᶜ

Proof state:
n : ℕ
⊢ Set.range succ = {0}ᶜ

Tactic:
rw [← succAbove_zero]

Result:
n : ℕ
⊢ Set.range (succAbove 0) = {0}ᶜ

Proof state:
n : ℕ
⊢ Set.range (succAbove 0) = {0}ᶜ

Tactic:
exact range_succAbove (0 : Fin (n + 1))

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem empty_inter (s : Finset α) : ∅ ∩ s = ∅ :=
  ext fun _ => mem_inter.trans <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ ∅ ∧ x✝ ∈ s ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem le_ker_iff_map [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} :
    p ≤ ker f ↔ map f p = ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
p : Submodule R M
⊢ p ≤ ker f ↔ map f p = ⊥

Tactic:
rw [ker, eq_bot_iff, map_le_iff_le_comap]

Result:
no goals