harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Extreme.lean
/-- x is an extreme point to A iff {x} is an extreme set of A. -/
@[simp] lemma isExtreme_singleton : IsExtreme 𝕜 A {x} ↔ x ∈ A.extremePoints 𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
⊢ IsExtreme 𝕜 A {x} ↔ x ∈ extremePoints 𝕜 A

Tactic:
refine ⟨fun hx ↦ ⟨singleton_subset_iff.1 hx.1, fun x₁ hx₁ x₂ hx₂ ↦ hx.2 hx₁ hx₂ rfl⟩, ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A → IsExtreme 𝕜 A {x}

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A → IsExtreme 𝕜 A {x}

Tactic:
rintro ⟨hxA, hAx⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ IsExtreme 𝕜 A {x}

Proof state:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x_1 : E⦄, x_1 ∈ {x} → x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {x} ∧ x₂ ∈ {x}

Tactic:
rintro x₁ hx₁A x₂ hx₂A y (rfl : y = x)

Result:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
y : E
hxA : y ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → y ∈ openSegment 𝕜 x₁ x₂ → x₁ = y ∧ x₂ = y
⊢ y ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {y} ∧ x₂ ∈ {y}

Proof state:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x₁ : E
hx₁A : x₁ ∈ A
x₂ : E
hx₂A : x₂ ∈ A
y : E
hxA : y ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → y ∈ openSegment 𝕜 x₁ x₂ → x₁ = y ∧ x₂ = y
⊢ y ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {y} ∧ x₂ ∈ {y}

Tactic:
exact hAx hx₁A hx₂A

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ IsExtreme 𝕜 A {x}

Tactic:
use singleton_subset_iff.2 hxA

Result:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
x : E
hxA : x ∈ A
hAx : ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ A → ∀ ⦃x₂ : E⦄, x₂ ∈ A → ∀ ⦃x_1 : E⦄, x_1 ∈ {x} → x_1 ∈ openSegment 𝕜 x₁ x₂ → x₁ ∈ {x} ∧ x₂ ∈ {x}
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
@[simp]
lemma mk_comp_mkInv [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W Y X]
    [HasSmallLocalizedHom.{w} W Y Y] (f : Y ⟶ X) (hf : W f) :
    (mk W f).comp (mkInv f hf) = mk W (𝟙 Y) :=
  (equiv W W.Q).injective (by simp [equiv_comp])

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y X
inst✝ : HasSmallLocalizedHom W Y Y
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mk W f).comp (mkInv f hf)) = (equiv W W.Q) (mk W (𝟙 Y))

Tactic:
simp [equiv_comp]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem getLast?_toList (s : Seq α) (h : s.Terminates) :
    (toList s h).getLast? = s.get? (s.length h - 1)

Proof state:
α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h).getLast? = s.get? (s.length h - 1)

