harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_insertListConst_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert):
    getValueD k' (insertListConst l toInsert) fallback= v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
v fallback : β
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ getValueD k' (insertListConst l toInsert) fallback = v

Tactic:
simp only [getValueD_eq_getValue?]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
v fallback : β
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ (getValue? k' (insertListConst l toInsert)).getD fallback = v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
v fallback : β
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ (getValue? k' (insertListConst l toInsert)).getD fallback = v

Tactic:
rw [getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem, Option.getD_some]

Result:
no goals
-- Mathlib/Data/Finsupp/Weight.lean
theorem finite_of_nat_weight_le [Finite σ] (w : σ → ℕ) (hw : ∀ x, w x ≠ 0) (n : ℕ) :
    {d : σ →₀ ℕ | weight w d ≤ n}.Finite

Proof state:
case h.h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
x : σ
⊢ n - d x + d x = n

Tactic:
apply Nat.sub_add_cancel

Result:
case h.h.h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
x : σ
⊢ d x ≤ n

Proof state:
case h.h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
x : σ
⊢ (d + (equivFunOnFinite.symm (Function.const σ n) - d)) x = (equivFunOnFinite.symm (Function.const σ n)) x

Tactic:
simp only [Finsupp.coe_add, Finsupp.coe_tsub, Pi.add_apply, Pi.sub_apply,
  Finsupp.equivFunOnFinite_symm_apply_toFun, Function.const_apply]

Result:
case h.h
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
x : σ
⊢ d x + (n - d x) = n

Proof state:
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ d ∈ ↑(Finset.image (fun uv => uv.1) (Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))))

Tactic:
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
  Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]

Result:
σ : Type u_1
inst✝ : Finite σ
w : σ → ℕ
hw : ∀ (x : σ), w x ≠ 0
n : ℕ
fg : Finset ((σ →₀ ℕ) × (σ →₀ ℕ)) := Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
hfg : fg = Finset.antidiagonal (equivFunOnFinite.symm (Function.const σ n))
d : σ →₀ ℕ
hd : d ∈ {d | (weight w) d ≤ n}
⊢ ∃ x, d + x = equivFunOnFinite.symm (Function.const σ n)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem containsThenInsertIfNew_fst (h : m.WF) {k : α} {v : β k} :
    (m.containsThenInsertIfNew k v).1 = m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝¹ : BEq α
inst✝ : Hashable α
h : m.WF
k : α
v : β k
⊢ (m.containsThenInsertIfNew k v).fst = m.contains k

Tactic:
simp_to_raw using Raw₀.containsThenInsertIfNew_fst

Result:
no goals
-- Mathlib/Algebra/QuaternionBasis.lean
theorem k_mul_k : q.k * q.k = -((c₁ * c₃) • (1 : A))

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * c₃ • 1) - ((c₁ * c₃) • 1 + c₂ • (q.i * c₃ • 1)) = -((c₁ * c₃) • 1)

Tactic:
linear_combination (norm := module)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.k = -((c₁ * c₃) • 1)

Tactic:
rw [← i_mul_j, mul_assoc, ← mul_assoc q.j _ _, j_mul_i, ← i_mul_j, ← mul_assoc, mul_sub, ←
  mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, sub_mul, smul_mul_assoc, mul_smul_comm,
  smul_mul_assoc, mul_assoc, j_mul_j, add_mul, smul_mul_assoc, j_mul_j, smul_smul,
  smul_mul_assoc, mul_assoc, j_mul_j]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * c₃ • 1) - ((c₁ * c₃) • 1 + c₂ • (q.i * c₃ • 1)) = -((c₁ * c₃) • 1)
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_target_union_compl_range_mem_nhds_of_mem {y : E} {x : M}
    (hy : y ∈ (extChartAt I x).target) : (extChartAt I x).target ∪ (range I)ᶜ ∈ 𝓝 y

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
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝[range ↑I] y ⊔ 𝓝[(range ↑I)ᶜ] y

