harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_range_eq_iSup {ι : Sort*} {v : ι → M} : span R (range v) = ⨆ i, R ∙ v i

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_9
v : ι → M
⊢ span R (range v) = ⨆ i, span R {v i}

Tactic:
rw [span_eq_iSup_of_singleton_spans, iSup_range]

Result:
no goals
-- Mathlib/Computability/Language.lean
@[simp]
lemma reverse_kstar (l : Language α) : l∗.reverse = l.reverse∗

Proof state:
α : Type u_1
l : Language α
⊢ l∗.reverse = l.reverse∗

Tactic:
simp only [kstar_eq_iSup_pow, reverse_iSup, reverse_pow]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma preimage_div (hm : Injective m) {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) :
    m ⁻¹' (s / t) = m ⁻¹' s / m ⁻¹' t :=
  hm.image_injective <| by
    rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (div_subset_range m hs ht)]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : DivisionMonoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' (⇑m ⁻¹' (s / t)) = ⇑m '' (⇑m ⁻¹' s / ⇑m ⁻¹' t)

Tactic:
rw [image_div, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
  image_preimage_eq_iff.2 (div_subset_range m hs ht)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_prod {ι : Type*} (f : ι → R[X]) (s : Finset ι) :
    s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => roots (f i)

Proof state:
case mk
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
f : ι → R[X]
m : Multiset ι
hm : m.Nodup
⊢ { val := m, nodup := hm }.prod f ≠ 0 →
    ({ val := m, nodup := hm }.prod f).roots = { val := m, nodup := hm }.val.bind fun i => (f i).roots

Tactic:
simpa [Multiset.prod_eq_zero_iff, Multiset.bind_map] using roots_multiset_prod (m.map f)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ s.prod f ≠ 0 → (s.prod f).roots = s.val.bind fun i => (f i).roots

Tactic:
rcases s with ⟨m, hm⟩

Result:
case mk
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
f : ι → R[X]
m : Multiset ι
hm : m.Nodup
⊢ { val := m, nodup := hm }.prod f ≠ 0 →
    ({ val := m, nodup := hm }.prod f).roots = { val := m, nodup := hm }.val.bind fun i => (f i).roots
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_one_iff_hasFDerivAt : ContDiff 𝕜 1 f ↔
    ∃ f' : E → E →L[𝕜] F, Continuous f' ∧ ∀ x, HasFDerivAt f (f' x) x

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
⊢ ContDiff 𝕜 1 f ↔ ∃ f', Continuous f' ∧ ∀ (x : E), HasFDerivAt f (f' x) x

Tactic:
convert contDiff_succ_iff_hasFDerivAt using 4

Result:
case h.e'_2.h.e'_2.h.h.e'_1.a
𝕜 : 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
x✝ : E → E →L[𝕜] F
⊢ Continuous x✝ ↔ ContDiff 𝕜 (↑0) x✝

Proof state:
case h.e'_2.h.e'_2.h.h.e'_1.a
𝕜 : 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
x✝ : E → E →L[𝕜] F
⊢ Continuous x✝ ↔ ContDiff 𝕜 (↑0) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem comapDomain_zero [∀ i, Zero (β i)] (h : κ → ι) (hh : Function.Injective h) :
    comapDomain h hh (0 : Π₀ i, β i) = 0

Proof state:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i✝ : κ
⊢ (comapDomain h hh 0) i✝ = 0 i✝

Tactic:
rw [zero_apply, comapDomain_apply, zero_apply]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
⊢ comapDomain h hh 0 = 0

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i✝ : κ
⊢ (comapDomain h hh 0) i✝ = 0 i✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_mul_tmod_right (a b : Int) : (-(a * b)).tmod a = 0

Proof state:
a b : Int
⊢ a ∣ a * b

Tactic:
exact Int.dvd_mul_right a b

Result:
no goals

Proof state:
a b : Int
⊢ (-(a * b)).tmod a = 0

Tactic:
rw [← dvd_iff_tmod_eq_zero, Int.dvd_neg]

Result:
a b : Int
⊢ a ∣ a * b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR

Proof state:
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l = (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Tactic:
rw [← Array.foldr_toList]

Result:
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l = (foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + l.toArray.size, []) l.toArray.toList).snd

Proof state:
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ f a (n.succ, enumFrom n.succ as) = (n, enumFrom n (a :: as))

Tactic:
simp [enumFrom, f]

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ foldr f (n + (a :: as).length, []) (a :: as) = (n, enumFrom n (a :: as))

Tactic:
rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]

Result:
α : Type u_1
n✝ : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
a : α
as : List α
n : Nat
⊢ f a (n.succ, enumFrom n.succ as) = (n, enumFrom n (a :: as))

Proof state:
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l = (foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + l.toArray.size, []) l.toArray.toList).snd

Tactic:
simp +zetaDelta [go]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l = (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Tactic:
let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)

Result:
case h.h.h
α : Type u_1
n : Nat
l : List α
f : α → Nat × List (Nat × α) → Nat × List (Nat × α) :=
  fun a x =>
    match x with
    | (n, acc) => (n - 1, (n - 1, a) :: acc)
⊢ enumFrom n l = (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Proof state:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l = enumFromTR n l

Tactic:
simp [enumFromTR, -Array.size_toArray]

Result:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l = (Array.foldr (fun a x => (x.fst - 1, (x.fst - 1, a) :: x.snd)) (n + l.toArray.size, []) l.toArray).snd

Proof state:
⊢ @enumFrom = @enumFromTR

Tactic:
funext α n l

Result:
case h.h.h
α : Type u_1
n : Nat
l : List α
⊢ enumFrom n l = enumFromTR n l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_eq_map_iff {f : α → β} :
    L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
n✝¹ : Nat
L₁ : Vector β n✝¹
n✝ : Nat
L₂ : Vector β n✝
l : Vector α (n✝¹ + n✝)
f : α → β
⊢ L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Tactic:
rw [eq_comm, map_eq_append_iff]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.le_iff_forall_le (h : IsSuccPrelimit a) : a ≤ b ↔ ∀ c < a, c ≤ b

Proof state:
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
⊢ a ≤ b ↔ ∀ c < a, c ≤ b

Tactic:
use fun ha c hc ↦ hc.le.trans ha

Result:
case mpr
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
⊢ (∀ c < a, c ≤ b) → a ≤ b

Proof state:
case mpr
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
⊢ a ≤ b

Tactic:
by_contra! ha

Result:
case mpr
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
ha : b < a
⊢ False

Proof state:
case mpr
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
ha : b < a
⊢ False

Tactic:
exact h b ⟨ha, fun c hb hc ↦ (H c hc).not_lt hb⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
⊢ (∀ c < a, c ≤ b) → a ≤ b

Tactic:
intro H

Result:
case mpr
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit a
H : ∀ c < a, c ≤ b
⊢ a ≤ b
-- Mathlib/CategoryTheory/Sites/Subsheaf.lean
theorem Subpresheaf.isSheaf_iff (h : Presieve.IsSheaf J F) :
    Presieve.IsSheaf J G.toPresheaf ↔
      ∀ (U) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U

Tactic:
change _ ↔ G.sheafify J ≤ G

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ sheafify J G ≤ G

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ sheafify J G ≤ G

Tactic:
exact ⟨Eq.ge, (G.le_sheafify J).antisymm⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ Presieve.IsSheaf J G.toPresheaf ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U

Tactic:
rw [← G.eq_sheafify_iff h]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
h : Presieve.IsSheaf J F
⊢ G = sheafify J G ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J (unop U) → s ∈ G.obj U
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem mk_eq_zero {g : R[X]} : mk f g = 0 ↔ f ∣ g :=
  mk_eq_mk.trans <| by rw [sub_zero]

Proof state:
R : Type u
inst✝ : CommRing R
f g : R[X]
⊢ f ∣ g - 0 ↔ f ∣ g

Tactic:
rw [sub_zero]

Result:
no goals
-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_le {m : ι} (ω : Ω) : hitting u s n m ω ≤ m

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
⊢ hitting u s n m ω ≤ m

Tactic:
simp only [hitting]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) ≤ m

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
⊢ (if ∃ j ∈ Set.Icc n m, u j ω ∈ s then sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) else m) ≤ m