Tactic:
rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem tendsto_order [OrderTopology α] {f : β → α} {a : α} {x : Filter β} :
    Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ b in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ b in x, f b < a'

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ i ∈ Iio a, ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ i ∈ Ioi a, ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ Tendsto f x (𝓝 a) ↔ (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'

Tactic:
simp only [nhds_eq_order a, tendsto_inf, tendsto_iInf, tendsto_principal]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
f : β → α
a : α
x : Filter β
⊢ ((∀ i ∈ Iio a, ∀ᶠ (a : β) in x, f a ∈ Ioi i) ∧ ∀ i ∈ Ioi a, ∀ᶠ (a : β) in x, f a ∈ Iio i) ↔
    (∀ a' < a, ∀ᶠ (b : β) in x, a' < f b) ∧ ∀ a' > a, ∀ᶠ (b : β) in x, f b < a'
-- Mathlib/Algebra/Algebra/Basic.lean
theorem NoZeroSMulDivisors.trans_faithfulSMul (R A M : Type*) [CommRing R] [Ring A] [Algebra R A]
    [FaithfulSMul R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
    [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M where
  eq_zero_or_eq_zero_of_smul_eq_zero hx

Proof state:
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : FaithfulSMul R A
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : NoZeroSMulDivisors A M
c✝ : R
x✝ : M
hx : c✝ • x✝ = 0
⊢ c✝ = 0 ∨ x✝ = 0

Tactic:
rw [← algebraMap_smul (A := A)] at hx

Result:
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : FaithfulSMul R A
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : NoZeroSMulDivisors A M
c✝ : R
x✝ : M
hx : (algebraMap R A) c✝ • x✝ = 0
⊢ c✝ = 0 ∨ x✝ = 0

Proof state:
R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁸ : CommRing R
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
inst✝⁵ : FaithfulSMul R A
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
inst✝ : NoZeroSMulDivisors A M
c✝ : R
x✝ : M
hx : (algebraMap R A) c✝ • x✝ = 0
⊢ c✝ = 0 ∨ x✝ = 0

Tactic:
simpa only [map_eq_zero_iff _ <| FaithfulSMul.algebraMap_injective R A] using
  eq_zero_or_eq_zero_of_smul_eq_zero hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) :
    get? (insertMany m l) k' = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ get? (insertMany m l) k' = some v

Tactic:
simp_to_raw using Raw₀.Const.get?_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma induce_pair_connected_of_adj {u v : V} (huv : G.Adj u v) :
    (G.induce {u, v}).Connected

Proof state:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (⊤.induce {u, v}).Connected

Tactic:
exact Subgraph.top_induce_pair_connected_of_adj huv

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (induce {u, v} G).Connected

Tactic:
rw [connected_induce_iff]

Result:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ (⊤.induce {u, v}).Connected
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
/-- If `y ∈ f.target` and `I y ∈ interior (range I)`,
then `I y` is an interior point of `(I ∘ f).target`. -/
lemma mem_interior_extend_target {y : H} (hy : y ∈ f.target)
    (hy' : I y ∈ interior (range I)) : I y ∈ interior (f.extend I).target

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I y ∈ interior (f.extend I).target

Tactic:
rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq,
  mem_inter_iff, mem_preimage]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I.symm (↑I y) ∈ f.target ∧ ↑I y ∈ interior (range ↑I)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : ↑I y ∈ interior (range ↑I)
⊢ ↑I.symm (↑I y) ∈ f.target ∧ ↑I y ∈ interior (range ↑I)

Tactic:
exact ⟨mem_of_eq_of_mem (I.left_inv (y)) hy, hy'⟩

Result:
no goals
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
/-- As `x → ∞`, `f x` decays faster than any power of `x`. -/
lemma hf_top' (r : ℝ) : P.f =O[atTop] (· ^ r)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : StrongFEPair E
r : ℝ
⊢ P.f =O[atTop] fun x => x ^ r

Tactic:
simpa [P.hf₀] using P.hf_top r

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma eval_negPolynomial (x y : R) : W'.negPolynomial.evalEval x y = W'.negY x y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.negPolynomial = W'.negY x y

Tactic:
rw [negY, sub_sub, negPolynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (-Y - C (C W'.a₁ * X + C W'.a₃)) = -y - (W'.a₁ * x + W'.a₃)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (-Y - C (C W'.a₁ * X + C W'.a₃)) = -y - (W'.a₁ * x + W'.a₃)

Tactic:
eval_simp

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mapRange_add (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0)
    (hf' : ∀ i x y, f i (x + y) = f i x + f i y) (g₁ g₂ : Π₀ i, β₁ i) :
    mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂

Proof state:
case h
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf (g₁ + g₂)) i✝ = (mapRange f hf g₁ + mapRange f hf g₂) i✝

Tactic:
simp only [mapRange_apply f, coe_add, Pi.add_apply, hf']

Result:
no goals

Proof state:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂

Tactic:
ext

Result:
case h
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf (g₁ + g₂)) i✝ = (mapRange f hf g₁ + mapRange f hf g₂) i✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem partition_eq_filter_filter (p : α → Bool) (l : List α) :
    partition p l = (filter p l, filter (not ∘ p) l)

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ partition p l = (filter p l, filter (not ∘ p) l)

Tactic:
simp [partition, aux]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l✝ as✝ bs✝ : List α
a : α
l : List α
⊢ partition.loop p (a :: l) (as✝, bs✝) = (as✝.reverse ++ filter p (a :: l), bs✝.reverse ++ filter (not ∘ p) (a :: l))

Tactic:
cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l as✝ bs✝ : List α
⊢ partition.loop p [] (as✝, bs✝) = (as✝.reverse ++ filter p [], bs✝.reverse ++ filter (not ∘ p) [])

Tactic:
simp [partition.loop, filter]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
lemma div_ofReal (z : ℂ) (x : ℝ) : z / x = ⟨z.re / x, z.im / x⟩

Proof state:
z : ℂ
x : ℝ
⊢ z / ↑x = { re := z.re / x, im := z.im / x }

Tactic:
simp_rw [div_eq_inv_mul, ← ofReal_inv, ofReal_mul']

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_eq_iInter_inter {v : Set τ} (hv : v ∈ f) :
    ω f ϕ s = ⋂ u : ↥f.sets, closure (image2 ϕ (u ∩ v) s)

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ⋂ u ∈ f, closure (image2 ϕ (u ∩ v) s) = ⋂ u, closure (image2 ϕ (↑u ∩ v) s)

Tactic:
apply biInter_eq_iInter

Result:
no goals

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ u, closure (image2 ϕ (↑u ∩ v) s)

Tactic:
rw [omegaLimit_eq_biInter_inter _ _ _ hv]

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ⋂ u ∈ f, closure (image2 ϕ (u ∩ v) s) = ⋂ u, closure (image2 ϕ (↑u ∩ v) s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
    foldr n f x = foldrM (m:=Id) n f x

Proof state:
n : Nat
α : Type u_1
f : Fin n → α → α
x : α
⊢ foldr n f x = foldrM n f x

Tactic:
induction n <;> simp [foldr_succ, foldrM_succ, *]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem finite_of_fin_dim_affineIndependent [FiniteDimensional k V] {p : ι → P}
    (hi : AffineIndependent k p) : Finite ι

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent k fun i => p ↑i -ᵥ p default
⊢ Finite ι

Tactic:
letI : IsNoetherian k V := IsNoetherian.iff_fg.2 inferInstance

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent k fun i => p ↑i -ᵥ p default
this : IsNoetherian k V := IsNoetherian.iff_fg.mpr inferInstance
⊢ Finite ι

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent k fun i => p ↑i -ᵥ p default
this : IsNoetherian k V := IsNoetherian.iff_fg.mpr inferInstance
⊢ Finite ι

Tactic:
exact
  (Set.finite_singleton default).finite_of_compl (Set.finite_coe_iff.1 hi.finite_of_isNoetherian)

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
⊢ Finite ι

Tactic:
inhabit ι

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
⊢ Finite ι

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
⊢ Finite ι

Tactic:
rw [affineIndependent_iff_linearIndependent_vsub k p default] at hi

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
a✝ : Nontrivial ι
inhabited_h : Inhabited ι
hi : LinearIndependent k fun i => p ↑i -ᵥ p default
⊢ Finite ι

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
⊢ Finite ι

Tactic:
nontriviality ι

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : FiniteDimensional k V
p : ι → P
hi : AffineIndependent k p
a✝ : Nontrivial ι
⊢ Finite ι
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_mul_monomial (p : R[X]) (n d : ℕ) (r : R) :
    coeff (p * monomial n r) (d + n) = coeff p d * r

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
r : R
⊢ (p * (monomial n) r).coeff (d + n) = p.coeff d * r

Tactic:
rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_add_right' (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : AEMeasurable g μ) :
    ∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
⊢ ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ

Tactic:
simpa only [add_comm] using lintegral_add_left' hg f

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem equalizer.isoSourceOfSelf_inv :
    (equalizer.isoSourceOfSelf f).inv = equalizer.lift (𝟙 X) (by simp)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoSourceOfSelf f).inv ≫ ι f f = lift (𝟙 X) ⋯ ≫ ι f f

Tactic:
simp [equalizer.isoSourceOfSelf]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoSourceOfSelf f).inv = lift (𝟙 X) ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoSourceOfSelf f).inv ≫ ι f f = lift (𝟙 X) ⋯ ≫ ι f f
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x : ↥H
n : ℤ
⊢ ↑(x ^ n) = ↑x ^ n

Tactic:
dsimp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem eLpNormEssSup_add_le {f g : α → E} :
    eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
x : α
⊢ (fun x => ‖(f + g) x‖ₑ) x ≤ ((fun x => ‖f x‖ₑ) + fun x => ‖g x‖ₑ) x

Tactic:
simp_rw [Pi.add_apply, enorm_eq_nnnorm, ← ENNReal.coe_add, ENNReal.coe_le_coe]

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
x : α
⊢ ‖f x + g x‖₊ ≤ ‖f x‖₊ + ‖g x‖₊

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
⊢ eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ

Tactic:
refine le_trans (essSup_mono_ae (Eventually.of_forall fun x => ?_)) (ENNReal.essSup_add_le _ _)

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
x : α
⊢ (fun x => ‖(f + g) x‖ₑ) x ≤ ((fun x => ‖f x‖ₑ) + fun x => ‖g x‖ₑ) x

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
x : α
⊢ ‖f x + g x‖₊ ≤ ‖f x‖₊ + ‖g x‖₊

Tactic:
exact nnnorm_add_le _ _

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
theorem preimage_id : F.preimage (𝟙 (F.obj X)) = 𝟙 X :=
  F.map_injective (by simp)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X : C
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (F.preimage (𝟙 (F.obj X))) = F.map (𝟙 X)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_univ (α : Type*) : (univ : Set α).ncard = Nat.card α

Proof state:
case inr
α : Type u_3
h : Infinite α
⊢ univ.Infinite

Tactic:
exact infinite_univ

Result:
no goals

Proof state:
case inl
α : Type u_3
h : Finite α
⊢ univ.ncard = Nat.card α

Tactic:
have hft := Fintype.ofFinite α

Result:
case inl
α : Type u_3
h : Finite α
hft : Fintype α
⊢ univ.ncard = Nat.card α

Proof state:
case inl
α : Type u_3
h : Finite α
hft : Fintype α
⊢ univ.ncard = Nat.card α

Tactic:
rw [ncard_eq_toFinset_card, Finite.toFinset_univ, Finset.card_univ, Nat.card_eq_fintype_card]

Result:
no goals

Proof state:
α : Type u_3
⊢ univ.ncard = Nat.card α

Tactic:
rcases finite_or_infinite α with h | h

Result:
case inl
α : Type u_3
h : Finite α
⊢ univ.ncard = Nat.card α

case inr
α : Type u_3
h : Infinite α
⊢ univ.ncard = Nat.card α

Proof state:
case inr
α : Type u_3
h : Infinite α
⊢ univ.ncard = Nat.card α

Tactic:
rw [Nat.card_eq_zero_of_infinite, Infinite.ncard]

Result:
case inr
α : Type u_3
h : Infinite α
⊢ univ.Infinite
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_div (hc : c ≠ 0) :
    (∫ x in a..b, f (x / c)) = c • ∫ x in a / c..b / c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (x / c) = c • ∫ (x : ℝ) in a / c..b / c, f x

Tactic:
simpa only [inv_inv] using integral_comp_mul_right f (inv_ne_zero hc)

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
@[to_additive]
lemma cauchy_iff_tendsto_swapped (𝓕 : Filter G) :
    Cauchy 𝓕 ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ p.2 / p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Proof state:
G : Type u_4
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝓕 : Filter G
⊢ Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Tendsto (fun p => p.2 / p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [Cauchy, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
theorem dotProduct_self_star_pos_iff {v : n → R} : 0 < dotProduct v (star v) ↔ v ≠ 0

Proof state:
n : Type u_2
R : Type u_4
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ 0 < v ⬝ᵥ star v ↔ v ≠ 0

Tactic:
simpa using dotProduct_star_self_pos_iff (v := star v)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c

Proof state:
a b c : Int
H : c ∣ a
⊢ (a + b) / c = a / c + b / c

Tactic:
rw [Int.add_comm, Int.add_ediv_of_dvd_right H, Int.add_comm]

Result:
no goals