harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/SeparatedMap.lean
theorem IsLocallyInjective.comp_right {f : X → Y} (hf : IsLocallyInjective f) {g : A → X}
    (cont : Continuous g) (hg : g.Injective) : IsLocallyInjective (f ∘ g)

Proof state:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsOpen (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
hg : Function.Injective g
⊢ IsOpen (Function.pullbackDiagonal (f ∘ g))

Tactic:
rw [← hg.preimage_pullbackDiagonal]

Result:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsOpen (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
hg : Function.Injective g
⊢ IsOpen (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)

Proof state:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsLocallyInjective f
g : A → X
cont : Continuous g
hg : Function.Injective g
⊢ IsLocallyInjective (f ∘ g)

Tactic:
rw [isLocallyInjective_iff_isOpen_diagonal] at hf ⊢

Result:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsOpen (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
hg : Function.Injective g
⊢ IsOpen (Function.pullbackDiagonal (f ∘ g))

Proof state:
X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
hf : IsOpen (Function.pullbackDiagonal f)
g : A → X
cont : Continuous g
hg : Function.Injective g
⊢ IsOpen (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)

Tactic:
apply hf.preimage (cont.mapPullback cont)

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem const_eq (a : α) : const a = a::const a

Proof state:
case a
α : Type u
a : α
⊢ ∀ (n : ℕ), (const a).get n = (a :: const a).get n

Tactic:
intro n

Result:
case a
α : Type u
a : α
n : ℕ
⊢ (const a).get n = (a :: const a).get n

Proof state:
α : Type u
a : α
⊢ const a = a :: const a

Tactic:
apply Stream'.ext

Result:
case a
α : Type u
a : α
⊢ ∀ (n : ℕ), (const a).get n = (a :: const a).get n

Proof state:
case a
α : Type u
a : α
n : ℕ
⊢ (const a).get n = (a :: const a).get n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
/-- If `f : X ⟶ Y` is a morphism of schemes with quasi-compact source and affine target, `f`
has a closed image and `f` induces an injection on global sections, then
`f` is surjective. -/
lemma surjective_of_isClosed_range_of_injective [CompactSpace X]
    (hfcl : IsClosed (Set.range f.base)) (hfinj : Function.Injective (f.appTop)) :
    Function.Surjective f.base

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
x : ↥⊤
h : (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (𝒰.map i).base) ↑x) ∉ Y.basicOpen s
⊢ (ConcreteCategory.hom ((𝒰.obj i).evaluation ⊤ ↑x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s)) =
    0

Tactic:
erw [← Scheme.Γevaluation_naturality_apply (𝒰.map i ≫ f)]

Result:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
x : ↥⊤
h : (ConcreteCategory.hom f.base) ((ConcreteCategory.hom (𝒰.map i).base) ↑x) ∉ Y.basicOpen s
⊢ (ConcreteCategory.hom (Scheme.Hom.residueFieldMap (𝒰.map i ≫ f) ↑x))
      ((ConcreteCategory.hom (Y.Γevaluation ((ConcreteCategory.hom (𝒰.map i ≫ f).base) ↑x))) s) =
    0

Proof state:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
⊢ (𝒰.obj i).basicOpen
      ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s)) =
    ⊥

Tactic:
rw [Scheme.basicOpen_eq_bot_iff_forall_evaluation_eq_zero]

Result:
case intro
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfcl : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
hfinj : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
I : Ideal ↑Γ(Y, ⊤)
hI : Set.range ⇑(ConcreteCategory.hom f.base) = Y.zeroLocus ↑I
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
s : ↑Γ(Y, ⊤)
hs : s ∈ ↑I
i : 𝒰.J
⊢ ∀ (x : ↥⊤),
    (ConcreteCategory.hom ((𝒰.obj i).evaluation ⊤ ↑x ⋯))
        ((ConcreteCategory.hom (Scheme.Hom.app (𝒰.map i) ⊤)) ((ConcreteCategory.hom (Scheme.Hom.appTop f)) s)) =
      0
