harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/Dvr.lean
theorem Ring.DimensionLEOne.localization {R : Type*} (Rₘ : Type*) [CommRing R] [IsDomain R]
    [CommRing Rₘ] [Algebra R Rₘ] {M : Submonoid R} [IsLocalization M Rₘ] (hM : M ≤ R⁰)
    [h : Ring.DimensionLEOne R] : Ring.DimensionLEOne Rₘ := ⟨by
  intro p hp0 hpp
  refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩
  have hpP' : (⟨p, hpp⟩ : { p : Ideal Rₘ // p.IsPrime }) < ⟨P, hPm.isPrime⟩ := hpP
  rw [← (IsLocalization.orderIsoOfPrime M Rₘ).lt_iff_lt] at hpP'
  haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) p) :=
    ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨p, hpp⟩).2.1
  haveI : Ideal.IsPrime (Ideal.comap (algebraMap R Rₘ) P) :=
    ((IsLocalization.orderIsoOfPrime M Rₘ) ⟨P, hPm.isPrime⟩).2.1
  have hlt : Ideal.comap (algebraMap R Rₘ) p < Ideal.comap (algebraMap R Rₘ) P := hpP'
  refine h.not_lt_lt ⊥ (Ideal.comap _ _) (Ideal.comap _ _) ⟨?_, hlt⟩
  exact IsLocalization.bot_lt_comap_prime _ _ hM _ hp0⟩

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
⊢ ∀ {p : Ideal Rₘ}, p ≠ ⊥ → p.IsPrime → p.IsMaximal

Tactic:
intro p hp0 hpp

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
⊢ p.IsMaximal

Proof state:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
⊢ p.IsMaximal

Tactic:
refine Ideal.isMaximal_def.mpr ⟨hpp.ne_top, Ideal.maximal_of_no_maximal fun P hpP hPm => ?_⟩

Result:
R : Type u_2
Rₘ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
M : Submonoid R
inst✝ : IsLocalization M Rₘ
hM : M ≤ R⁰
h : DimensionLEOne R
p : Ideal Rₘ
hp0 : p ≠ ⊥
hpp : p.IsPrime
P : Ideal Rₘ
hpP : p < P
hPm : P.IsMaximal
⊢ False
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem le_span_singleton_iff {s : Submodule R M} {v₀ : M} :
    (s ≤ R ∙ v₀) ↔ ∀ v ∈ s, ∃ r : R, r • v₀ = v

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
v₀ : M
⊢ s ≤ span R {v₀} ↔ ∀ v ∈ s, ∃ r, r • v₀ = v

Tactic:
simp_rw [SetLike.le_def, mem_span_singleton]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem exists_dist_le_lt (hδ : 0 ≤ δ) (hε : 0 < ε) (h : dist x z < ε + δ) :
    ∃ y, dist x y ≤ δ ∧ dist y z < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
rw [← div_lt_one (add_pos_of_pos_of_nonneg hε hδ)] at h

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z < ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ y, dist x y ≤ δ ∧ dist y z < ε

Tactic:
refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ)
  (div_nonneg hδ <| add_nonneg hε.le hδ) <| by
    rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']).imp
  fun y hy => ?_

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z / (ε + δ) < 1
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
exact ⟨mul_le_of_le_one_left hδ h.le, mul_lt_of_lt_one_left hε h⟩

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem ne_zero_of_mul_eq_one (I J : FractionalIdeal R₁⁰ K) (h : I * J = 1) : I ≠ 0 := fun hI =>
  zero_ne_one' (FractionalIdeal R₁⁰ K)
    (by
      convert h
      simp [hI])

Proof state:
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I = 0
⊢ 0 = 1

Tactic:
convert h

Result:
case h.e'_2
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I = 0
⊢ 0 = I * J

Proof state:
case h.e'_2
R₁ : Type u_3
inst✝² : CommRing R₁
K : Type u_4
inst✝¹ : Field K
inst✝ : Algebra R₁ K
I J : FractionalIdeal R₁⁰ K
h : I * J = 1
hI : I = 0
⊢ 0 = I * J

Tactic:
simp [hI]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
    (as.push a).all p = (as.all p && p a) :=
  all_push' (by simp)

Proof state:
α : Type u_1
inst✝ : BEq α
as : Array α
a : α
p : α → Bool
⊢ (as.push a).size = as.size + 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma sumElim_vecMul_fromRows [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R)
    (v₁ : m₁ → R) (v₂ : m₂ → R) :
    Sum.elim v₁ v₂ ᵥ* fromRows B₁ B₂ = v₁ ᵥ* B₁ + v₂ ᵥ* B₂

