harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem denseRange_coe [NoncompactSpace X] : DenseRange ((↑) : X → OnePoint X)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ Dense {∞}ᶜ

Tactic:
exact dense_compl_singleton _

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ DenseRange some

Tactic:
rw [DenseRange, ← compl_infty]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NoncompactSpace X
⊢ Dense {∞}ᶜ
-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem Matrix.finite_spectrum (A : Matrix n n R) : Set.Finite (spectrum R A)

Proof state:
n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R A).Finite

Tactic:
rw [← AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv <| Pi.basisFun R n) A]

Result:
n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R ((toLinAlgEquiv (Pi.basisFun R n)) A)).Finite

Proof state:
n : Type u_1
R : Type u_2
inst✝² : Field R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
⊢ (spectrum R ((toLinAlgEquiv (Pi.basisFun R n)) A)).Finite

Tactic:
exact Module.End.finite_spectrum _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_Iio_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) :
    f.measure (Iio x) = ∞

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
⊢ f.measure (Iic (x - 1)) ≤ f.measure (Iio x)

Tactic:
exact measure_mono <| Set.Iic_subset_Iio.mpr <| sub_one_lt x

Result:
no goals

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
⊢ f.measure (Iio x) = ⊤

Tactic:
rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf (x - 1)]

Result:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
⊢ f.measure (Iic (x - 1)) ≤ f.measure (Iio x)
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_diff_Iio : Ico a b \ Iio c = Ico (max a c) b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ico a b \ Iio c = Ico (a ⊔ c) b

Tactic:
rw [diff_eq, compl_Iio, Ico_inter_Ici]

Result:
no goals
-- Mathlib/Logic/ExistsUnique.lean
theorem existsUnique_eq' {a' : α} : ∃! a, a' = a

Proof state:
α : Sort u_1
a' : α
⊢ ∃! a, a' = a

Tactic:
simp only [ExistsUnique, and_self, forall_eq', exists_eq']

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem univ_sum_single [Fintype α] [AddCommMonoid M] (f : α →₀ M) :
    ∑ a : α, single a (f a) = f

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ ∑ a : α, single a (f a) = f

Tactic:
classical
refine DFunLike.coe_injective ?_
simp_rw [coe_finset_sum, single_eq_pi_single, Finset.univ_sum_single]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ (fun f => ⇑f) (∑ a : α, single a (f a)) = (fun f => ⇑f) f

Tactic:
simp_rw [coe_finset_sum, single_eq_pi_single, Finset.univ_sum_single]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ ∑ a : α, single a (f a) = f

Tactic:
refine DFunLike.coe_injective ?_

Result:
α : Type u_1
M : Type u_8
inst✝¹ : Fintype α
inst✝ : AddCommMonoid M
f : α →₀ M
⊢ (fun f => ⇑f) (∑ a : α, single a (f a)) = (fun f => ⇑f) f
-- Mathlib/Order/Monotone/Union.lean
theorem MonotoneOn.Iic_union_Ici (h₁ : MonotoneOn f (Iic a)) (h₂ : MonotoneOn f (Ici a)) :
    Monotone f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)

Tactic:
exact MonotoneOn.union_right h₁ h₂ isGreatest_Iic isLeast_Ici

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ Monotone f

Tactic:
rw [← monotoneOn_univ, ← @Iic_union_Ici _ _ a]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : MonotoneOn f (Iic a)
h₂ : MonotoneOn f (Ici a)
⊢ MonotoneOn f (Iic a ∪ Ici a)
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma freeDesc_apply {X : Type u} {M : ModuleCat.{u} R} (f : X ⟶ M) (x : X) :
    freeDesc f (freeMk x) = f x

Proof state:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ (ConcreteCategory.hom (freeDesc f)) (freeMk x) = f x

Tactic:
dsimp [freeDesc]

Result:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ ((Finsupp.lift (↑M) R X) f) (freeMk x) = f x

Proof state:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 0 • f x = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ ((Finsupp.lift (↑M) R X) f) (freeMk x) = f x

Tactic:
erw [Finsupp.lift_apply, Finsupp.sum_single_index]

Result:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 1 • f x = f x

R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 0 • f x = 0

Proof state:
R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 1 • f x = f x

R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ 0 • f x = 0

Tactic:
all_goals simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem exists_circumsphere_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V]
    (hd : finrank ℝ V = n) (hc : Cospherical ps) :
    ∃ c : Sphere P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumsphere = c

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
refine exists_circumsphere_eq_of_cospherical_subset ?_ hd hc

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ps ⊆ ↑⊤

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ps ⊆ ↑⊤