-- Mathlib/Analysis/Convex/Star.lean
theorem starConvex_iUnion {ι : Sort*} {s : ι → Set E} (hs : ∀ i, StarConvex 𝕜 x (s i)) :
    StarConvex 𝕜 x (⋃ i, s i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : y ∈ ⋃ i, s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⋃ i, s i

Tactic:
rw [mem_iUnion] at hy ⊢

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ i, a • x + b • y ∈ s i

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hy : y ∈ s i
⊢ ∃ i, a • x + b • y ∈ s i

Tactic:
exact ⟨i, hs i hy ha hb hab⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ i, a • x + b • y ∈ s i

Tactic:
obtain ⟨i, hy⟩ := hy

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hy : y ∈ s i
⊢ ∃ i, a • x + b • y ∈ s i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
⊢ StarConvex 𝕜 x (⋃ i, s i)

Tactic:
rintro y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
ι : Sort u_4
s : ι → Set E
hs : ∀ (i : ι), StarConvex 𝕜 x (s i)
y : E
hy : y ∈ ⋃ i, s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⋃ i, s i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.erase [BEq α] [Hashable α] {m : Raw α β} {a : α} (h : m.WF) : (m.erase a).WF

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
h : m.WF
⊢ (m.erase a).WF

Tactic:
simpa [Raw.erase, h.size_buckets_pos] using .erase₀ h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem one_lt_rpow {x : ℝ≥0∞} {z : ℝ} (hx : 1 < x) (hz : 0 < z) : 1 < x ^ z

Proof state:
case top
z : ℝ
hz : 0 < z
hx : 1 < ⊤
⊢ 1 < ⊤ ^ z

Tactic:
simp [top_rpow_of_pos hz]

Result:
no goals

Proof state:
case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ 1 < ↑x✝ ^ z

Tactic:
simp only [some_eq_coe, one_lt_coe_iff] at hx

Result:
case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < x✝
⊢ 1 < ↑x✝ ^ z

Proof state:
case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < x✝
⊢ 1 < ↑x✝ ^ z

Tactic:
simp [← coe_rpow_of_nonneg _ (le_of_lt hz), NNReal.one_lt_rpow hx hz]

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
hx : 1 < x
hz : 0 < z
⊢ 1 < x ^ z

Tactic:
cases x

Result:
case top
z : ℝ
hz : 0 < z
hx : 1 < ⊤
⊢ 1 < ⊤ ^ z

case coe
z : ℝ
hz : 0 < z
x✝ : ℝ≥0
hx : 1 < ↑x✝
⊢ 1 < ↑x✝ ^ z
-- Mathlib/Order/Atoms.lean
theorem Set.Ici.isAtom_iff {b : Set.Ici a} : IsAtom b ↔ a ⋖ b

Proof state:
α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ IsAtom b ↔ a ⋖ ↑b

Tactic:
rw [← bot_covBy_iff]

Result:
α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ ⊥ ⋖ b ↔ a ⋖ ↑b

Proof state:
α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ (range ⇑(OrderEmbedding.subtype fun c => a ≤ c)).OrdConnected

Tactic:
simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Ici

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ ⊥ ⋖ b ↔ a ⋖ ↑b

Tactic:
refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm

Result:
α : Type u_2
inst✝ : PartialOrder α
a : α
b : ↑(Ici a)
⊢ (range ⇑(OrderEmbedding.subtype fun c => a ≤ c)).OrdConnected
-- Mathlib/Data/ZMod/IntUnitsPower.lean
@[norm_cast] lemma uzpow_natCast (u : ℤˣ) (n : ℕ) : u ^ (n : R) = u ^ n

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ u ^ ↑n = u ^ n

Tactic:
change ((n : R) • Additive.ofMul u).toMul = _

Result:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ Additive.toMul (↑n • Additive.ofMul u) = u ^ n

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ Additive.toMul (↑n • Additive.ofMul u) = u ^ n

Tactic:
rw [Nat.cast_smul_eq_nsmul, toMul_nsmul, toMul_ofMul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.toListModel_insertManyIfNewUnit_list [BEq α] [Hashable α] [EquivBEq α]
    [LawfulHashable α] {m : Raw₀ α (fun _ => Unit)} {l : List α} (h : Raw.WFImp m.1) :
    Perm (toListModel (Const.insertManyIfNewUnit m l).1.1.buckets)
      (List.insertListIfNewUnit (toListModel m.1.buckets) l)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => Unit
l : List α
h : Raw.WFImp m.val
⊢ toListModel (insertManyIfNewUnit m l).val.val.buckets ~ insertListIfNewUnit (toListModel m.val.buckets) l

Tactic:
rw [Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => Unit
l : List α
h : Raw.WFImp m.val
⊢ toListModel (insertListIfNewUnitₘ m l).val.buckets ~ insertListIfNewUnit (toListModel m.val.buckets) l

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => Unit
l : List α
h : Raw.WFImp m.val
⊢ toListModel (insertListIfNewUnitₘ m l).val.buckets ~ insertListIfNewUnit (toListModel m.val.buckets) l

Tactic:
apply toListModel_insertListIfNewUnitₘ h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
@[to_additive sub_nonneg_ae]
lemma one_le_div_ae {β : Type*} [Group β] [LE β] [MulRightMono β] (f g : α → β) :
    1 ≤ᵐ[μ] g / f ↔ f ≤ᵐ[μ] g

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
⊢ 1 ≤ᶠ[ae μ] g / f ↔ f ≤ᶠ[ae μ] g

Tactic:
refine ⟨fun h ↦ h.mono fun a ha ↦ ?_, fun h ↦ h.mono fun a ha ↦ ?_⟩

Result:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᶠ[ae μ] g / f
a : α
ha : 1 a ≤ (g / f) a
⊢ f a ≤ g a

case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᶠ[ae μ] g
a : α
ha : f a ≤ g a
⊢ 1 a ≤ (g / f) a

Proof state:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : f ≤ᶠ[ae μ] g
a : α
ha : f a ≤ g a
⊢ 1 a ≤ (g / f) a

Tactic:
rwa [Pi.one_apply, Pi.div_apply, one_le_div']

Result:
no goals

Proof state:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : Group β
inst✝¹ : LE β
inst✝ : MulRightMono β
f g : α → β
h : 1 ≤ᶠ[ae μ] g / f
a : α
ha : 1 a ≤ (g / f) a
⊢ f a ≤ g a

Tactic:
rwa [Pi.one_apply, Pi.div_apply, one_le_div'] at ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem intersperse_eq_intersperseTR : @intersperse = @intersperseTR

Proof state:
case h

⊢ ∀ (x : Type u_1), intersperse = intersperseTR

Tactic:
intro α

Result:
case h
α : Type u_1
⊢ intersperse = intersperseTR

Proof state:
case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l = intersperseTR sep l

Tactic:
simp [intersperseTR]

Result:
case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l =
    match l with
    | nil => nil
    | x :: nil => x :: nil
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) nil xs

Proof state:
⊢ @intersperse = @intersperseTR

Tactic:
apply funext

Result:
case h

⊢ ∀ (x : Type u_1), intersperse = intersperseTR

Proof state:
case h.h.h
α : Type u_1
sep : α
⊢ ∀ (x : List α), intersperse sep x = intersperseTR sep x

Tactic:
intro l

Result:
case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l = intersperseTR sep l

Proof state:
case h
α : Type u_1
⊢ intersperse = intersperseTR

Tactic:
apply funext

Result:
case h.h
α : Type u_1
⊢ ∀ (x : α), intersperse x = intersperseTR x

Proof state:
case h.h
α : Type u_1
sep : α
⊢ intersperse sep = intersperseTR sep

Tactic:
apply funext

Result:
case h.h.h
α : Type u_1
sep : α
⊢ ∀ (x : List α), intersperse sep x = intersperseTR sep x

Proof state:
case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l =
    match l with
    | nil => nil
    | x :: nil => x :: nil
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) nil xs

Tactic:
match l with
| [] | [_] => rfl
| x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*]

Result:
no goals

Proof state:
case h.h
α : Type u_1
⊢ ∀ (x : α), intersperse x = intersperseTR x

Tactic:
intro sep

Result:
case h.h
α : Type u_1
sep : α
⊢ intersperse sep = intersperseTR sep

Proof state:
α : Type u_1
sep : α
l : List α
x y : α
xs : List α
⊢ intersperse sep (x :: y :: xs) =
    match x :: y :: xs with
    | nil => nil
    | x :: nil => x :: nil
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) nil xs

Tactic:
simp [intersperse]

Result:
α : Type u_1
sep : α
l : List α
x y : α
xs : List α
⊢ intersperse sep (y :: xs) = y :: foldr (fun a r => sep :: a :: r) nil xs

Proof state:
α : Type u_1
sep : α
l : List α
head✝ : α
⊢ intersperse sep (head✝ :: nil) =
    match head✝ :: nil with
    | nil => nil
    | x :: nil => x :: nil
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) nil xs

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
sep : α
l : List α
x y : α
xs : List α
⊢ intersperse sep (y :: xs) = y :: foldr (fun a r => sep :: a :: r) nil xs

