harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem hasBasis_coclosedLindelof :
    (Filter.coclosedLindelof X).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ (coclosedLindelof X).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl

Tactic:
simp only [Filter.coclosedLindelof, iInf_and']

Result:
X : Type u
inst✝ : TopologicalSpace X
⊢ (⨅ s, ⨅ (_ : IsClosed s ∧ IsLindelof s), 𝓟 sᶜ).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set X),
    IsClosed i ∧ IsLindelof i →
      ∀ (j : Set X), IsClosed j ∧ IsLindelof j → ∃ k, (IsClosed k ∧ IsLindelof k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ

Tactic:
rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs₁ : IsClosed s
hs₂ : IsLindelof s
t : Set X
ht₁ : IsClosed t
ht₂ : IsLindelof t
⊢ ∃ k, (IsClosed k ∧ IsLindelof k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs₁ : IsClosed s
hs₂ : IsLindelof s
t : Set X
ht₁ : IsClosed t
ht₂ : IsLindelof t
⊢ ∃ k, (IsClosed k ∧ IsLindelof k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ

Tactic:
exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
  compl_subset_compl.2 subset_union_right⟩⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ (⨅ s, ⨅ (_ : IsClosed s ∧ IsLindelof s), 𝓟 sᶜ).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl

Tactic:
refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isLindelof_empty⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set X),
    IsClosed i ∧ IsLindelof i →
      ∀ (j : Set X), IsClosed j ∧ IsLindelof j → ∃ k, (IsClosed k ∧ IsLindelof k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordCompl_of_not_prime (n p : ℕ) (hp : ¬p.Prime) : ordCompl[p] n = n

Proof state:
n p : ℕ
hp : ¬Prime p
⊢ n / p ^ n.factorization p = n

Tactic:
simp [factorization_eq_zero_of_non_prime n hp]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem finiteDimensional_of_det_ne_one {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M →ₗ[𝕜] M)
    (hf : LinearMap.det f ≠ 1) : FiniteDimensional 𝕜 M

Proof state:
case pos
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩

Result:
case pos.intro.intro
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
s : Finset M
hs : Basis { x // x ∈ s } 𝕜 M
⊢ FiniteDimensional 𝕜 M

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
⊢ FiniteDimensional 𝕜 M

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s 𝕜 M)

Result:
case pos
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M

case neg
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M

Proof state:
case neg
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M

Tactic:
simp [LinearMap.coe_det, H] at hf

Result:
no goals

Proof state:
case pos.intro.intro
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
s : Finset M
hs : Basis { x // x ∈ s } 𝕜 M
⊢ FiniteDimensional 𝕜 M

Tactic:
exact FiniteDimensional.of_fintype_basis hs

Result:
no goals

Proof state:
case neg
M : Type u_2
inst✝² : AddCommGroup M
𝕜 : Type u_7
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M

Tactic:
classical simp [LinearMap.coe_det, H] at hf

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem le_of_add_le_add_left (a b c : ℤ√d) (h : c + a ≤ c + b) : a ≤ b

Proof state:
d : ℕ
a b c : ℤ√↑d
h : c + a ≤ c + b
⊢ a ≤ b

Tactic:
simpa using Zsqrtd.add_le_add_left _ _ h (-c)

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div_self' (a b : G) : a / (a / b) = b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a / (a / b) = b

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem dist_sq_mul_dist_add_dist_sq_mul_dist (a b c p : P) (h : ∠ b p c = π) :
    dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p =
    dist b c * (dist a p ^ 2 + dist b p * dist c p)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    (dist b p + dist c p) * (dist a p ^ 2 + dist b p * dist c p)

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c p : P
h : ∠ b p c = π
⊢ dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p)

Tactic:
rw [pow_two, pow_two, law_cos a p b, law_cos a p c,
  eq_sub_of_add_eq (angle_add_angle_eq_pi_of_angle_eq_pi a h), Real.cos_pi_sub,
  dist_eq_add_dist_of_angle_eq_pi h]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c p : P
h : ∠ b p c = π
⊢ (dist a p * dist a p + dist b p * dist b p - 2 * dist a p * dist b p * -Real.cos (∠ a p c)) * dist c p +
      (dist a p * dist a p + dist c p * dist c p - 2 * dist a p * dist c p * Real.cos (∠ a p c)) * dist b p =
    (dist b p + dist c p) * (dist a p ^ 2 + dist b p * dist c p)
-- Mathlib/Data/Set/Image.lean
theorem image_comp (f : β → γ) (g : α → β) (a : Set α) : f ∘ g '' a = f '' (g '' a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
a : Set α
⊢ f ∘ g '' a = f '' (g '' a)

Tactic:
aesop

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem lift_card_iSup_le_sum_card {ι : Type u} [Small.{v} ι] (f : ι → Ordinal.{v}) :
    Cardinal.lift.{u} (⨆ i, f i).card ≤ Cardinal.sum fun i ↦ (f i).card

Proof state:
case mk.intro
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
i : ι
hi : x < f i
⊢ ∃ a, (fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩) a = ⟨x, hx⟩

Tactic:
exact ⟨⟨i, enumIsoToType _ ⟨x, hi⟩⟩, by simp⟩

Result:
no goals

Proof state:
case mk
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
⊢ ∃ a, (fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩) a = ⟨x, hx⟩

Tactic:
obtain ⟨i, hi⟩ := Ordinal.lt_iSup_iff.mp hx

Result:
case mk.intro
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
i : ι
hi : x < f i
⊢ ∃ a, (fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩) a = ⟨x, hx⟩

Proof state:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
i : ι
hi : x < f i
⊢ (fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩) ⟨i, (f i).enumIsoToType ⟨x, hi⟩⟩ = ⟨x, hx⟩

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
⊢ Surjective fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩

Tactic:
rintro ⟨x, hx⟩

Result:
case mk
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
⊢ ∃ a, (fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩) a = ⟨x, hx⟩

Proof state:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
⊢ Cardinal.lift.{u, v} #(⨆ i, f i).toType ≤ sum fun i => #(f i).toType

Tactic:
rw [← mk_sigma, ← Cardinal.lift_id'.{v} #(Σ _, _), ← Cardinal.lift_umax.{v, u}]

Result:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
⊢ Cardinal.lift.{max v u, v} #(⨆ i, f i).toType ≤ Cardinal.lift.{v, max v u} #((x : ι) × (f x).toType)

Proof state:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ sum fun i => (f i).card

Tactic:
simp_rw [← mk_toType]

Result:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
⊢ Cardinal.lift.{u, v} #(⨆ i, f i).toType ≤ sum fun i => #(f i).toType

Proof state:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
⊢ Surjective (⇑(⨆ i, f i).enumIsoToType ∘ fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩)

Tactic:
rw [EquivLike.comp_surjective]

Result:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Ordinal.{v}
⊢ Surjective fun x => ⟨↑((f x.fst).enumIsoToType.symm x.snd), ⋯⟩
-- Mathlib/GroupTheory/Nilpotent.lean
theorem upperCentralSeriesStep_eq_comap_center :
    upperCentralSeriesStep H = Subgroup.comap (mk' H) (center (G ⧸ H))

Proof state:
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ ∈ H ↔ ↑y * (mk' H) x✝ = (mk' H) x✝ * ↑y

Tactic:
rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem,
  div_eq_mul_inv, mul_inv_rev, mul_assoc]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ ∀ (x : G), ↑x * (mk' H) x✝ = (mk' H) x✝ * ↑x

Tactic:
apply forall_congr'

Result:
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ ∀ (a : G), x✝ * a * x✝⁻¹ * a⁻¹ ∈ H ↔ ↑a * (mk' H) x✝ = (mk' H) x✝ * ↑a

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ x✝ ∈ comap (mk' H) (center (G ⧸ H))

Tactic:
rw [mem_comap, mem_center_iff, forall_mk]

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ ∀ (x : G), ↑x * (mk' H) x✝ = (mk' H) x✝ * ↑x

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
⊢ upperCentralSeriesStep H = comap (mk' H) (center (G ⧸ H))

Tactic:
ext

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ x✝ ∈ comap (mk' H) (center (G ⧸ H))

Proof state:
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ : G
⊢ ∀ (a : G), x✝ * a * x✝⁻¹ * a⁻¹ ∈ H ↔ ↑a * (mk' H) x✝ = (mk' H) x✝ * ↑a

Tactic:
intro y

Result:
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ ∈ H ↔ ↑y * (mk' H) x✝ = (mk' H) x✝ * ↑y
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measure_ne_zero_iff_nonempty_of_isMulLeftInvariant [Regular μ] (hμ : μ ≠ 0) {s : Set G}
    (hs : IsOpen s) : μ s ≠ 0 ↔ s.Nonempty

Proof state:
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
hμ : μ ≠ 0
s : Set G
hs : IsOpen s
⊢ μ s ≠ 0 ↔ s.Nonempty

Tactic:
simpa [null_iff_of_isMulLeftInvariant (μ := μ) hs, hμ] using nonempty_iff_ne_empty.symm

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp]
lemma dens_sdiff_add_dens_inter (s t : Finset α) : dens (s \ t) + dens (s ∩ t) = dens s

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t).dens + (s ∩ t).dens = s.dens

Tactic:
rw [← dens_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

Result:
no goals
-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem Finsupp.toDFinsupp_single (i : ι) (m : M) :
    (Finsupp.single i m).toDFinsupp = DFinsupp.single i m

Proof state:
case h
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ (single i m).toDFinsupp i✝ = (DFinsupp.single i m) i✝

Tactic:
simp [Finsupp.single_apply, DFinsupp.single_apply]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
⊢ (single i m).toDFinsupp = DFinsupp.single i m

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ (single i m).toDFinsupp i✝ = (DFinsupp.single i m) i✝
-- Mathlib/Data/Finsupp/Single.lean
theorem single_injective (a : α) : Function.Injective (single a : M → α →₀ M) := fun b₁ b₂ eq => by
  have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ (single a b₁) a = (single a b₂) a

Tactic:
rw [eq]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : (single a b₁) a = (single a b₂) a
⊢ b₁ = b₂

Tactic:
rwa [single_eq_same, single_eq_same] at this

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
⊢ b₁ = b₂

Tactic:
have : (single a b₁ : α →₀ M) a = (single a b₂ : α →₀ M) a := by rw [eq]

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b₁ b₂ : M
eq : single a b₁ = single a b₂
this : (single a b₁) a = (single a b₂) a
⊢ b₁ = b₂
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem QInfty_idem : (QInfty : K[X] ⟶ _) ≫ QInfty = QInfty

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ QInfty ≫ QInfty = QInfty

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (QInfty ≫ QInfty).f n = QInfty.f n

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (QInfty ≫ QInfty).f n = QInfty.f n

Tactic:
exact QInfty_f_idem n

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_lintegral_eq_lintegral_restrict (f : α →ₛ ℝ≥0∞) {s : Set α}
    (hs : MeasurableSet s) : (restrict f s).lintegral μ = f.lintegral (μ.restrict s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (f.restrict s).lintegral μ = f.lintegral (μ.restrict s)

Tactic:
rw [f.restrict_lintegral hs, lintegral_restrict]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem _root_.Filter.EventuallyEq.mlieBracketWithin_vectorField'
    (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W) (ht : t ⊆ s) :
    mlieBracketWithin I V₁ W₁ t =ᶠ[𝓝[s] x] mlieBracketWithin I V W t

Proof state:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ mlieBracketWithin I V₁ W₁ t y = mlieBracketWithin I V W t y

Tactic:
apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq

Result:
case h.hV
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ =ᶠ[𝓝[t] y] V

case h.hxV
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ V₁ y = V y

case h.hW
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ =ᶠ[𝓝[t] y] W

case h.hxW
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s t : Set M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
y : M
hVy : V₁ y = V y
hWy : W₁ y = W y
hVy' : ∀ᶠ (x : M) in 𝓝[s] y, V₁ x = V x
hWy' : ∀ᶠ (x : M) in 𝓝[s] y, W₁ x = W x
⊢ W₁ y = W y
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.min {f g : δ → α} (hf : Measurable f) (hg : Measurable g) :
    Measurable fun a => min (f a) (g a)

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : SecondCountableTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable fun a => f a ⊓ g a

Tactic:
simpa only [min_def] using hf.piecewise (measurableSet_le hf hg) hg

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffAt_iff_contMDiffOn_nhds
    [IsManifold I n M] [IsManifold I' n M'] (hn : n ≠ ∞) :
    ContMDiffAt I I' n f x ↔ ∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
hn : n ≠ ∞
⊢ ContMDiffAt I I' n f x ↔ ∃ u ∈ 𝓝 x, ContMDiffOn I I' n f u

Tactic:
simp [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contMDiffOn_nhds hn, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem supDegree_eq_natDegree (p : R[X]) : p.toFinsupp.supDegree id = p.natDegree

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
apply WithBot.coe_injective

Result:
case inr.a
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ↑(AddMonoidAlgebra.supDegree id p.toFinsupp) = ↑p.natDegree

Proof state:
case inr.a
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.support.Nonempty

Tactic:
rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : Semiring R
⊢ AddMonoidAlgebra.supDegree id (toFinsupp 0) = natDegree 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Tactic:
obtain rfl|h := eq_or_ne p 0

Result:
case inl
R : Type u
inst✝ : Semiring R
⊢ AddMonoidAlgebra.supDegree id (toFinsupp 0) = natDegree 0

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ AddMonoidAlgebra.supDegree id p.toFinsupp = p.natDegree

Proof state:
case inr.a
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ ↑(AddMonoidAlgebra.supDegree id p.toFinsupp) = ↑p.natDegree

Tactic:
rw [← AddMonoidAlgebra.supDegree_withBot_some_comp, Function.comp_id, supDegree_eq_degree,
  degree_eq_natDegree h, Nat.cast_withBot]

Result:
case inr.a
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.toFinsupp.support.Nonempty
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_set_self (v : Vector α n) (i : Nat) (x : α) (hi : i < n) :
    (v.set i x hi)[i] = x

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
hi : i < n
⊢ (v.set i x hi)[i] = x

Tactic:
simp [getElem_set]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem coe_ofDigits (α : Type*) [Semiring α] (b : ℕ) (L : List ℕ) :
    ((ofDigits b L : ℕ) : α) = ofDigits (b : α) L

Proof state:
case nil
α : Type u_1
inst✝ : Semiring α
b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []

Tactic:
simp [ofDigits]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ↑(ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Tactic:
rw [ih]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Semiring α
b : ℕ
L : List ℕ
⊢ ↑(ofDigits b L) = ofDigits (↑b) L

Tactic:
induction' L with d L ih

Result:
case nil
α : Type u_1
inst✝ : Semiring α
b : ℕ
⊢ ↑(ofDigits b []) = ofDigits ↑b []

case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(ofDigits b (d :: L)) = ofDigits (↑b) (d :: L)

Proof state:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Tactic:
push_cast

Result:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑d + ↑b * ↑(ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L

Proof state:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(ofDigits b (d :: L)) = ofDigits (↑b) (d :: L)

Tactic:
dsimp [ofDigits]

Result:
case cons
α : Type u_1
inst✝ : Semiring α
b d : ℕ
L : List ℕ
ih : ↑(ofDigits b L) = ofDigits (↑b) L
⊢ ↑(d + b * ofDigits b L) = ↑d + ↑b * ofDigits (↑b) L
-- Mathlib/Tactic/Ring/Compare.lean
theorem le_congr {α : Type*} [LE α] {a b c d : α} (h1 : a = b) (h2 : b ≤ c) (h3 : d = c) :
    a ≤ d

Proof state:
α : Type u_1
inst✝ : LE α
a b c d : α
h1 : a = b
h2 : b ≤ c
h3 : d = c
⊢ a ≤ d

Tactic:
rwa [h1, h3]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_mul (a b c : Int) : (a - b) * c = a * c - b * c

Proof state:
a b c : Int
⊢ (a - b) * c = a * c - b * c

Tactic:
simp [Int.sub_eq_add_neg, Int.add_mul]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
theorem doubleFactorial_eq_prod_odd :
    ∀ n : ℕ, (2 * n + 1)‼ = ∏ i ∈ Finset.range n, (2 * (i + 1) + 1)
  | 0 => rfl
  | n + 1 => by
    rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
      (by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]
    rfl

Proof state:
n : ℕ
⊢ (2 * (n + 1) + 1)‼ = ∏ i ∈ Finset.range (n + 1), (2 * (i + 1) + 1)

Tactic:
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
  (by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]

Result:
n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼

Proof state:
n : ℕ
⊢ 2 * (n + 1) + 1 = 2 * n + 1 + 2

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼

Tactic:
rfl

Result:
no goals