Tactic:
split_ifs with h

Result:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ m

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ m

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h

Result:
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

Proof state:
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : u j ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

Tactic:
change j ∈ {i | u i ω ∈ s} at hj₂

Result:
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : j ∈ {i | u i ω ∈ s}
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

Proof state:
case pos.intro.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
j : ι
hj₁ : j ∈ Set.Icc n m
hj₂ : j ∈ {i | u i ω ∈ s}
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ m

Tactic:
exact (csInf_le (BddBelow.inter_of_left bddBelow_Icc) (Set.mem_inter hj₁ hj₂)).trans hj₁.2

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem isClopenable_iff_measurableSet
    [tγ : TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ] [BorelSpace γ] :
    IsClopenable s ↔ MeasurableSet s

Proof state:
case intro.intro.intro.intro
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed s
s_open : IsOpen s
⊢ MeasurableSet s

Tactic:
exact MeasurableSpace.measurableSet_generateFrom s_open

Result:
no goals

Proof state:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
⊢ IsClopenable s ↔ MeasurableSet s

Tactic:
refine ⟨fun hs => ?_, fun hs => hs.isClopenable⟩

Result:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : IsClopenable s
⊢ MeasurableSet s

Proof state:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝² : PolishSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
hs : IsClopenable s
⊢ MeasurableSet s