Tactic:
induction xs generalizing y <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem disjoint_take_drop : ∀ {l : List α}, l.Nodup → m ≤ n → Disjoint (l.take m) (l.drop n)
  | [], _, _ => by simp
  | x :: xs, hl, h => by
    cases m <;> cases n <;> simp only [disjoint_cons_left, drop, not_mem_nil, disjoint_nil_left,
      take, not_false_eq_true, and_self]
    · case succ.zero => cases h
    · cases hl with | cons h₀ h₁ =>
      refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩
      exact disjoint_take_drop h₁ (Nat.le_of_succ_le_succ h)

Proof state:
case succ.zero
α : Type u_1
x : α
xs : List α
hl : (x :: xs).Nodup
n✝ : Nat
h : n✝ + 1 ≤ 0
⊢ ¬x ∈ x :: xs ∧ (take n✝ xs).Disjoint (x :: xs)

Tactic:
case succ.zero => cases h

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
hl : (x :: xs).Nodup
n✝ : Nat
h : n✝ + 1 ≤ 0
⊢ ¬x ∈ x :: xs ∧ (take n✝ xs).Disjoint (x :: xs)

Tactic:
cases h

Result:
no goals

Proof state:
case succ.succ.cons
α : Type u_1
x : α
xs : List α
n✝¹ n✝ : Nat
h : n✝¹ + 1 ≤ n✝ + 1
h₁ : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ (take n✝¹ xs).Disjoint (drop n✝ xs)

