harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/Partrec.lean
theorem list_ofFn :
    ∀ {n} {f : Fin n → α → σ},
      (∀ i, Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
  | 0, _, _ => by
    simp only [List.ofFn_zero]
    exact const []
  | n + 1, f, hf => by
    simp only [List.ofFn_succ]
    exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a => List.ofFn fun i => f i a

Tactic:
simp only [List.ofFn_succ]

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a => f 0 a :: List.ofFn fun i => f i.succ a

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a => f 0 a :: List.ofFn fun i => f i.succ a

Tactic:
exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)
⊢ Computable fun a => []

Tactic:
exact const []

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)
⊢ Computable fun a => List.ofFn fun i => x✝¹ i a

Tactic:
simp only [List.ofFn_zero]

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)
⊢ Computable fun a => []
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem extract_gcd' (f g : β → α) (hs : ∃ x, x ∈ s ∧ f x ≠ 0)
    (hg : ∀ b ∈ s, f b = s.gcd f * g b) : s.gcd g = 1 :=
  ((@mul_right_eq_self₀ _ _ (s.gcd f) _).1 <| by
        conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]).resolve_right <| by
    contrapose! hs
    exact gcd_eq_zero_iff.1 hs

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ ¬s.gcd f = 0

Tactic:
contrapose! hs

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hg : ∀ b ∈ s, f b = s.gcd f * g b
hs : s.gcd f = 0
⊢ ∀ x ∈ s, f x = 0

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hg : ∀ b ∈ s, f b = s.gcd f * g b
hs : s.gcd f = 0
⊢ ∀ x ∈ s, f x = 0

Tactic:
exact gcd_eq_zero_iff.1 hs

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ s.gcd f * s.gcd g = s.gcd f

Tactic:
conv_lhs => rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
    ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : Raw α (fun _ => β)).insert k v) tl

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
tl : List (α × β)
⊢ (Raw₀.Const.insertMany Raw₀.empty ((k, v) :: tl)).val.val =
    (Raw₀.Const.insertMany (Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v) tl).val.val

Tactic:
rw [Raw₀.Const.insertMany_empty_list_cons]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
tl : List (α × β)
⊢ ofList ((k, v) :: tl) = insertMany (∅.insert k v) tl

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
k : α
v : β
tl : List (α × β)
⊢ (Raw₀.Const.insertMany Raw₀.empty ((k, v) :: tl)).val.val =
    (Raw₀.Const.insertMany (Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v) tl).val.val
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_modify (h : m.1.WF) {k : α} {f : β k → β k} :
    (m.modify k f).1.isEmpty = m.1.isEmpty

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : β k → β k
⊢ (m.modify k f).val.isEmpty = m.val.isEmpty

Tactic:
simp_to_model [modify] using List.isEmpty_modifyKey

Result:
no goals
-- Mathlib/Data/Finset/Slice.lean
theorem sized_iUnion₂ {f : ∀ i, κ i → Set (Finset α)} :
    (⋃ (i) (j), f i j).Sized r ↔ ∀ i j, (f i j).Sized r

Proof state:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
r : ℕ
f : (i : ι) → κ i → Set (Finset α)
⊢ Sized r (⋃ i, ⋃ j, f i j) ↔ ∀ (i : ι) (j : κ i), Sized r (f i j)

Tactic:
simp only [Set.sized_iUnion]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid {f : PartialHomeomorph H H}
    (hf : f ∈ G) : f ∈ G.maximalAtlas H

Proof state:
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
f : PartialHomeomorph H H
hf : f ∈ G
⊢ f.symm ≫ₕ PartialHomeomorph.refl H ∈ G ∧ (PartialHomeomorph.refl H).symm ≫ₕ f ∈ G

Tactic:
exact ⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩

Result:
no goals

Proof state:
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
f : PartialHomeomorph H H
hf : f ∈ G
⊢ f ∈ maximalAtlas H G

Tactic:
rintro e (rfl : e = PartialHomeomorph.refl H)

