harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/LocallyCompact.lean
theorem IsOpenQuotientMap.locallyCompactSpace [LocallyCompactSpace X] {f : X → Y}
    (hf : IsOpenQuotientMap f) : LocallyCompactSpace Y where
  local_compact_nhds

Proof state:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
K : Set X
hKx : K ∈ 𝓝 x
hKU : K ⊆ f ⁻¹' U
hKc : IsCompact K
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s

Tactic:
exact ⟨f '' K, hf.isOpenMap.image_mem_nhds hKx, image_subset_iff.2 hKU, hKc.image hf.continuous⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s

Tactic:
rcases local_compact_nhds (hf.continuous.continuousAt hU) with ⟨K, hKx, hKU, hKc⟩

Result:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
K : Set X
hKx : K ∈ 𝓝 x
hKU : K ⊆ f ⁻¹' U
hKc : IsCompact K
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∀ n ∈ 𝓝 x, ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s

Tactic:
refine hf.surjective.forall.2 fun x U hU ↦ ?_

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
U : Set Y
hU : U ∈ 𝓝 (f x)
⊢ ∃ s ∈ 𝓝 (f x), s ⊆ U ∧ IsCompact s
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.uniformContinuousOn_iff {f : α → β} {g : β → γ} {S : Set α}
    (hg : IsUniformInducing g) :
    UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S