Proof state:
case h
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
x✝ : n
⊢ (Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂) x✝ = (v₁ ᵥ* B₁ + v₂ ᵥ* B₂) x✝

Tactic:
simp [Matrix.vecMul, fromRows, dotProduct]

Result:
no goals

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
⊢ Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂ = v₁ ᵥ* B₁ + v₂ ᵥ* B₂

Tactic:
ext

Result:
case h
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
x✝ : n
⊢ (Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂) x✝ = (v₁ ᵥ* B₁ + v₂ ᵥ* B₂) x✝
-- Mathlib/Data/Real/EReal.lean
lemma toENNReal_ne_zero_iff {x : EReal} : x.toENNReal ≠ 0 ↔ 0 < x

Proof state:
x : EReal
⊢ x.toENNReal ≠ 0 ↔ 0 < x

Tactic:
simp [toENNReal_eq_zero_iff.not]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_eq_bot (f : ι → α) : iInf f = ⊥ ↔ ∀ b > ⊥, ∃ i, f i < b

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iInf f = ⊥ ↔ ∀ b > ⊥, ∃ i, f i < b

Tactic:
simp only [← sInf_range, sInf_eq_bot, Set.exists_range_iff]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_iff_ultrafilter_le_nhds :
    IsCompact s ↔ ∀ f : Ultrafilter X, ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Proof state:
case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x ↑f) ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
simp only [Ultrafilter.clusterPt_iff]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
refine (forall_neBot_le_iff ?_).trans ?_

Result:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Monotone fun f => ∃ x ∈ s, ClusterPt x f

case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x ↑f) ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

Proof state:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Monotone fun f => ∃ x ∈ s, ClusterPt x f

Tactic:
rintro f g hle ⟨x, hxs, hxf⟩

Result:
case refine_1.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f g : Filter X
hle : f ≤ g
x : X
hxs : x ∈ s
hxf : ClusterPt x f
⊢ ∃ x ∈ s, ClusterPt x g

Proof state:
case refine_1.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f g : Filter X
hle : f ≤ g
x : X
hxs : x ∈ s
hxf : ClusterPt x f
⊢ ∃ x ∈ s, ClusterPt x g

Tactic:
exact ⟨x, hxs, hxf.mono hle⟩

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem pred_to_nat {n : PosNum} (h : 1 < n) : (pred n : ℕ) = Nat.pred n

Proof state:
case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = (↑n).pred

Tactic:
rw [← pred'_to_nat, e]

Result:
case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = ↑(pos a✝)

Proof state:
n : PosNum
h : 1 < n
⊢ ↑n.pred = (↑n).pred

Tactic:
unfold pred

Result:
n : PosNum
h : 1 < n
⊢ ↑(Num.casesOn n.pred' 1 id) = (↑n).pred

Proof state:
case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Tactic:
have : (1 : ℕ) ≤ Nat.pred n := Nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h)

Result:
case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ (↑n).pred
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Proof state:
case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ (↑n).pred
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Tactic:
rw [← pred'_to_nat, e] at this

Result:
case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑zero
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Proof state:
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑zero
⊢ ¬1 ≤ ↑zero

Tactic:
decide

Result:
no goals

Proof state:
n : PosNum
h : 1 < n
⊢ ↑(Num.casesOn n.pred' 1 id) = (↑n).pred

Tactic:
cases e : pred' n

Result:
case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = (↑n).pred

Proof state:
case zero
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ ↑zero
⊢ ↑(Num.casesOn zero 1 id) = (↑n).pred

Tactic:
exact absurd this (by decide)

Result:
no goals

Proof state:
case pos
n : PosNum
h : 1 < n
a✝ : PosNum
e : n.pred' = pos a✝
⊢ ↑(Num.casesOn (pos a✝) 1 id) = ↑(pos a✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem bddBelow_range_add : BddBelow (range fun u => p u + q (x - u)) :=
  ⟨0, by
    rintro _ ⟨x, rfl⟩
    dsimp; positivity⟩

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
⊢ 0 ∈ lowerBounds (range fun u => p u + q (x - u))

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ (fun u => p u + q (x✝ - u)) x

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ (fun u => p u + q (x✝ - u)) x

Tactic:
dsimp

Result:
case intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ - x)

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x✝ x : E
⊢ 0 ≤ p x + q (x✝ - x)

Tactic:
positivity

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem setIntegral_condExp (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)] (hf : Integrable f μ)
    (hs : MeasurableSet[m] s) : ∫ x in s, (μ[f|m]) x ∂μ = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
s : Set α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
exact setIntegral_condExpL1 hf hs

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
s : Set α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ[f|m]) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [setIntegral_congr_ae (hm s hs) ((condExp_ae_eq_condExpL1 hm f).mono fun x hx _ => hx)]

Result:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
s : Set α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
hf : Integrable f μ
hs : MeasurableSet s
⊢ ∫ (x : α) in s, ↑↑(condExpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
-- Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
theorem squashSeq_nth_of_not_terminated {gp_n gp_succ_n : Pair K} (s_nth_eq : s.get? n = some gp_n)
    (s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n) :
    (squashSeq s n).get? n = some ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩

Proof state:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
gp_n gp_succ_n : Pair K
s_nth_eq : s.get? n = some gp_n
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ (squashSeq s n).get? n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }

Tactic:
simp [*, squashSeq]

Result:
no goals
-- Mathlib/Analysis/Analytic/Linear.lean
theorem hasFPowerSeriesOnBall (f : E →L[𝕜] F) (x : E) :
    HasFPowerSeriesOnBall f (f.fpowerSeries x) x ∞ :=
  { r_le

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ ⊤ ≤ (f.fpowerSeries x).radius

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E →L[𝕜] F
x y✝ : E
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => (f.fpowerSeries x (n + 2)) fun x => y✝)
    (f (x + y✝) - ∑ i ∈ Finset.range 2, (f.fpowerSeries x i) fun x => y✝)

Tactic:
simp [Finset.sum_range_succ, ← sub_sub, hasSum_zero, fpowerSeries]

Result:
no goals
-- Mathlib/LinearAlgebra/Pi.lean
theorem iInf_ker_proj : (⨅ i, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) :
    Submodule R ((i : ι) → φ i)) = ⊥ :=
  bot_unique <|
    SetLike.le_def.2 fun a h => by
      simp only [mem_iInf, mem_ker, proj_apply] at h
      exact (mem_bot _).2 (funext fun i => h i)