Tactic:
exact disjoint_take_drop h₁ (Nat.le_of_succ_le_succ h)

Result:
no goals

Proof state:
case succ.succ
α : Type u_1
x : α
xs : List α
hl : (x :: xs).Nodup
n✝¹ n✝ : Nat
h : n✝¹ + 1 ≤ n✝ + 1
⊢ ¬x ∈ drop n✝ xs ∧ (take n✝¹ xs).Disjoint (drop n✝ xs)

Tactic:
cases hl with | cons h₀ h₁ =>
refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩
exact disjoint_take_drop h₁ (Nat.le_of_succ_le_succ h)

Result:
no goals

Proof state:
α : Type u_1
m n : Nat
x : α
xs : List α
hl : (x :: xs).Nodup
h : m ≤ n
⊢ (take m (x :: xs)).Disjoint (drop n (x :: xs))

Tactic:
cases m <;> cases n <;> simp only [disjoint_cons_left, drop, not_mem_nil, disjoint_nil_left,
  take, not_false_eq_true, and_self]

Result:
case succ.zero
α : Type u_1
x : α
xs : List α
hl : (x :: xs).Nodup
n✝ : Nat
h : n✝ + 1 ≤ 0
⊢ ¬x ∈ x :: xs ∧ (take n✝ xs).Disjoint (x :: xs)

case succ.succ
α : Type u_1
x : α
xs : List α
hl : (x :: xs).Nodup
n✝¹ n✝ : Nat
h : n✝¹ + 1 ≤ n✝ + 1
⊢ ¬x ∈ drop n✝ xs ∧ (take n✝¹ xs).Disjoint (drop n✝ xs)

Proof state:
case succ.succ.cons
α : Type u_1
x : α
xs : List α
n✝¹ n✝ : Nat
h : n✝¹ + 1 ≤ n✝ + 1
h₁ : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ ¬x ∈ drop n✝ xs ∧ (take n✝¹ xs).Disjoint (drop n✝ xs)

Tactic:
refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩

Result:
case succ.succ.cons
α : Type u_1
x : α
xs : List α
n✝¹ n✝ : Nat
h : n✝¹ + 1 ≤ n✝ + 1
h₁ : Pairwise (fun x1 x2 => x1 ≠ x2) xs
h₀ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ (take n✝¹ xs).Disjoint (drop n✝ xs)

