harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Ordmap/Ordset.lean
theorem size_balance' {l x r} (hl : @Sized α l) (hr : Sized r) :
    size (@balance' α l x r) = size l + size r + 1

Proof state:
case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
exact hr.rotateL_size

Result:
no goals

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).size = l.size + r.size + 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r).size =
    l.size + r.size + 1

Tactic:
split_ifs

Result:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝ : l.size + r.size ≤ 1
⊢ (l.node' x r).size = l.size + r.size + 1

case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝¹ : ¬l.size + r.size ≤ 1
h✝ : r.size > delta * l.size
⊢ (l.rotateL x r).size = l.size + r.size + 1

case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : ¬l.size > delta * r.size
⊢ (l.node' x r).size = l.size + r.size + 1

Proof state:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
h✝² : ¬l.size + r.size ≤ 1
h✝¹ : ¬r.size > delta * l.size
h✝ : l.size > delta * r.size
⊢ (l.rotateR x r).size = l.size + r.size + 1

Tactic:
exact hl.rotateR_size

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (l.balance' x r).size = l.size + r.size + 1

Tactic:
unfold balance'

Result:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r).size =
    l.size + r.size + 1
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.mul_div_cancel` for a simpler version assuming `a ≠ 0`, `a ≠ ∞`. -/
protected lemma mul_div_cancel' (ha₀ : a = 0 → b = 0) (ha : a = ∞ → b = 0) : a * (b / a) = b

Proof state:
a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ⊤ → b = 0
⊢ a * (b / a) = b

Tactic:
rw [mul_comm, ENNReal.div_mul_cancel' ha₀ ha]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph_le_beth (o : Ordinal) : ℵ_ o ≤ ℶ_ o

Proof state:
case H₃
o : Ordinal.{u_1}
ho : o.IsLimit
IH : ∀ o' < o, ℵ_ o' ≤ ℶ_ o'
⊢ ⨆ a, ℵ_ ↑a ≤ ⨆ a, ℶ_ ↑a

Tactic:
exact ciSup_mono (bddAbove_of_small _) fun x => IH x.1 x.2

Result:
no goals

Proof state:
case H₃
o : Ordinal.{u_1}
ho : o.IsLimit
IH : ∀ o' < o, ℵ_ o' ≤ ℶ_ o'
⊢ ℵ_ o ≤ ℶ_ o

Tactic:
rw [aleph_limit ho, beth_limit ho]

Result:
case H₃
o : Ordinal.{u_1}
ho : o.IsLimit
IH : ∀ o' < o, ℵ_ o' ≤ ℶ_ o'
⊢ ⨆ a, ℵ_ ↑a ≤ ⨆ a, ℶ_ ↑a

Proof state:
o : Ordinal.{u_1}
⊢ ℵ_ o ≤ ℶ_ o

Tactic:
induction o using limitRecOn with
| H₁ => simp
| H₂ o h =>
  rw [aleph_succ, beth_succ, succ_le_iff]
  exact (cantor _).trans_le (power_le_power_left two_ne_zero h)
| H₃ o ho IH =>
  rw [aleph_limit ho, beth_limit ho]
  exact ciSup_mono (bddAbove_of_small _) fun x => IH x.1 x.2

Result:
no goals

Proof state:
case H₁

⊢ ℵ_ 0 ≤ ℶ_ 0

Tactic:
simp

Result:
no goals

Proof state:
case H₂
o : Ordinal.{u_1}
h : ℵ_ o ≤ ℶ_ o
⊢ ℵ_ (succ o) ≤ ℶ_ (succ o)

Tactic:
rw [aleph_succ, beth_succ, succ_le_iff]

Result:
case H₂
o : Ordinal.{u_1}
h : ℵ_ o ≤ ℶ_ o
⊢ ℵ_ o < 2 ^ ℶ_ o

Proof state:
case H₂
o : Ordinal.{u_1}
h : ℵ_ o ≤ ℶ_ o
⊢ ℵ_ o < 2 ^ ℶ_ o

Tactic:
exact (cantor _).trans_le (power_le_power_left two_ne_zero h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem ofNat_toNat (a : Int) : (a.toNat : Int) = max a 0

Proof state:
a : Int
n : Nat
⊢ ↑(ofNat n).toNat = max (ofNat n) 0

Tactic:
simp

Result:
no goals

Proof state:
a : Int
⊢ ↑a.toNat = max a 0

Tactic:
match a with
| Int.ofNat n => simp
| Int.negSucc n => simp

Result:
no goals

Proof state:
a : Int
n : Nat
⊢ ↑-[n+1].toNat = max -[n+1] 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem integral_sin_mul_sin_mul_cos_pow_eq (hn : 2 ≤ n) (hz : z ≠ 0) :
    (∫ x in (0 : ℝ)..π / 2, Complex.sin (2 * z * x) * sin x * (cos x : ℂ) ^ (n - 1)) =
      (n / (2 * z) * ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) -
        (n - 1) / (2 * z) *
          ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (n - 2)

Proof state:
case h.e'_3.hg
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ IntervalIntegrable (fun x => (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))) volume 0 (π / 2)

Tactic:
apply Continuous.intervalIntegrable

Result:
case h.e'_3.hg.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y => ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
⊢ Continuous fun x => (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2))

Proof state:
case h.e'_8.h
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x => x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
y : ℝ
⊢ ↑(sin y) * ↑(cos y) ^ (n - 1) = Complex.sin ↑y * ((fun x => x ^ (n - 1)) ∘ Complex.cos) ↑y

Tactic:
simp only [Complex.ofReal_sin, Complex.ofReal_cos, Function.comp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem zero_modByMonic (p : R[X]) : 0 %ₘ p = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).2
    else 0) =
    0

Tactic:
by_cases hp : Monic p

Result:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).2
    else 0) =
    0

case neg
R : Type u
inst✝ : Ring R
p : R[X]
hp : ¬p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).2
    else 0) =
    0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if h_1 : p.degree ≤ degree 0 ∧ 0 ≠ 0 then
          let z := C (leadingCoeff 0) * X ^ (natDegree 0 - p.natDegree);
          let_fun _wf := ⋯;
          let dm := (0 - p * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, 0)).2
    else 0) =
    0

Tactic:
dsimp

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).2
    else 0) =
    0

Proof state:
case pos
R : Type u
inst✝ : Ring R
p : R[X]
hp : p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).2
    else 0) =
    0

Tactic:
rw [dif_pos hp, if_neg (mt And.right (not_not_intro rfl)), Prod.snd_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ 0 %ₘ p = 0

Tactic:
unfold modByMonic divModByMonicAux

Result:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (if h : p.Monic then
      (if h_1 : p.degree ≤ degree 0 ∧ 0 ≠ 0 then
          let z := C (leadingCoeff 0) * X ^ (natDegree 0 - p.natDegree);
          let_fun _wf := ⋯;
          let dm := (0 - p * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, 0)).2
    else 0) =
    0

Proof state:
case neg
R : Type u
inst✝ : Ring R
p : R[X]
hp : ¬p.Monic
⊢ (if h : p.Monic then
      (if p.degree ≤ ⊥ ∧ ¬0 = 0 then
          (C 0 * X ^ (0 - p.natDegree) + ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).1,
            ((0 - p * (C 0 * X ^ (0 - p.natDegree))).divModByMonicAux ⋯).2)
        else 0).2
    else 0) =
    0

Tactic:
rw [dif_neg hp]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem uniformIntegrable_finite [Finite ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞)
    (hf : ∀ i, MemLp (f i) p μ) : UniformIntegrable f p μ

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
y : ℝ≥0∞
hy : y ∈ Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ
⊢ y < ⊤

Tactic:
rw [Finset.mem_image] at hy

Result:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
y : ℝ≥0∞
hy : ∃ a ∈ Finset.univ, eLpNorm (f a) p μ = y
⊢ y < ⊤

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
y : ℝ≥0∞
hy : ∃ a ∈ Finset.univ, eLpNorm (f a) p μ = y
⊢ y < ⊤

Tactic:
obtain ⟨i, -, rfl⟩ := hy

Result:
case pos.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i✝ i : ι
⊢ eLpNorm (f i) p μ < ⊤

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst✝ : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ⊤
val✝ : Fintype ι
hι : Nonempty ι
h✝ : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ⊤
C : ℝ≥0∞ := (Finset.image (fun i => eLpNorm (f i) p μ) Finset.univ).max' ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ C

Tactic:
exact Finset.le_max' (α := ℝ≥0∞) _ _ (Finset.mem_image.2 ⟨i, Finset.mem_univ _, rfl⟩)

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem map_restriction {R : Type u} [CommRing R] (p : R[X]) :
    p.restriction.map (algebraMap _ _) = p :=
  ext fun n => by rw [coeff_map, Algebra.algebraMap_ofSubring_apply, coeff_restriction]

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
n : ℕ
⊢ (map (algebraMap (↥(Subring.closure ↑p.coeffs)) R) p.restriction).coeff n = p.coeff n

Tactic:
rw [coeff_map, Algebra.algebraMap_ofSubring_apply, coeff_restriction]

Result:
no goals
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
theorem trans : FaithfullyFlat R M

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
⊢ FaithfullyFlat R M

Tactic:
rw [iff_zero_iff_lTensor_zero]

Result:
R : Type u_1
inst✝⁸ : CommRing R
S : Type u_2
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FaithfullyFlat R S
inst✝ : FaithfullyFlat S M
⊢ Flat R M ∧
    ∀ {N : Type (max u_1 u_3)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u_1 u_3)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), lTensor M f = 0 ↔ f = 0
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem finite_of_discr_bdd_of_isReal :
    {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F} |
      haveI :  NumberField K := @NumberField.mk _ _ inferInstance K.prop
      {w : InfinitePlace K | IsReal w}.Nonempty ∧ |discr K| ≤ N }.Finite

Proof state:
A : Type u_2
inst✝¹ : Field A
inst✝ : CharZero A
N : ℕ
D : ℕ := rankOfDiscrBdd N
B : ℝ≥0 := boundOfDiscBdd N
C : ℕ := ⌈(B ⊔ 1) ^ D * ↑(D.choose (D / 2))⌉₊
x✝¹ : { F // FiniteDimensional ℚ ↥F }
K : IntermediateField ℚ A
hK₀ : FiniteDimensional ℚ ↥K
x✝ : ⟨K, hK₀⟩ ∈ {K | {w | w.IsReal}.Nonempty ∧ |discr ↥↑K| ≤ ↑N}
hK₂ : |discr ↥↑⟨K, hK₀⟩| ≤ ↑N
this✝¹ : CharZero ↥K
this✝ : NumberField ↥K
w₀ : InfinitePlace ↥↑⟨K, hK₀⟩
hw₀ : w₀ ∈ {w | w.IsReal}
this : minkowskiBound (↥K) 1 < ↑(convexBodyLTFactor ↥K) * ↑B
x : 𝓞 ↥K
hx₁ : ℚ⟮↑x⟯ = ⊤
hx₂ : ∀ (w : InfinitePlace ↥K), w ↑x < ↑(B ⊔ 1)
hx : IsIntegral ℤ ((algebraMap (𝓞 ↥K) ↥K) x)
i : ℕ
⊢ ↑(B ⊔ 1) ⊔ 1 = ↑B ⊔ 1

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_interpolate_of_eval_eq {f : F[X]} (hvs : Set.InjOn v s) (degree_f_lt : f.degree < #s)
    (eval_f : ∀ i ∈ s, f.eval (v i) = r i) : f = interpolate s v r

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = r i
⊢ ((interpolate s v) fun i => eval (v i) f) = (interpolate s v) r

Tactic:
exact interpolate_eq_of_values_eq_on _ _ eval_f

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v) r

Tactic:
rw [eq_interpolate hvs degree_f_lt]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = r i
⊢ ((interpolate s v) fun i => eval (v i) f) = (interpolate s v) r
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem Finsupp.sum_sum_index' (h0 : ∀ i, t i 0 = 0) (h1 : ∀ i x y, t i (x + y) = t i x + t i y) :
    (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t

Proof state:
α : Type u_1
ι : Type u_2
A : Type u_4
C : Type u_6
inst✝¹ : AddCommMonoid A
inst✝ : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
⊢ (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t

Tactic:
classical
exact Finset.induction_on s rfl fun a s has ih => by
  simp_rw [Finset.sum_insert has, Finsupp.sum_add_index' h0 h1, ih]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
A : Type u_4
C : Type u_6
inst✝¹ : AddCommMonoid A
inst✝ : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
⊢ (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t

Tactic:
exact Finset.induction_on s rfl fun a s has ih => by
  simp_rw [Finset.sum_insert has, Finsupp.sum_add_index' h0 h1, ih]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
A : Type u_4
C : Type u_6
inst✝¹ : AddCommMonoid A
inst✝ : AddCommMonoid C
t : ι → A → C
s✝ : Finset α
f : α → ι →₀ A
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
a : α
s : Finset α
has : a ∉ s
ih : (∑ x ∈ s, f x).sum t = ∑ x ∈ s, (f x).sum t
⊢ (∑ x ∈ insert a s, f x).sum t = ∑ x ∈ insert a s, (f x).sum t

Tactic:
simp_rw [Finset.sum_insert has, Finsupp.sum_add_index' h0 h1, ih]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem mono_of_isLimitMkIdId (f : X ⟶ Y) (t : IsLimit (mk (𝟙 X) (𝟙 X) rfl : PullbackCone f f)) :
    Mono f :=
  ⟨fun {Z} g h eq => by
    rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl⟩

Proof state:
case mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
val✝ : Z ⟶ (mk (𝟙 X) (𝟙 X) ⋯).pt
eq : (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst) ≫ f = (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd) ≫ f
⊢ val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst = val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
g h : Z ⟶ X
eq : g ≫ f = h ≫ f
⊢ g = h

Tactic:
rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩

Result:
case mk.intro
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
val✝ : Z ⟶ (mk (𝟙 X) (𝟙 X) ⋯).pt
eq : (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst) ≫ f = (val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd) ≫ f
⊢ val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).fst = val✝ ≫ (mk (𝟙 X) (𝟙 X) ⋯).snd
-- Mathlib/Algebra/Ring/Int/Defs.lean
/-- Note this holds in marginally more generality than `Int.cast_mul` -/
lemma cast_mul_eq_zsmul_cast {α : Type*} [AddCommGroupWithOne α] :
    ∀ m n : ℤ, ↑(m * n) = m • (n : α) :=
  fun m ↦ Int.induction_on m (by simp) (fun _ ih ↦ by simp [add_mul, add_zsmul, ih]) fun _ ih ↦ by
    simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]

Proof state:
α : Type u_1
inst✝ : AddCommGroupWithOne α
m : ℤ
x✝ : ℕ
ih : ∀ (n : ℤ), ↑(↑x✝ * n) = ↑x✝ • ↑n
⊢ ∀ (n : ℤ), ↑((↑x✝ + 1) * n) = (↑x✝ + 1) • ↑n

Tactic:
simp [add_mul, add_zsmul, ih]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddCommGroupWithOne α
m : ℤ
⊢ ∀ (n : ℤ), ↑(0 * n) = 0 • ↑n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddCommGroupWithOne α
m : ℤ
x✝ : ℕ
ih : ∀ (n : ℤ), ↑(-↑x✝ * n) = -↑x✝ • ↑n
⊢ ∀ (n : ℤ), ↑((-↑x✝ - 1) * n) = (-↑x✝ - 1) • ↑n

Tactic:
simp only [sub_mul, one_mul, cast_sub, ih, sub_zsmul, one_zsmul, ← sub_eq_add_neg, forall_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_lt_of_lt_sub {a b c : Nat} (h : a < c - b) : a + b < c

Proof state:
case h
a b c : Nat
h : a < 0
hgt : c < b
⊢ a < 0

Tactic:
exact h

Result:
no goals

Proof state:
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ a < 0

Tactic:
rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hgt)] at h

Result:
case h
a b c : Nat
h : a < 0
hgt : c < b
⊢ a < 0

Proof state:
a b c : Nat
h : a < c - b
hle : b ≤ c
this : a + b + 1 ≤ c
⊢ a + b < c

Tactic:
exact this

Result:
no goals

Proof state:
a b c : Nat
h : a < c - b
⊢ b ≤ c

Tactic:
apply Nat.ge_of_not_lt

Result:
case h
a b c : Nat
h : a < c - b
⊢ ¬c < b

Proof state:
a b c : Nat
h : a < c - b
hle : b ≤ c
this : a.succ + b ≤ c
⊢ a + b < c

Tactic:
simp [Nat.succ_add] at this

Result:
a b c : Nat
h : a < c - b
hle : b ≤ c
this : a + b + 1 ≤ c
⊢ a + b < c

Proof state:
a b c : Nat
h : a < c - b
⊢ a + b < c

Tactic:
have hle : b ≤ c := by
  apply Nat.ge_of_not_lt
  intro hgt
  apply Nat.not_lt_zero a
  rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hgt)] at h
  exact h

Result:
a b c : Nat
h : a < c - b
hle : b ≤ c
⊢ a + b < c

Proof state:
a b c : Nat
h : a < c - b
hle : b ≤ c
⊢ a + b < c

Tactic:
have : a.succ + b ≤ c := add_le_of_le_sub hle h

Result:
a b c : Nat
h : a < c - b
hle : b ≤ c
this : a.succ + b ≤ c
⊢ a + b < c

Proof state:
case h
a b c : Nat
h : a < c - b
⊢ ¬c < b

Tactic:
intro hgt

Result:
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ False

Proof state:
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ False

Tactic:
apply Nat.not_lt_zero a

Result:
case h
a b c : Nat
h : a < c - b
hgt : c < b
⊢ a < 0
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma toSpec_base_apply_eq_comap {f} (x : Proj| pbo f) :
    (toSpec 𝒜 f).base x = PrimeSpectrum.comap (mapId 𝒜 (Submonoid.powers_le.mpr x.2))
      (closedPoint (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (ConcreteCategory.hom (toSpec 𝒜 f).base) x =
    (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
show PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x).hom
      (IsLocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) = _

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (PrimeSpectrum.comap (CommRingCat.Hom.hom (awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x)))
      (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) =
    (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (PrimeSpectrum.comap (CommRingCat.Hom.hom (awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x)))
      (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) =
    (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
rw [awayToΓ_ΓToStalk, CommRingCat.hom_comp, PrimeSpectrum.comap_comp]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (mapId 𝒜 ⋯)))).comp
        (PrimeSpectrum.comap
          (CommRingCat.Hom.hom ((«Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv))))
      (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) =
    (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ ((PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (mapId 𝒜 ⋯)))).comp
        (PrimeSpectrum.comap
          (CommRingCat.Hom.hom ((«Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv))))
      (closedPoint ↑((Proj.restrict ⋯).presheaf.stalk x)) =
    (PrimeSpectrum.comap (mapId 𝒜 ⋯)) (closedPoint (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))

Tactic:
exact congr(PrimeSpectrum.comap _ $(@IsLocalRing.comap_closedPoint
  (HomogeneousLocalization.AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) _ _
  ((Proj| pbo f).presheaf.stalk x) _ _ _ (isLocalHom_of_isIso _)))

Result:
no goals