Tactic:
exact Set.subset_univ _

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
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
haveI : Nonempty (⊤ : AffineSubspace ℝ P) := Set.univ.nonempty

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
rw [← finrank_top, ← direction_top ℝ V P] at hd

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
-- Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean
theorem mulMap'_surjective : Function.Surjective (mulMap' A B)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
⊢ Function.Surjective ⇑(A.mulMap' B)

Tactic:
simp_rw [mulMap', AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe,
  EquivLike.comp_surjective, AlgHom.rangeRestrict_surjective]

Result:
no goals
-- Mathlib/Geometry/Group/Growth/LinearLowerBound.lean
/-- The growth of a set generating an infinite group is at least linear. -/
@[to_additive "The growth of a set generating an infinite group is at least linear."]
lemma add_one_le_card_pow (hX₁ : 1 ∈ X) (hXclosure : (closure (X : Set G) : Set G).Infinite) :
    ∀ n, n + 1 ≤ #(X ^ n)
  | 0 => by simp
  | n + 1 => (add_one_le_card_pow hX₁ hXclosure _).trans_lt <| card_lt_card <|
      pow_right_strictMono hX₁ (by simp [hXclosure, Set.infinite_univ]) n.lt_succ_self

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
⊢ 0 + 1 ≤ #(X ^ 0)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hXclosure : (↑(closure ↑X)).Infinite
n : ℕ
⊢ (↑(closure ↑X)).Infinite

Tactic:
simp [hXclosure, Set.infinite_univ]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem single_finset_sum [AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α) :
    single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

Proof state:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a ∘ fun b => f b) s.val).sum = ∑ b ∈ s, single a (f b)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ?m.46011

Tactic:
apply single_multiset_sum

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b)

Tactic:
trans

Result:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ single a (∑ b ∈ s, f b) = ?m.46011

α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ ?m.46011 = ∑ b ∈ s, single a (f b)

α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ α →₀ M

Proof state:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a) (Multiset.map (fun b => f b) s.val)).sum = ∑ b ∈ s, single a (f b)

Tactic:
rw [Multiset.map_map]

Result:
α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a ∘ fun b => f b) s.val).sum = ∑ b ∈ s, single a (f b)
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_sq_sub_sinh_sq (x : ℝ) : cosh x ^ 2 - sinh x ^ 2 = 1

Proof state:
x : ℝ
⊢ cosh x ^ 2 - sinh x ^ 2 = 1

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(cosh x ^ 2 - sinh x ^ 2) = ↑1

Proof state:
x : ℝ
⊢ ↑(cosh x ^ 2 - sinh x ^ 2) = ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
lemma small : Small.{v} X

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v + 1, u} (Cardinal.mk X) < Cardinal.lift.{max u (v + 1), v} κ
⊢ Small.{v, u} X

Tactic:
simpa only [Cardinal.small_iff_lift_mk_lt_univ] using h.trans (Cardinal.lift_lt_univ' κ)

Result:
no goals

Proof state:
X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
⊢ Small.{v, u} X

Tactic:
dsimp [HasCardinalLT] at h

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
⊢ Small.{v, u} X

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
⊢ Small.{v, u} X

Tactic:
rw [← Cardinal.lift_lt.{_, v + 1}, Cardinal.lift_lift, Cardinal.lift_lift] at h

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v + 1, u} (Cardinal.mk X) < Cardinal.lift.{max u (v + 1), v} κ
⊢ Small.{v, u} X
-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
@[simp]
lemma norm_coe_unit (u : 𝒪[K]ˣ) : ‖((u : 𝒪[K]) : K)‖ = 1

Proof state:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
u : (↥𝒪[K])ˣ
⊢ ‖↑↑u‖ = 1

Tactic:
simpa [← NNReal.coe_inj] using
  (Valuation.integer.integers (NormedField.valuation (K := K))).valuation_unit u

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma measurableSet_generateFrom_memPartition (t : ℕ → Set α) (n : ℕ) :
    MeasurableSet[generateFrom (memPartition t (n + 1))] (t n)

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet (t n)

Tactic:
rw [this]

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet (⋃ u ∈ memPartition t n, u ∩ t n)

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}

Tactic:
exact ⟨v, hv, Or.inl rfl⟩

Result:
no goals

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet (⋃ u ∈ memPartition t n, u ∩ t n)

Tactic:
refine MeasurableSet.biUnion (finite_memPartition _ _).countable (fun v hv ↦ ?_)

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v ∩ t n)

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ MeasurableSet (t n)

Tactic:
have : t n = ⋃ u ∈ memPartition t n, u ∩ t n := by
  simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
⊢ MeasurableSet (t n)

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
⊢ t n = ⋃ u ∈ memPartition t n, u ∩ t n

Tactic:
simp_rw [← iUnion_inter, ← sUnion_eq_biUnion, sUnion_memPartition, univ_inter]