Tactic:
exact Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin_of_mem hy) self_mem_nhdsWithin

Result:
no goals

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
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝 y

Tactic:
rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]

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
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range ↑I)ᶜ ∈ 𝓝[range ↑I] y ⊔ 𝓝[(range ↑I)ᶜ] y
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem prevD_chainComplex (f : ∀ i j, P.X i ⟶ Q.X j) (j : ℕ) :
    prevD j f = f j (j + 1) ≫ Q.d _ _

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ (prevD j) f = f j (j + 1) ≫ Q.d (j + 1) j

Tactic:
dsimp [prevD]

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ f j ((ComplexShape.down ℕ).prev j) ≫ Q.d ((ComplexShape.down ℕ).prev j) j = f j (j + 1) ≫ Q.d (j + 1) j

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
this : (ComplexShape.down ℕ).prev j = j + 1
⊢ f j ((ComplexShape.down ℕ).prev j) ≫ Q.d ((ComplexShape.down ℕ).prev j) j = f j (j + 1) ≫ Q.d (j + 1) j

Tactic:
congr 2

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ f j ((ComplexShape.down ℕ).prev j) ≫ Q.d ((ComplexShape.down ℕ).prev j) j = f j (j + 1) ≫ Q.d (j + 1) j

Tactic:
have : (ComplexShape.down ℕ).prev j = j + 1 := ChainComplex.prev ℕ j

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
this : (ComplexShape.down ℕ).prev j = j + 1
⊢ f j ((ComplexShape.down ℕ).prev j) ≫ Q.d ((ComplexShape.down ℕ).prev j) j = f j (j + 1) ≫ Q.d (j + 1) j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) :
    xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : ¬findIdx p xs ≤ i
⊢ False

Tactic:
simp at h3

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : i < findIdx p xs
⊢ False

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs = i

Tactic:
apply Nat.le_antisymm _ (le_findIdx_of_not h h2)

Result:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs ≤ i

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs ≤ i

Tactic:
apply Decidable.byContradiction

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬findIdx p xs ≤ i → False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : i < findIdx p xs
⊢ False

Tactic:
simp_all [not_of_lt_findIdx h3]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
⊢ findIdx p xs = i ↔ p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false

Tactic:
refine ⟨fun f ↦ ⟨f ▸ (@findIdx_getElem _ p xs (f ▸ h)), fun _ hji ↦ not_of_lt_findIdx (f ▸ hji)⟩,
  fun ⟨_, h2⟩ ↦ ?_⟩

Result:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ findIdx p xs = i

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬findIdx p xs ≤ i → False

Tactic:
intro h3

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
x✝ : p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false
left✝ : p xs[i] = true
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
h3 : ¬findIdx p xs ≤ i
⊢ False
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_trim_ae (hm : m ≤ m0) {f : β → G} (hf : AEStronglyMeasurable[m] f (μ.trim hm)) :
    ∫ x, f x ∂μ = ∫ x, f x ∂μ.trim hm

Proof state:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
rw [integral_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk), integral_congr_ae hf.ae_eq_mk]

Result:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ = ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm

Proof state:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : AEStronglyMeasurable f (μ.trim hm)
⊢ ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ = ∫ (a : β), AEStronglyMeasurable.mk f hf a ∂μ.trim hm

Tactic:
exact integral_trim hm hf.stronglyMeasurable_mk

Result:
no goals
-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational {ξ : ℝ} (hξ : Irrational ξ) :
    {q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2}.Infinite

Proof state:
ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
⊢ ↑⌊ξ⌋ ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}

Tactic:
simp [abs_of_nonneg, Int.fract_lt_one]

Result:
no goals