Proof state:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
a : (i : ι) → φ i
h : a ∈ ⨅ i, ker (proj i)
⊢ a ∈ ⊥

Tactic:
simp only [mem_iInf, mem_ker, proj_apply] at h

Result:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
a : (i : ι) → φ i
h : ∀ (i : ι), a i = 0
⊢ a ∈ ⊥

Proof state:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
a : (i : ι) → φ i
h : ∀ (i : ι), a i = 0
⊢ a ∈ ⊥

Tactic:
exact (mem_bot _).2 (funext fun i => h i)

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem id_map {α : TypeVec n} (x : F α) : TypeVec.id <$$> x = x

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ abs (TypeVec.id <$$> repr x) = abs (repr x)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ TypeVec.id <$$> x = x

Tactic:
rw [← abs_repr x, ← abs_map]

Result:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
⊢ abs (TypeVec.id <$$> repr x) = abs (repr x)
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_nonneg : 0 ≤ hausdorffDist s t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ 0 ≤ hausdorffDist s t

Tactic:
simp [hausdorffDist]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem sdiff_symmDiff_eq_sup : (a \ b) ∆ b = a ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) ∆ b = a ⊔ b

Tactic:
rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem lt_of_le_of_lt : ∀ {x y z : Bool}, x ≤ y → y < z → x < z

Proof state:
⊢ ∀ {x y z : Bool}, x ≤ y → y < z → x < z

Tactic:
decide

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem getElem_le_maximum_of_length_pos {i : ℕ} (w : i < l.length) (h := (Nat.zero_lt_of_lt w)) :
    l[i] ≤ l.maximum_of_length_pos h

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : optParam (0 < l.length) ⋯
⊢ l[i] ∈ l

Tactic:
exact getElem_mem _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : optParam (0 < l.length) ⋯
⊢ l[i] ≤ maximum_of_length_pos h

Tactic:
apply le_maximum_of_length_pos_of_mem

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : optParam (0 < l.length) ⋯
⊢ l[i] ∈ l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_map (f : β → α) (xs : Vector β n) :
    find? p (xs.map f) = (xs.find? (p ∘ f)).map f