Proof state:
α : Type u_1
m n : Nat
x✝¹ : [].Nodup
x✝ : m ≤ n
⊢ (take m []).Disjoint (drop n [])

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
/-- See `eLpNorm_smul_measure_of_ne_top'` for a version with scalar multiplication by `ℝ≥0∞`. -/
lemma eLpNorm_smul_measure_of_ne_top' (hp : p ≠ ∞) (c : ℝ≥0) (f : α → F) :
    eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ ⊤
c : ℝ≥0
f : α → F
this : 0 ≤ p.toReal⁻¹
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
refine (eLpNorm_smul_measure_of_ne_top hp ..).trans ?_

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ ⊤
c : ℝ≥0
f : α → F
this : 0 ≤ p.toReal⁻¹
⊢ ↑ENNReal.ofNNRealHom.toMonoidWithZeroHom c ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ ⊤
c : ℝ≥0
f : α → F
this : 0 ≤ p.toReal⁻¹
⊢ ↑ENNReal.ofNNRealHom.toMonoidWithZeroHom c ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
simp [ENNReal.smul_def, ENNReal.coe_rpow_of_nonneg, this]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ ⊤
c : ℝ≥0
f : α → F
⊢ 0 ≤ p.toReal⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ ⊤
c : ℝ≥0
f : α → F
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
have : 0 ≤ p.toReal⁻¹ := by positivity

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
hp : p ≠ ⊤
c : ℝ≥0
f : α → F
this : 0 ≤ p.toReal⁻¹
⊢ eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ
-- Mathlib/Order/Filter/Partial.lean
theorem ptendsto'_of_ptendsto {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} (h : f.Dom ∈ l₁) :
    PTendsto f l₁ l₂ → PTendsto' f l₁ l₂

Proof state:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.preimage s ∈ l₁

Tactic:
rw [PFun.preimage_eq]

Result:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.core s ∩ f.Dom ∈ l₁

Proof state:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
⊢ PTendsto f l₁ l₂ → PTendsto' f l₁ l₂

Tactic:
rw [ptendsto_def, ptendsto'_def]

Result:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
⊢ (∀ s ∈ l₂, f.core s ∈ l₁) → ∀ s ∈ l₂, f.preimage s ∈ l₁

Proof state:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
⊢ (∀ s ∈ l₂, f.core s ∈ l₁) → ∀ s ∈ l₂, f.preimage s ∈ l₁

Tactic:
intro h' s sl₂

Result:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.preimage s ∈ l₁

Proof state:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
h : f.Dom ∈ l₁
h' : ∀ s ∈ l₂, f.core s ∈ l₁
s : Set β
sl₂ : s ∈ l₂
⊢ f.core s ∩ f.Dom ∈ l₁

Tactic:
exact inter_mem (h' s sl₂) h

Result:
no goals
-- Mathlib/Analysis/Complex/Arg.lean
theorem sameRay_iff_arg_div_eq_zero : SameRay ℝ x y ↔ arg (x / y) = 0

Proof state:
case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
by_cases hy : y = 0

Result:
case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Proof state:
x y : ℂ
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
by_cases hx : x = 0

Result:
case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Proof state:
case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
simp [hx, hy, arg_div_coe_angle, sub_eq_zero]

Result:
no goals

Proof state:
case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
simp [hy]

Result:
no goals

Proof state:
x y : ℂ
⊢ SameRay ℝ x y ↔ (x / y).arg = 0

Tactic:
rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]

Result:
x y : ℂ
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
-- Mathlib/Logic/Encodable/Basic.lean
theorem decode_ofEquiv {α β} [Encodable α] (e : β ≃ α) (n : ℕ) :
    @decode _ (ofEquiv _ e) n = (decode n).map e.symm :=
  show Option.bind _ _ = Option.map _ _
  by rw [Option.map_eq_bind]

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Encodable α
e : β ≃ α
n : ℕ
⊢ (decode n).bind (some ∘ ⇑e.symm) = Option.map (⇑e.symm) (decode n)

Tactic:
rw [Option.map_eq_bind]

Result:
no goals