Proof state:
case intro.intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
q : ℚ
left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
hq : ∀ b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}, |ξ - ↑q| ≤ |ξ - ↑b|
q' : ℚ
hmem : |ξ - ↑q'| < 1 / ↑q'.den ^ 2
hbetter : |ξ - ↑q'| < |ξ - ↑q|
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt (hq q' hmem) hbetter)

Result:
no goals

Proof state:
ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
⊢ False

Tactic:
obtain ⟨q, _, hq⟩ :=
  exists_min_image {q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2} (fun q => |ξ - q|) h
    ⟨⌊ξ⌋, by simp [abs_of_nonneg, Int.fract_lt_one]⟩

Result:
case intro.intro
ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
q : ℚ
left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
hq : ∀ b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}, |ξ - ↑q| ≤ |ξ - ↑b|
⊢ False

Proof state:
ξ : ℝ
hξ : Irrational ξ
⊢ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite

Tactic:
refine Or.resolve_left (Set.finite_or_infinite _) fun h => ?_

Result:
ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
⊢ False

Proof state:
case intro.intro
ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
q : ℚ
left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
hq : ∀ b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}, |ξ - ↑q| ≤ |ξ - ↑b|
⊢ False

Tactic:
obtain ⟨q', hmem, hbetter⟩ := exists_rat_abs_sub_lt_and_lt_of_irrational hξ q

Result:
case intro.intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
h : {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Finite
q : ℚ
left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
hq : ∀ b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}, |ξ - ↑q| ≤ |ξ - ↑b|
q' : ℚ
hmem : |ξ - ↑q'| < 1 / ↑q'.den ^ 2
hbetter : |ξ - ↑q'| < |ξ - ↑q|
⊢ False
-- Mathlib/Data/Array/ExtractLemmas.lean
theorem extract_append_left {a b : Array α} {i j : Nat} (h : j ≤ a.size) :
    (a ++ b).extract i j = a.extract i j

Proof state:
case h₂
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
h1 : Nat
h2 : h1 < ((a ++ b).extract i j).size
h3 : h1 < (a.extract i j).size
⊢ ((a ++ b).extract i j)[h1] = (a.extract i j)[h1]

Tactic:
rw [getElem_extract, getElem_append_left, getElem_extract]

Result:
no goals

Proof state:
case h₁
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
⊢ ((a ++ b).extract i j).size = (a.extract i j).size

Tactic:
simp only [size_extract, size_append]

Result:
case h₁
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
⊢ min j (a.size + b.size) - i = min j a.size - i

Proof state:
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
⊢ (a ++ b).extract i j = a.extract i j

Tactic:
apply ext

Result:
case h₁
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
⊢ ((a ++ b).extract i j).size = (a.extract i j).size

case h₂
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < ((a ++ b).extract i j).size) (hi₂ : i_1 < (a.extract i j).size),
    ((a ++ b).extract i j)[i_1] = (a.extract i j)[i_1]

Proof state:
case h₁
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
⊢ min j (a.size + b.size) - i = min j a.size - i

Tactic:
omega

Result:
no goals

Proof state:
case h₂
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < ((a ++ b).extract i j).size) (hi₂ : i_1 < (a.extract i j).size),
    ((a ++ b).extract i j)[i_1] = (a.extract i j)[i_1]

Tactic:
intro h1 h2 h3