Tactic:
borelize γ

Result:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
hs : IsClopenable s
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
⊢ MeasurableSet s

Proof state:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
hs : IsClopenable s
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
⊢ MeasurableSet s

Tactic:
obtain ⟨t', t't, t'_polish, _, s_open⟩ :
  ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs

Result:
case intro.intro.intro.intro
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed s
s_open : IsOpen s
⊢ MeasurableSet s

Proof state:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed s
s_open : IsOpen s
⊢ PolishSpace γ

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.intro.intro.intro
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed s
s_open : IsOpen s
⊢ MeasurableSet s

Tactic:
rw [← borel_eq_borel_of_le t'_polish _ t't]

Result:
case intro.intro.intro.intro
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed s
s_open : IsOpen s
⊢ MeasurableSet s

γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst✝¹ : PolishSpace γ
inst✝ : BorelSpace γ
this✝ : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left✝ : IsClosed s
s_open : IsOpen s
⊢ PolishSpace γ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem negOne_eq_allOnes : -1#w = allOnes w

Proof state:
w : Nat
g : ¬w = 0
q : 1 < 2 ^ w
⊢ 2 ^ w - 1 < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
⊢ -1#w = allOnes w

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
⊢ (-1#w).toNat = (allOnes w).toNat

Proof state:
w : Nat
g : ¬w = 0
q : 1 < 2 ^ w
⊢ (-1#w).toNat = (allOnes w).toNat

Tactic:
have r : (2^w - 1) < 2^w := by omega

Result:
w : Nat
g : ¬w = 0
q : 1 < 2 ^ w
r : 2 ^ w - 1 < 2 ^ w
⊢ (-1#w).toNat = (allOnes w).toNat

Proof state:
case a
w : Nat
⊢ (-1#w).toNat = (allOnes w).toNat

Tactic:
if g : w = 0 then
  simp [g]
else
  have q : 1 < 2^w := by simp [g]
  have r : (2^w - 1) < 2^w := by omega
  simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]

Result:
no goals

Proof state:
w : Nat
g : ¬w = 0
⊢ (-1#w).toNat = (allOnes w).toNat

Tactic:
have q : 1 < 2^w := by simp [g]

Result:
w : Nat
g : ¬w = 0
q : 1 < 2 ^ w
⊢ (-1#w).toNat = (allOnes w).toNat

Proof state:
w : Nat
g : w = 0
⊢ (-1#w).toNat = (allOnes w).toNat

Tactic:
simp [g]

Result:
no goals

Proof state:
w : Nat
g : ¬w = 0
q : 1 < 2 ^ w
r : 2 ^ w - 1 < 2 ^ w
⊢ (-1#w).toNat = (allOnes w).toNat

Tactic:
simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]

Result:
no goals

Proof state:
w : Nat
g : ¬w = 0
⊢ 1 < 2 ^ w

Tactic:
simp [g]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma leadingCoeff_preHilbertPoly [CharZero F] (d k : ℕ) :
    (preHilbertPoly F d k).leadingCoeff = (d ! : F)⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).leadingCoeff = (↑d !)⁻¹

Tactic:
rw [leadingCoeff, natDegree_preHilbertPoly, coeff_preHilbertPoly_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_filterMap_some_eq_filter_map_isSome (f : α → Option β) (l : List α) :
    (l.filterMap f).map some = (l.map f).filter fun b => b.isSome

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ map some (filterMap f l) = filter (fun b => b.isSome) (map f l)

Tactic:
induction l <;> simp [filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : map some (filterMap f tail✝) = filter (fun b => b.isSome) (map f tail✝)
⊢ map some
      (match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) =
    filter (fun b => b.isSome) (f head✝ :: map f tail✝)

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : map some (filterMap f tail✝) = filter (fun b => b.isSome) (map f tail✝)
⊢ map some
      (match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) =
    filter (fun b => b.isSome) (f head✝ :: map f tail✝)

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem sum_take_map_length_splitWrtComposition (l : List α) (c : Composition l.length) (i : ℕ) :
    (((l.splitWrtComposition c).map length).take i).sum = c.sizeUpTo i

Proof state:
case e_a.e_a
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ map length (l.splitWrtComposition c) = c.blocks

Tactic:
exact map_length_splitWrtComposition l c

Result:
no goals

Proof state:
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ (take i (map length (l.splitWrtComposition c))).sum = c.sizeUpTo i

Tactic:
congr

Result:
case e_a.e_a
α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ map length (l.splitWrtComposition c) = c.blocks
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
lemma hasRightDerivedFunctor_iff :
    F.HasRightDerivedFunctor W ↔ HasLeftKanExtension L F

Proof state:
C : Type u_1
D : Type u_5
H : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_6, u_5} D
inst✝¹ : Category.{u_4, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F

Tactic:
rw [this, hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_5
H : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_6, u_5} D
inst✝¹ : Category.{u_4, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F

Tactic:
have : HasRightDerivedFunctor F W ↔ HasLeftKanExtension W.Q F :=
  ⟨fun h => h.hasLeftKanExtension', fun h => ⟨h⟩⟩

Result:
C : Type u_1
D : Type u_5
H : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_6, u_5} D
inst✝¹ : Category.{u_4, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shift_shift' (i j : A) :
    f⟦i⟧'⟦j⟧' = (shiftAdd X i j).inv ≫ f⟦i + j⟧' ≫ (shiftAdd Y i j).hom

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctorAdd C i j).inv.app X ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom =
    (shiftFunctor C i ⋙ shiftFunctor C j).map f

Tactic:
apply NatIso.naturality_1

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom =
    (shiftFunctor C j).map ((shiftFunctor C i).map f)

Tactic:
rw [← Functor.comp_map, NatIso.app_inv]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctorAdd C i j).inv.app X ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom =
    (shiftFunctor C i ⋙ shiftFunctor C j).map f

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom

Tactic:
symm

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftAdd X i j).inv ≫ (shiftFunctor C (i + j)).map f ≫ (shiftAdd Y i j).hom =
    (shiftFunctor C j).map ((shiftFunctor C i).map f)
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
/-- This holds true for all `x : ℂ` because of the junk values `0 / 0 = 0` and `log 0 = 0`. -/
@[simp] lemma log_div_self (x : ℂ) : log (x / x) = 0

Proof state:
x : ℂ
⊢ log (x / x) = 0

Tactic:
simp [log]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[simp] lemma shatters_shatterer : 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ 𝒜.shatterer.Shatters s ↔ 𝒜.Shatters s

Tactic:
simp_rw [← mem_shatterer, shatterer_idem]

Result:
no goals