Proof state:
case mk
β α : Type
n : Nat
p : α → Bool
f : β → α
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ find? p (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    Option.map f (find? (p ∘ f) { toArray := toArray✝, size_toArray := size_toArray✝ })

Tactic:
simp

Result:
no goals

Proof state:
β α : Type
n : Nat
p : α → Bool
f : β → α
xs : Vector β n
⊢ find? p (map f xs) = Option.map f (find? (p ∘ f) xs)

Tactic:
cases xs

Result:
case mk
β α : Type
n : Nat
p : α → Bool
f : β → α
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ find? p (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    Option.map f (find? (p ∘ f) { toArray := toArray✝, size_toArray := size_toArray✝ })
-- Mathlib/Data/Finset/Sups.lean
lemma map_infs (f : F) (hf) (s t : Finset α) :
    map ⟨f, hf⟩ (s ⊼ t) = map ⟨f, hf⟩ s ⊼ map ⟨f, hf⟩ t

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : SemilatticeInf α
inst✝² : SemilatticeInf β
inst✝¹ : FunLike F α β
inst✝ : InfHomClass F α β
f : F
hf : Injective ⇑f
s t : Finset α
⊢ map { toFun := ⇑f, inj' := hf } (s ⊼ t) = map { toFun := ⇑f, inj' := hf } s ⊼ map { toFun := ⇑f, inj' := hf } t

Tactic:
simpa [map_eq_image] using image_infs f s t

Result:
no goals
-- Mathlib/RingTheory/IntegralDomain.lean
theorem card_nthRoots_subgroup_units [Fintype G] [DecidableEq G] (f : G →* R) (hf : Injective f)
    {n : ℕ} (hn : 0 < n) (g₀ : G) :
    #{g | g ^ n = g₀} ≤ Multiset.card (nthRoots n (f g₀))

Proof state:
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ⇑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ ∀ a ∈ filter (fun g => g ^ n = g₀) univ, f a ∈ (nthRoots n (f g₀)).toFinset

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ⇑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ #(filter (fun g => g ^ n = g₀) univ) ≤ (nthRoots n (f g₀)).card

Tactic:
calc
  _ ≤ #(nthRoots n (f g₀)).toFinset := card_le_card_of_injOn f (by aesop) hf.injOn
  _ ≤ _ := (nthRoots n (f g₀)).toFinset_card_le

Result:
no goals

Proof state:
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ⇑f
n : ℕ
hn : 0 < n
g₀ : G
⊢ #(filter (fun g => g ^ n = g₀) univ) ≤ (nthRoots n (f g₀)).card

Tactic:
haveI : DecidableEq R := Classical.decEq _

Result:
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ⇑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ #(filter (fun g => g ^ n = g₀) univ) ≤ (nthRoots n (f g₀)).card
-- Mathlib/Algebra/Lie/Abelian.lean
theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :
    Std.Commutative (α := A) (· * ·) ↔ IsLieAbelian A

Proof state:
A : Type v
inst✝ : Ring A
h₁ : (Std.Commutative fun x1 x2 => x1 * x2) ↔ ∀ (a b : A), a * b = b * a
h₂ : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
⊢ (Std.Commutative fun x1 x2 => x1 * x2) ↔ IsLieAbelian A

Tactic:
simp only [h₁, h₂, LieRing.of_associative_ring_bracket, sub_eq_zero]

Result:
no goals

Proof state:
A : Type v
inst✝ : Ring A
h₁ : (Std.Commutative fun x1 x2 => x1 * x2) ↔ ∀ (a b : A), a * b = b * a
⊢ (Std.Commutative fun x1 x2 => x1 * x2) ↔ IsLieAbelian A

Tactic:
have h₂ : IsLieAbelian A ↔ ∀ a b : A, ⁅a, b⁆ = 0 := ⟨fun h => h.1, fun h => ⟨h⟩⟩

Result:
A : Type v
inst✝ : Ring A
h₁ : (Std.Commutative fun x1 x2 => x1 * x2) ↔ ∀ (a b : A), a * b = b * a
h₂ : IsLieAbelian A ↔ ∀ (a b : A), ⁅a, b⁆ = 0
⊢ (Std.Commutative fun x1 x2 => x1 * x2) ↔ IsLieAbelian A
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem contDiffOn_iff_continuousOn_differentiableOn_deriv {n : ℕ∞} (hs : UniqueDiffOn 𝕜 s) :
    ContDiffOn 𝕜 n f s ↔ (∀ m : ℕ, (m : ℕ∞) ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ m : ℕ, (m : ℕ∞) < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
n : ℕ∞
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (↑n) f s ↔
    (∀ (m : ℕ), ↑m ≤ n → ContinuousOn (iteratedDerivWithin m f s) s) ∧
      ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s

Tactic:
simp only [contDiffOn_iff_continuousOn_differentiableOn hs, iteratedFDerivWithin_eq_equiv_comp,
  LinearIsometryEquiv.comp_continuousOn_iff, LinearIsometryEquiv.comp_differentiableOn_iff]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem isStarNormal_of_mem {x : R} (hx : x ∈ skewAdjoint R) : IsStarNormal x :=
  ⟨by
    simp only [mem_iff] at hx
    simp only [hx, Commute.neg_left, Commute.refl]⟩

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : x ∈ skewAdjoint R
⊢ Commute (star x) x

Tactic:
simp only [mem_iff] at hx

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x

Tactic:
simp only [hx, Commute.neg_left, Commute.refl]

Result:
no goals