Result:
H : Type u
inst✝ : TopologicalSpace H
G : StructureGroupoid H
f : PartialHomeomorph H H
hf : f ∈ G
⊢ f.symm ≫ₕ PartialHomeomorph.refl H ∈ G ∧ (PartialHomeomorph.refl H).symm ≫ₕ f ∈ G
-- Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean
theorem epi_of_zero_cokernel {X Y : C} (f : X ⟶ Y) (Z : C)
    (l : IsColimit (CokernelCofork.ofπ (0 : Y ⟶ Z) (show f ≫ 0 = 0 by simp))) : Epi f :=
  ⟨fun u v huv => by
    obtain ⟨W, w, hw, hl⟩ := normalMonoOfMono (equalizer.ι u v)
    obtain ⟨m, hm⟩ := equalizer.lift' f huv
    have hwf : f ≫ w = 0

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
⊢ u = v

Tactic:
obtain ⟨W, w, hw, hl⟩ := normalMonoOfMono (equalizer.ι u v)

Result:
case mk
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
⊢ u = v

Proof state:
case mk.mk.mk
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
n : (CokernelCofork.ofπ 0 ⋯).pt ⟶ W
hn : 0 = w
this : IsIso (equalizer.ι u v)
⊢ equalizer.ι u v ≫ u = equalizer.ι u v ≫ v

Tactic:
exact equalizer.condition _ _

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ f ≫ w = 0

Tactic:
rw [← hm, Category.assoc, hw, comp_zero]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem nonMemberSubfamily_memberSubfamily :
    (𝒜.memberSubfamily a).nonMemberSubfamily a = 𝒜.memberSubfamily a

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ memberSubfamily a 𝒜

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (memberSubfamily a 𝒜) = memberSubfamily a 𝒜

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
a✝ : Finset α
⊢ a✝ ∈ nonMemberSubfamily a (memberSubfamily a 𝒜) ↔ a✝ ∈ memberSubfamily a 𝒜
-- Mathlib/Data/Real/Archimedean.lean
theorem sInf_le_iff (h : BddBelow s) (h' : s.Nonempty) :
    sInf s ≤ a ↔ ∀ ε, 0 < ε → ∃ x ∈ s, x < a + ε

Proof state:
case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε

Tactic:
exact exists_lt_of_csInf_lt h' (H ε ε_pos)

Result:
no goals

Proof state:
case mpr.intro.intro
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε

Tactic:
exact csInf_lt_of_lt h x_in hx

Result:
no goals

Proof state:
case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε

Tactic:
rcases H ε ε_pos with ⟨x, x_in, hx⟩

Result:
case mpr.intro.intro
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε

Proof state:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

Tactic:
constructor <;> intro H ε ε_pos

Result:
case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε

case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε

Proof state:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

Tactic:
rw [le_iff_forall_pos_lt_add]

Result:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_def_of_neg {x : ℝ} (hx : x < 0) (y : ℝ) : x ^ y = exp (log x * y) * cos (y * π)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)

Tactic:
rw [this, Complex.exp_add_mul_I, ← Complex.ofReal_exp, ← Complex.ofReal_cos, ←
  Complex.ofReal_sin, mul_add, ← Complex.ofReal_mul, ← mul_assoc, ← Complex.ofReal_mul,
  Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im,
  Real.log_neg_eq_log]

Result:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ rexp (log x * y) * cos (y * π) + ((↑(rexp (log x * y) * sin (y * π))).re * 0 - 0 * Complex.I.im) =
    rexp (log x * y) * cos (y * π)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)

Tactic:
have : Complex.log x * y = ↑(log (-x) * y) + ↑(y * π) * Complex.I := by
  simp only [Complex.log, Complex.norm_real, norm_eq_abs, abs_of_neg hx, log_neg_eq_log,
    Complex.arg_ofReal_of_neg hx, Complex.ofReal_mul]
  ring

Result:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
⊢ Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I

Tactic:
simp only [Complex.log, Complex.norm_real, norm_eq_abs, abs_of_neg hx, log_neg_eq_log,
  Complex.arg_ofReal_of_neg hx, Complex.ofReal_mul]