Tactic:
dsimp only [UniformContinuousOn, Tendsto]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
S : Set α
hg : IsUniformInducing g
⊢ map (fun x => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔
    map (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ

Tactic:
rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_setOf_prime : schnirelmannDensity (setOf Nat.Prime) = 0 :=
  schnirelmannDensity_eq_zero_of_one_not_mem <| by simp [Nat.not_prime_one]

Proof state:
⊢ 1 ∉ setOf Nat.Prime

Tactic:
simp [Nat.not_prime_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_subset {t' : Finset ι} (ht : t ⊆ t') (h : ∀ i ∈ t', i ∉ t → w i = 0) :
    t.centerMass w z = t'.centerMass w z

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
i : ι
hit' : i ∈ t'
hit : i ∉ t
⊢ (∑ x ∈ t', w x)⁻¹ • w i • z i = 0

Tactic:
rw [h i hit' hit, zero_smul, smul_zero]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ t.centerMass w z = t'.centerMass w z

Tactic:
rw [centerMass, sum_subset ht h, smul_sum, centerMass, smul_sum]

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ ∑ x ∈ t, (∑ x ∈ t', w x)⁻¹ • w x • z x = ∑ x ∈ t', (∑ i ∈ t', w i)⁻¹ • w x • z x

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ ∀ x ∈ t', x ∉ t → (∑ x ∈ t', w x)⁻¹ • w x • z x = 0

Tactic:
intro i hit' hit

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
i : ι
hit' : i ∈ t'
hit : i ∉ t
⊢ (∑ x ∈ t', w x)⁻¹ • w i • z i = 0

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ ∑ x ∈ t, (∑ x ∈ t', w x)⁻¹ • w x • z x = ∑ x ∈ t', (∑ i ∈ t', w i)⁻¹ • w x • z x

Tactic:
apply sum_subset ht

Result:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
t' : Finset ι
ht : t ⊆ t'
h : ∀ i ∈ t', i ∉ t → w i = 0
⊢ ∀ x ∈ t', x ∉ t → (∑ x ∈ t', w x)⁻¹ • w x • z x = 0
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma inv_mul_le_one₀ (ha : 0 < a) : a⁻¹ * b ≤ 1 ↔ b ≤ a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 < a
⊢ a⁻¹ * b ≤ 1 ↔ b ≤ a

Tactic:
rw [inv_mul_le_iff₀ ha, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Strict.lean
theorem whiskerLeft_eqToHom {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g = h) :
    f ◁ eqToHom η = eqToHom (congr_arg₂ (· ≫ ·) rfl η)

Proof state:
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [whiskerLeft_id, eqToHom_refl]

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g = h
⊢ f ◁ eqToHom η = eqToHom ⋯

Tactic:
cases η

Result:
case refl
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ f ◁ eqToHom ⋯ = eqToHom ⋯
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_one : descPochhammer R 1 = X

Proof state:
R : Type u
inst✝ : Ring R
⊢ descPochhammer R 1 = X

Tactic:
simp [descPochhammer]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem res_injective : Injective (@res α)

Proof state:
α : Type u_2
x y : ℕ → α
h : res x = res y
⊢ x = y

Tactic:
ext n

Result:
case h
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ x n = y n

Proof state:
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ res x n.succ = res y n.succ

Tactic:
rw [h]

Result:
no goals

Proof state:
case h
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ x n = y n

Tactic:
apply res_eq_res.mp _ (Nat.lt_succ_self _)

Result:
α : Type u_2
x y : ℕ → α
h : res x = res y
n : ℕ
⊢ res x n.succ = res y n.succ

Proof state:
α : Type u_2
⊢ Injective res

Tactic:
intro x y h

Result:
α : Type u_2
x y : ℕ → α
h : res x = res y
⊢ x = y
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_add_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.tan (o.oangle x (x + y)) = ‖y‖ / ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).tan = ‖y‖ / ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/Data/Multiset/Interval.lean
theorem card_Ioc :
    #(Finset.Ioc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) - 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Ioc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 1

Tactic:
rw [Finset.card_Ioc_eq_card_Icc_sub_one, card_Icc]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_eq_iff_eq_image {f : α → β} (hf : Bijective f) {s t} :
    f ⁻¹' s = t ↔ s = f '' t

Proof state:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ f ⁻¹' s = t ↔ s = f '' t

Tactic:
rw [← image_eq_image hf.1, hf.2.image_preimage]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem subset_symm_image {α β} (e : α ≃ β) (s : Set α) (t : Set β) :
    s ⊆ e.symm '' t ↔ e '' s ⊆ t :=
  calc
    s ⊆ e.symm '' t ↔ e.symm.symm '' s ⊆ t

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ s ⊆ ⇑e.symm '' t ↔ ⇑e.symm.symm '' s ⊆ t

Tactic:
rw [e.symm.symm_image_subset]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ ⇑e.symm.symm '' s ⊆ t ↔ ⇑e '' s ⊆ t

Tactic:
rw [e.symm_symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_append {l₁ l₂ : List (α × β)} {k : α} :
    (l₁ ++ l₂).lookup k = (l₁.lookup k).or (l₂.lookup k)

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l₁ l₂ : List (α × β)
k : α
⊢ lookup k (l₁ ++ l₂) = (lookup k l₁).or (lookup k l₂)

Tactic:
simp [lookup_eq_findSome?, findSome?_append]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem smul_stdBasisMatrix [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) :
    r • stdBasisMatrix i j a = stdBasisMatrix i j (r • a)

Proof state:
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
⊢ (r • of fun i' j' => if i = i' ∧ j = j' then a else 0) = of fun i' j' => if i = i' ∧ j = j' then r • a else 0

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
i✝ : m
j✝ : n
⊢ (r • of fun i' j' => if i = i' ∧ j = j' then a else 0) i✝ j✝ =
    of (fun i' j' => if i = i' ∧ j = j' then r • a else 0) i✝ j✝

Proof state:
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
⊢ r • stdBasisMatrix i j a = stdBasisMatrix i j (r • a)

Tactic:
unfold stdBasisMatrix

Result:
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
⊢ (r • of fun i' j' => if i = i' ∧ j = j' then a else 0) = of fun i' j' => if i = i' ∧ j = j' then r • a else 0

Proof state:
case a
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
i✝ : m
j✝ : n
⊢ (r • of fun i' j' => if i = i' ∧ j = j' then a else 0) i✝ j✝ =
    of (fun i' j' => if i = i' ∧ j = j' then r • a else 0) i✝ j✝

Tactic:
simp [smul_ite]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
lemma Measure.AbsolutelyContinuous.trim {ν : Measure α} (hμν : μ ≪ ν) (hm : m ≤ m0) :
    μ.trim hm ≪ ν.trim hm

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : ν s = 0
⊢ μ s = 0

Tactic:
exact hμν hsν

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
⊢ μ.trim hm ≪ ν.trim hm

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun s hs hsν ↦ ?_)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : (ν.trim hm) s = 0
⊢ (μ.trim hm) s = 0

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : (ν.trim hm) s = 0
⊢ (μ.trim hm) s = 0

Tactic:
rw [trim_measurableSet_eq hm hs] at hsν ⊢

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : ν s = 0
⊢ μ s = 0
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem one_smul' {Γ} [OrderedAddCommMonoid Γ] [AddAction Γ Γ'] [IsOrderedCancelVAdd Γ Γ']
    [MonoidWithZero R] [MulActionWithZero R V] {x : HahnModule Γ' R V} :
    (1 : HahnSeries Γ R) • x = x

Proof state:
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
x : HahnModule Γ' R V
⊢ 1 • x = x

Tactic:
ext g

Result:
case h.h
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
x : HahnModule Γ' R V
g : Γ'
⊢ ((of R).symm (1 • x)).coeff g = ((of R).symm x).coeff g

Proof state:
case h.h
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁶ : PartialOrder Γ'
inst✝⁵ : AddCommMonoid V
Γ : Type u_6
inst✝⁴ : OrderedAddCommMonoid Γ
inst✝³ : AddAction Γ Γ'
inst✝² : IsOrderedCancelVAdd Γ Γ'
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
x : HahnModule Γ' R V
g : Γ'
⊢ ((of R).symm (1 • x)).coeff g = ((of R).symm x).coeff g

Tactic:
exact coeff_single_zero_smul.trans (one_smul R (x.coeff g))

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem transfer_self : p.transfer G p.edges_subset_edgeSet = p

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.transfer G ⋯ = p

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_map (f : α → β) (l : List α) (w) :
    (map f l).head w = f (l.head (by simpa using w))

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
w : map f (head✝ :: tail✝) ≠ []
⊢ (map f (head✝ :: tail✝)).head w = f ((head✝ :: tail✝).head ⋯)

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
w : map f l ≠ []
⊢ (map f l).head w = f (l.head ⋯)

Tactic:
cases l

Result:
case nil
α : Type u_1
β : Type u_2
f : α → β
w : map f [] ≠ []
⊢ (map f []).head w = f ([].head ⋯)

case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
w : map f (head✝ :: tail✝) ≠ []
⊢ (map f (head✝ :: tail✝)).head w = f ((head✝ :: tail✝).head ⋯)

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
w : map f [] ≠ []
⊢ (map f []).head w = f ([].head ⋯)

Tactic:
simp at w

Result:
no goals

Proof state:
α : Type ?u.131653
β : Type ?u.131660
f : α → β
l : List α
w : map f l ≠ []
⊢ l ≠ []

Tactic:
simpa using w

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem lt_iterate_pos_iff {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) :
    x + n * m < f^[n] x ↔ x + m < f x

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x

Tactic:
simpa only [not_le] using not_congr (f.iterate_pos_le_iff hn)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_eq_max' {a b : Cardinal} (ha : ℵ₀ ≤ b) : a + b = max a b

Proof state:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
⊢ a + b = a ⊔ b

Tactic:
rw [add_comm, max_comm, add_eq_max ha]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem nhds_eq_uniformity_prod {a b : α} :
    𝓝 (a, b) =
      (𝓤 α).lift' fun s : Set (α × α) => { y : α | (y, a) ∈ s } ×ˢ { y : α | (b, y) ∈ s }

Proof state:
case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone fun s => {y | (y, a) ∈ s}

Tactic:
exact monotone_preimage (f := fun y => (y, a))

Result:
no goals

Proof state:
case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
refine fun t => Monotone.set_prod ?_ monotone_const

Result:
case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
t : Set (α × α)
⊢ Monotone fun s => {y | (y, a) ∈ s}

Proof state:
case hg₁
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)), Monotone fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

Tactic:
exact fun s => monotone_const.set_prod monotone_preimage

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ 𝓝 (a, b) = (𝓤 α).lift' fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}

Tactic:
rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']

Result:
case hg₁
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (s : Set (α × α)), Monotone fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}

case hg₂
α : Type ua
inst✝ : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)), Monotone fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_eq_mapFinIdx {l : Vector α n} {f : Nat → α → β} :
    l.mapIdx f = l.mapFinIdx (fun i a _ => f i a)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : Nat → α → β
⊢ mapIdx f l = l.mapFinIdx fun i a x => f i a

Tactic:
simp [mapFinIdx_eq_mapIdx]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem le_himp_iff_left : a ≤ a ⇨ b ↔ a ≤ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ a ⇨ b ↔ a ≤ b

Tactic:
rw [le_himp_iff, inf_idem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
    {v : β k} :
    (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true

Tactic:
simp_to_raw using Raw₀.contains_of_contains_insertIfNew'

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem ae_eq_bot : ae μ = ⊥ ↔ μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ae μ = ⊥ ↔ μ = 0

Tactic:
rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_zero_ite (R) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R]
    (k : ℕ) : choose (0 : R) k = if k = 0 then 1 else 0

Proof state:
case neg
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : ¬k = 0
⊢ choose 0 k = 0

Tactic:
rw [choose_zero_pos R <| Nat.pos_of_ne_zero hk]

Result:
no goals

Proof state:
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ choose 0 k = if k = 0 then 1 else 0

Tactic:
split_ifs with hk

Result:
case pos
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : k = 0
⊢ choose 0 k = 1

case neg
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : ¬k = 0
⊢ choose 0 k = 0

Proof state:
case pos
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
hk : k = 0
⊢ choose 0 k = 1

Tactic:
rw [hk, choose_zero_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_bin : eval assign (.bin lhs op rhs) = op.eval (lhs.eval assign) (rhs.eval assign)

Proof state:
assign : BVExpr.Assignment
a✝ : Nat
lhs : BVExpr a✝
op : BVBinPred
rhs : BVExpr a✝
⊢ eval assign (bin lhs op rhs) = op.eval (BVExpr.eval assign lhs) (BVExpr.eval assign rhs)

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma start_mem_verts_toSubgraph (p : G.Walk u v) : u ∈ p.toSubgraph.verts

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.toSubgraph.verts

Tactic:
simp [mem_verts_toSubgraph]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma iCycles_d : K.iCycles i ≫ K.d i j = 0

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : c.Rel i j
⊢ K.iCycles i ≫ K.d i j = 0

Tactic:
obtain rfl := c.next_eq' hij

Result:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ K.iCycles i ≫ K.d i (c.next i) = 0

Proof state:
case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ K.iCycles i ≫ K.d i j = 0

Tactic:
rw [K.shape _ _ hij, comp_zero]

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
hij : c.Rel i (c.next i)
⊢ K.iCycles i ≫ K.d i (c.next i) = 0

Tactic:
exact (K.sc i).iCycles_g

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
⊢ K.iCycles i ≫ K.d i j = 0

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : c.Rel i j
⊢ K.iCycles i ≫ K.d i j = 0

case neg
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : ¬c.Rel i j
⊢ K.iCycles i ≫ K.d i j = 0
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem annihilator_bot : (⊥ : Submodule R M).annihilator = ⊤ :=
  top_le_iff.mp fun _ _ ↦ mem_annihilator.mpr fun _ ↦ by rintro rfl; rw [smul_zero]

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² : R
x✝¹ : x✝² ∈ ⊤
x✝ : M
⊢ x✝ ∈ ⊥ → x✝² • x✝ = 0

Tactic:
rintro rfl

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : R
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ • 0 = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : R
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ • 0 = 0

Tactic:
rw [smul_zero]

Result:
no goals