Result:
no goals

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ memPartition t (n + 1)

Tactic:
rw [memPartition_succ]

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ {s | ∃ u ∈ memPartition t n, s = u ∩ t n ∨ s = u \ t n}

Proof state:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ MeasurableSet (v ∩ t n)

Tactic:
refine measurableSet_generateFrom ?_

Result:
α : Type u_1
t : ℕ → Set α
n : ℕ
this : t n = ⋃ u ∈ memPartition t n, u ∩ t n
v : Set α
hv : v ∈ memPartition t n
⊢ v ∩ t n ∈ memPartition t (n + 1)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_dblX (P : Fin 3 → A) : (W'.baseChange B).toJacobian.dblX (f ∘ P) =
    f ((W'.baseChange A).toJacobian.dblX P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.dblX (⇑f ∘ P) = f ((baseChange W' A).toJacobian.dblX P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblX, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_leadingCoeff (hkm : k < m) (hmn : m < n) (hw : w ≠ 0) :
    (trinomial k m n u v w).leadingCoeff = w

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hw : w ≠ 0
⊢ (trinomial k m n u v w).leadingCoeff = w

Tactic:
rw [leadingCoeff, trinomial_natDegree hkm hmn hw, trinomial_leading_coeff' hkm hmn]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Complex.lean
theorem isPrimitiveRoot_exp (n : ℕ) (h0 : n ≠ 0) : IsPrimitiveRoot (exp (2 * π * I / n)) n

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n)) n

Tactic:
simpa only [Nat.cast_one, one_div] using
  isPrimitiveRoot_exp_of_coprime 1 n h0 n.coprime_one_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_push_of_pos {p : α → Bool} {a : α} {l : Array α}
    (h : p a) (w : stop = l.size + 1):
    (l.push a).filter p 0 stop = (l.filter p).push a

Proof state:
α : Type u_1
stop : Nat
p : α → Bool
a : α
l : Array α
h : p a = true
w : stop = l.size + 1
⊢ filter p (l.push a) 0 stop = (filter p l).push a

Tactic:
subst w

Result:
α : Type u_1
p : α → Bool
a : α
l : Array α
h : p a = true
⊢ filter p (l.push a) 0 (l.size + 1) = (filter p l).push a

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
h : p a = true
l : List α
⊢ filter p ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = (filter p { toList := l }).push a

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
h : p a = true
⊢ filter p (l.push a) 0 (l.size + 1) = (filter p l).push a

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
h : p a = true
l : List α
⊢ filter p ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = (filter p { toList := l }).push a
-- Mathlib/Computability/PostTuringMachine.lean
theorem reaches₁_fwd {σ} {f : σ → Option σ} {a b c} (h₁ : Reaches₁ f a c) (h₂ : b ∈ f a) :
    Reaches f b c

Proof state:
case intro.intro
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b' c
⊢ Reaches f b c

Tactic:
cases Option.mem_unique hab h₂

Result:
case intro.intro.refl
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b c
⊢ Reaches f b c

Proof state:
case intro.intro.refl
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ hab : b ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b c
⊢ Reaches f b c

Tactic:
exact hbc

Result:
no goals

Proof state:
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
⊢ Reaches f b c

Tactic:
rcases TransGen.head'_iff.1 h₁ with ⟨b', hab, hbc⟩

Result:
case intro.intro
σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
b' : σ
hab : b' ∈ f a
hbc : ReflTransGen (fun a b => b ∈ f a) b' c
⊢ Reaches f b c
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signAux_swap_zero_one {n : ℕ} (hn : 2 ≤ n) :
    signAux (swap (⟨0, lt_of_lt_of_le (by decide) hn⟩ : Fin n) ⟨1, lt_of_lt_of_le (by decide) hn⟩) =
      -1

Proof state:
n : ℕ
hn : 2 ≤ n
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
rcases n with (_ | _ | n)

Result:
case zero
hn : 2 ≤ 0
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

case succ.zero
hn : 2 ≤ 0 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

case succ.succ
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Proof state:
α : Type u
inst✝ : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ 1 < 2

Tactic:
decide

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
β : Type v
n : ℕ
hn : 2 ≤ n
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
case succ.succ
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
exact signAux_swap_zero_one' n

Result:
no goals

Proof state:
case zero
hn : 2 ≤ 0
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
norm_num at hn

Result:
no goals

Proof state:
case succ.zero
hn : 2 ≤ 0 + 1
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
norm_num at hn

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem orthogonalComplement_iSup_eigenspaces_eq_bot' (hT : T.IsSymmetric) :
    (⨆ μ : Eigenvalues T, eigenspace T μ)ᗮ = ⊥ :=
  show (⨆ μ : { μ // eigenspace T μ ≠ ⊥ }, eigenspace T μ)ᗮ = ⊥ by
    rw [iSup_ne_bot_subtype, hT.orthogonalComplement_iSup_eigenspaces_eq_bot]

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
inst✝ : FiniteDimensional 𝕜 E
hT : T.IsSymmetric
⊢ (⨆ μ, eigenspace T ↑μ)ᗮ = ⊥

Tactic:
rw [iSup_ne_bot_subtype, hT.orthogonalComplement_iSup_eigenspaces_eq_bot]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem keys_insert {a} {b : β a} (s : AList β) : (insert a b s).keys = a :: s.keys.erase a

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ (insert a b s).keys = a :: s.keys.erase a

Tactic:
simp [insert, keys, keys_kerase]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_eq_coe_toFinset_card (s : Set α) [Fintype s] : encard s = s.toFinset.card

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.encard = ↑s.toFinset.card

Tactic:
have h := toFinite s

Result:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.encard = ↑s.toFinset.card

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ s.encard = ↑s.toFinset.card

Tactic:
rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]

Result:
no goals
-- Mathlib/Topology/Sets/Opens.lean
lemma IsBasis.le_iff {α} {t₁ t₂ : TopologicalSpace α}
    {Us : Set (Opens α)} (hUs : @IsBasis α t₂ Us) :
    t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen[t₁] U

Proof state:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
⊢ t₁ ≤ generateFrom (SetLike.coe '' Us) ↔ ∀ U ∈ Us, IsOpen ↑U

Tactic:
simp [Set.subset_def, le_generateFrom_iff_subset_isOpen]

Result:
no goals

Proof state:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
⊢ t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen ↑U

Tactic:
conv_lhs => rw [hUs.eq_generateFrom]

Result:
α : Type u_5
t₁ t₂ : TopologicalSpace α
Us : Set (Opens α)
hUs : IsBasis Us
⊢ t₁ ≤ generateFrom (SetLike.coe '' Us) ↔ ∀ U ∈ Us, IsOpen ↑U
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
protected lemma connected_iff {H : G.Subgraph} :
    H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty

Tactic:
rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_self (m : Nat) : lcm m m = m

Proof state:
m : Nat
h : m = 0
⊢ m.lcm m = m

Tactic:
rw [h, lcm_zero_left]

Result:
no goals

Proof state:
m : Nat
⊢ m.lcm m = m

Tactic:
match eq_zero_or_pos m with
| .inl h => rw [h, lcm_zero_left]
| .inr h => simp [lcm, Nat.mul_div_cancel _ h]

Result:
no goals

Proof state:
m : Nat
h : m > 0
⊢ m.lcm m = m

Tactic:
simp [lcm, Nat.mul_div_cancel _ h]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_iInf_principal_finite {ι : Type*} (s : ι → Set α) :
    (⨅ i, 𝓟 (s i)).HasBasis (fun t : Set ι => t.Finite) fun t => ⋂ i ∈ t, s i

Proof state:
α : Type u_1
ι : Type u_6
s : ι → Set α
⊢ (⨅ i, 𝓟 (s i)).HasBasis (fun t => t.Finite) fun t => ⋂ i ∈ t, s i

Tactic:
refine ⟨fun U => (mem_iInf_finite _).trans ?_⟩

Result:
α : Type u_1
ι : Type u_6
s : ι → Set α
U : Set α
⊢ (∃ t, U ∈ ⨅ i ∈ t, 𝓟 (s i)) ↔ ∃ i, i.Finite ∧ ⋂ i_1 ∈ i, s i_1 ⊆ U

Proof state:
α : Type u_1
ι : Type u_6
s : ι → Set α
U : Set α
⊢ (∃ t, U ∈ ⨅ i ∈ t, 𝓟 (s i)) ↔ ∃ i, i.Finite ∧ ⋂ i_1 ∈ i, s i_1 ⊆ U

Tactic:
simp only [iInf_principal_finset, mem_iUnion, mem_principal, exists_prop,
  exists_finite_iff_finset, Finset.set_biInter_coe]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.le_of_isLocalized_span {N P : Submodule R M}
    (h : ∀ r : s, N.localized₀ (.powers r.1) (f r) ≤ P.localized₀ (.powers r.1) (f r)) : N ≤ P :=
  fun m hm ↦ mem_of_isLocalized_span s span_eq _ f fun r ↦ h r ⟨m, hm, 1, by simp⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
N P : Submodule R M
h : ∀ (r : ↑s), localized₀ (Submonoid.powers ↑r) (f r) N ≤ localized₀ (Submonoid.powers ↑r) (f r) P
m : M
hm : m ∈ N
r : ↑s
⊢ mk' (f r) m 1 = (f r) m

Tactic:
simp

Result:
no goals