Result:
x : ℝ
hx : x < 0
y : ℝ
⊢ (↑(log x) + ↑π * Complex.I) * ↑y = ↑(log x) * ↑y + ↑y * ↑π * Complex.I

Proof state:
x : ℝ
hx : x < 0
y : ℝ
this : Complex.log ↑x * ↑y = ↑(log (-x) * y) + ↑(y * π) * Complex.I
⊢ rexp (log x * y) * cos (y * π) + ((↑(rexp (log x * y) * sin (y * π))).re * 0 - 0 * Complex.I.im) =
    rexp (log x * y) * cos (y * π)

Tactic:
ring

Result:
no goals

Proof state:
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0

Tactic:
exact ne_of_lt hx

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
⊢ x ^ y = rexp (log x * y) * cos (y * π)

Tactic:
rw [rpow_def, Complex.cpow_def, if_neg]

Result:
x : ℝ
hx : x < 0
y : ℝ
⊢ (Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)

case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0

Proof state:
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬↑x = 0

Tactic:
rw [Complex.ofReal_eq_zero]

Result:
case hnc
x : ℝ
hx : x < 0
y : ℝ
⊢ ¬x = 0

Proof state:
x : ℝ
hx : x < 0
y : ℝ
⊢ (↑(log x) + ↑π * Complex.I) * ↑y = ↑(log x) * ↑y + ↑y * ↑π * Complex.I

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem innerDualCone_eq_iInter_innerDualCone_singleton :
    (s.innerDualCone : Set H) = ⋂ i : s, (({↑i} : Set H).innerDualCone : Set H)

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s : Set H
⊢ ↑s.innerDualCone = ⋂ i, ↑{↑i}.innerDualCone

Tactic:
rw [← ConvexCone.coe_iInf, ← innerDualCone_iUnion, iUnion_of_singleton_coe]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
theorem basis_le_iff {J K : TwoSidedIdeal R} {d e : σ →₀ ℕ} (hK : K ≠ ⊤) :
    basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e⟩ ↔ J ≤ K ∧ e ≤ d

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d

Tactic:
constructor

Result:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ basis σ R (J, d) ≤ basis σ R (K, e) → J ≤ K ∧ e ≤ d

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
⊢ J ≤ K ∧ e ≤ d → basis σ R (J, d) ≤ basis σ R (K, e)

Proof state:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
⊢ ↑J ⊆ ↑K ∧ e ≤ d

Tactic:
constructor

Result:
case mp.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
⊢ ↑J ⊆ ↑K

case mp.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
J K : TwoSidedIdeal R
d e : σ →₀ ℕ
hK : K ≠ ⊤
h : ∀ (a : MvPowerSeries σ R), (∀ e ≤ d, (coeff R e) a ∈ J) → ∀ e_1 ≤ e, (coeff R e_1) a ∈ K
⊢ e ≤ d
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem seqTendstoAeSeq_spec (hfg : TendstoInMeasure μ f atTop g) (n k : ℕ)
    (hn : seqTendstoAeSeq hfg n ≤ k) :
    μ { x | (2 : ℝ)⁻¹ ^ n ≤ dist (f k x) (g x) } ≤ (2 : ℝ≥0∞)⁻¹ ^ n