Result:
case h₂
α : Type u
a b : Array α
i j : Nat
h : j ≤ a.size
h1 : Nat
h2 : h1 < ((a ++ b).extract i j).size
h3 : h1 < (a.extract i j).size
⊢ ((a ++ b).extract i j)[h1] = (a.extract i j)[h1]
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.bInter {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} {u : Set ι} (h : ∃ n ∈ u, IndepSets (s n) s' κ μ) :
    IndepSets (⋂ n ∈ u, s n) s' κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
h : ∃ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n ∈ u, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
rcases h with ⟨n, hn, h⟩

Result:
case intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n ∈ u, s n
ht2 : t2 ∈ s'
n : ι
hn : n ∈ u
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
h : ∃ n ∈ u, IndepSets (s n) s' κ μ
⊢ IndepSets (⋂ n ∈ u, s n) s' κ μ

Tactic:
intro t1 t2 ht1 ht2

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
h : ∃ n ∈ u, IndepSets (s n) s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n ∈ u, s n
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
case intro.intro
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
u : Set ι
t1 t2 : Set Ω
ht1 : t1 ∈ ⋂ n ∈ u, s n
ht2 : t2 ∈ s'
n : ι
hn : n ∈ u
h : IndepSets (s n) s' κ μ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact h t1 t2 (Set.biInter_subset_of_mem hn ht1) ht2

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.induction_on {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α) (hs : s.Finite)
    (empty : motive ∅ finite_empty)
    (insert : ∀ {a s}, a ∉ s →
      ∀ hs : Set.Finite s, motive s hs → motive (insert a s) (hs.insert a)) :
    motive s hs

Proof state:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
⊢ motive s hs

Tactic:
lift s to Finset α using id hs

Result:
case intro
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
s : Finset α
hs : (↑s).Finite
⊢ motive (↑s) hs

Proof state:
case intro.h₁
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
hs : (↑∅).Finite
⊢ motive (↑∅) hs

Tactic:
simpa

Result:
no goals

Proof state:
case intro
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
s : Finset α
hs : (↑s).Finite
⊢ motive (↑s) hs

Tactic:
induction' s using Finset.cons_induction_on with a s ha ih

Result:
case intro.h₁
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
hs : (↑∅).Finite
⊢ motive (↑∅) hs

case intro.h₂
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
a : α
s : Finset α
ha : a ∉ s
ih : ∀ (hs : (↑s).Finite), motive (↑s) hs
hs : (↑(Finset.cons a s ha)).Finite
⊢ motive (↑(Finset.cons a s ha)) hs

Proof state:
case intro.h₂
α : Type u
motive : (s : Set α) → s.Finite → Prop
empty : motive ∅ ⋯
insert : ∀ {a : α} {s : Set α}, a ∉ s → ∀ (hs : s.Finite), motive s hs → motive (Insert.insert a s) ⋯
a : α
s : Finset α
ha : a ∉ s
ih : ∀ (hs : (↑s).Finite), motive (↑s) hs
hs : (↑(Finset.cons a s ha)).Finite
⊢ motive (↑(Finset.cons a s ha)) hs

Tactic:
simpa using @insert a s ha (Set.toFinite _) (ih _)

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem rootSet_monomial [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R}
    (ha : a ≠ 0) : (monomial n a).rootSet S = {0}

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ ((monomial n) a).rootSet S = {0}

Tactic:
rw [rootSet, aroots_monomial ha,
  Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ ((monomial n) a).rootSet S = {0}

Tactic:
classical
rw [rootSet, aroots_monomial ha,
  Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton, Finset.coe_singleton]

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_comp_trace_of_basis [Algebra S T] [IsScalarTower R S T] {ι κ : Type*} [Finite ι]
    [Finite κ] (b : Basis ι R S) (c : Basis κ S T) :
    (trace R S).comp ((trace S T).restrictScalars R) = trace R T

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
⊢ trace R S ∘ₗ ↑R (trace S T) = trace R T

Tactic:
ext

Result:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x✝ : T
⊢ (trace R S ∘ₗ ↑R (trace S T)) x✝ = (trace R T) x✝

Proof state:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
b : Basis ι R S
c : Basis κ S T
x✝ : T
⊢ (trace R S ∘ₗ ↑R (trace S T)) x✝ = (trace R T) x✝

Tactic:
rw [LinearMap.comp_apply, LinearMap.restrictScalars_apply, trace_trace_of_basis b c]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem exists_of_set' {l : List α} (h : n < l.length) :
    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂

Proof state:
α : Type u_1
n : Nat
a' : α
l : List α
h : n < l.length
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ modify (fun x => a') n l = l₁ ++ a' :: l₂

Tactic:
exact exists_of_modify _ h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a' : α
l : List α
h : n < l.length
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂

Tactic:
rw [set_eq_modify]

Result:
α : Type u_1
n : Nat
a' : α
l : List α
h : n < l.length
⊢ ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ modify (fun x => a') n l = l₁ ++ a' :: l₂