Proof state:
case zero
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg 0 ≤ k
⊢ μ {x | 2⁻¹ ^ 0 ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ 0

Tactic:
exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n k : ℕ
hn : seqTendstoAeSeq hfg n ≤ k
⊢ μ {x | 2⁻¹ ^ n ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ n

Tactic:
cases n

Result:
case zero
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg 0 ≤ k
⊢ μ {x | 2⁻¹ ^ 0 ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ 0

case succ
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (n✝ + 1) ≤ k
⊢ μ {x | 2⁻¹ ^ (n✝ + 1) ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ (n✝ + 1)

Proof state:
case succ
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (n✝ + 1) ≤ k
⊢ μ {x | 2⁻¹ ^ (n✝ + 1) ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ (n✝ + 1)

Tactic:
exact Classical.choose_spec
  (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)

Result:
no goals
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
@[simp]
lemma shiftIso_zero_inv_app (a : A) (X : C) :
    (F.shiftIso 0 a a (zero_add a)).inv.app X = (shiftFunctorZero D A).inv.app _

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (isoWhiskerLeft (F.functor a) (shiftFunctorZero D A)).inv.app X =
    (shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (F.shiftIso 0 a a ⋯).inv.app X = (shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)

Tactic:
rw [shiftIso_zero]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (isoWhiskerLeft (F.functor a) (shiftFunctorZero D A)).inv.app X =
    (shiftFunctorZero D A).inv.app ((F.functor a).toPrefunctor.1 X)
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem succ_mersenne (k : ℕ) : mersenne k + 1 = 2 ^ k

Proof state:
k : ℕ
⊢ 1 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
k : ℕ
⊢ mersenne k + 1 = 2 ^ k

Tactic:
rw [mersenne, tsub_add_cancel_of_le]

Result:
k : ℕ
⊢ 1 ≤ 2 ^ k

Proof state:
k : ℕ
⊢ 1 ≤ 2 ^ k

Tactic:
exact one_le_pow₀ (by norm_num)

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem smul_mem_of_mem (hx : x ∈ fundamentalCone K) (hc : c ≠ 0) :
    c • x ∈ fundamentalCone K

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∉ {x | mixedEmbedding.norm x = 0}

Tactic:
rw [Set.mem_setOf_eq, mixedEmbedding.norm_smul, mul_eq_zero, not_or]

Result:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬mixedEmbedding.norm x = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∈ fundamentalCone K

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∉ {x | mixedEmbedding.norm x = 0}

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ c • x ∈ logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
rw [Set.mem_preimage, logMap_real_smul hx.2 hc]

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ logMap x ∈ ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
exact hx.1

Result:
no goals

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
c : ℝ
hx : x ∈ fundamentalCone K
hc : c ≠ 0
⊢ ¬|c| ^ Module.finrank ℚ K = 0 ∧ ¬mixedEmbedding.norm x = 0

Tactic:
exact ⟨pow_ne_zero _ (abs_ne_zero.mpr hc), hx.2⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_empty (δ : ℝ) : thickening δ (∅ : Set α) = ∅

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
⊢ thickening δ ∅ = ∅

Tactic:
simp only [thickening, setOf_false, infEdist_empty, not_top_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_append (l₁ l₂ : Array α) :
    (l₁ ++ l₂).eraseP p = if l₁.any p then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).eraseP p =
    if { toList := l₁ }.any p = true then { toList := l₁ }.eraseP p ++ { toList := l₂ }
    else { toList := l₁ } ++ { toList := l₂ }.eraseP p

Tactic:
simp only [List.append_toArray, List.eraseP_toArray, List.eraseP_append l₁ l₂, List.any_toArray']

Result:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ (if l₁.any p = true then List.eraseP p l₁ ++ l₂ else l₁ ++ List.eraseP p l₂).toArray =
    if l₁.any p = true then (List.eraseP p l₁ ++ l₂).toArray else (l₁ ++ List.eraseP p l₂).toArray

Proof state:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
⊢ ({ toList := l₁ } ++ l₂).eraseP p =
    if { toList := l₁ }.any p = true then { toList := l₁ }.eraseP p ++ l₂ else { toList := l₁ } ++ l₂.eraseP p

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).eraseP p =
    if { toList := l₁ }.any p = true then { toList := l₁ }.eraseP p ++ { toList := l₂ }
    else { toList := l₁ } ++ { toList := l₂ }.eraseP p

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ (if l₁.any p = true then List.eraseP p l₁ ++ l₂ else l₁ ++ List.eraseP p l₂).toArray =
    if l₁.any p = true then (List.eraseP p l₁ ++ l₂).toArray else (l₁ ++ List.eraseP p l₂).toArray

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : Array α
⊢ (l₁ ++ l₂).eraseP p = if l₁.any p = true then l₁.eraseP p ++ l₂ else l₁ ++ l₂.eraseP p

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
⊢ ({ toList := l₁ } ++ l₂).eraseP p =
    if { toList := l₁ }.any p = true then { toList := l₁ }.eraseP p ++ l₂ else { toList := l₁ } ++ l₂.eraseP p