harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
/-- The homogeneous degree bounds the total degree.

See also `MvPolynomial.IsHomogeneous.totalDegree` when `φ` is non-zero. -/
lemma totalDegree_le (hφ : IsHomogeneous φ n) : φ.totalDegree ≤ n

Proof state:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun x e => e) ≤ n

Tactic:
rw [mem_support_iff] at hd

Result:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (d.sum fun x e => e) ≤ n

Proof state:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
⊢ ∀ b ∈ φ.support, (b.sum fun x e => e) ≤ n

Tactic:
intro d hd

Result:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun x e => e) ≤ n

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
⊢ φ.totalDegree ≤ n

Tactic:
apply Finset.sup_le

Result:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
⊢ ∀ b ∈ φ.support, (b.sum fun x e => e) ≤ n

Proof state:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (d.sum fun x e => e) ≤ n

Tactic:
simp_rw [Finsupp.sum, ← hφ hd, weight_apply, Pi.one_apply, smul_eq_mul, mul_one, Finsupp.sum,
  le_rfl]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
Alternative definition of coheight, with the supremum only ranging over those series
that begin at `a`.
-/
lemma coheight_eq_iSup_head_eq (a : α) :
    coheight a = ⨆ (p : LTSeries α) (_ : p.head = a), ↑(p.length)

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (x : RelSeries fun x1 x2 => x1 < x2),
    ⨆ (_ : ({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).head = a),
        ↑({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).length =
      ⨆ (_ : x.last = a), ↑x.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length

Tactic:
apply Equiv.iSup_congr ⟨RelSeries.reverse, RelSeries.reverse, RelSeries.reverse_reverse,
  RelSeries.reverse_reverse⟩

Result:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ∀ (x : RelSeries fun x1 x2 => x1 < x2),
    ⨆ (_ : ({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).head = a),
        ↑({ toFun := RelSeries.reverse, invFun := RelSeries.reverse, left_inv := ⋯, right_inv := ⋯ } x).length =
      ⨆ (_ : x.last = a), ↑x.length

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ coheight a = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length

Tactic:
show height (α := αᵒᵈ) a = ⨆ (p : LTSeries α) (_ : p.head = a), ↑(p.length)

Result:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ height a = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ height a = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length

Tactic:
rw [height_eq_iSup_last_eq]

Result:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_inj' (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : length t₁ = length t₂) : s₁ = s₂ ∧ t₁ = t₂ :=
  append_inj h <| @Nat.add_right_cancel _ t₁.length _ <| by
    let hap := congrArg length h; simp only [length_append, ← hl] at hap; exact hap

Proof state:
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.length = t₂.length
⊢ s₁.length + t₁.length = s₂.length + t₁.length

Tactic:
let hap := congrArg length h

Result:
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.length = t₂.length
hap : (s₁ ++ t₁).length = (s₂ ++ t₂).length := congrArg length h
⊢ s₁.length + t₁.length = s₂.length + t₁.length

Proof state:
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.length = t₂.length
hap : s₁.length + t₁.length = s₂.length + t₁.length
⊢ s₁.length + t₁.length = s₂.length + t₁.length

Tactic:
exact hap

Result:
no goals

Proof state:
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.length = t₂.length
hap : (s₁ ++ t₁).length = (s₂ ++ t₂).length := congrArg length h
⊢ s₁.length + t₁.length = s₂.length + t₁.length

Tactic:
simp only [length_append, ← hl] at hap

Result:
α✝ : Type u_1
s₁ t₁ s₂ t₂ : List α✝
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.length = t₂.length
hap : s₁.length + t₁.length = s₂.length + t₁.length
⊢ s₁.length + t₁.length = s₂.length + t₁.length
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_smul_iff [NormedRing 𝕜] [MulActionWithZero 𝕜 β] [BoundedSMul 𝕜 β] {c : 𝕜}
    (hc : IsUnit c) (f : α → β) : HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ

Proof state:
case intro.mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ → HasFiniteIntegral f μ

Tactic:
intro h

Result:
case intro.mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
h : HasFiniteIntegral (↑c • f) μ
⊢ HasFiniteIntegral f μ

Proof state:
case intro.mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral f μ → HasFiniteIntegral (↑c • f) μ

Tactic:
exact HasFiniteIntegral.smul _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
c : 𝕜
hc : IsUnit c
f : α → β
⊢ HasFiniteIntegral (c • f) μ ↔ HasFiniteIntegral f μ

Tactic:
obtain ⟨c, rfl⟩ := hc

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ ↔ HasFiniteIntegral f μ

Proof state:
case intro.mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
h : HasFiniteIntegral (↑c • f) μ
⊢ HasFiniteIntegral f μ

Tactic:
simpa only [smul_smul, Units.inv_mul, one_smul] using h.smul ((c⁻¹ : 𝕜ˣ) : 𝕜)

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ ↔ HasFiniteIntegral f μ

Tactic:
constructor

Result:
case intro.mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ → HasFiniteIntegral f μ

case intro.mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_5
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral f μ → HasFiniteIntegral (↑c • f) μ
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.balLeft {l : RBNode α} {v : α} {r : RBNode α}
    (lv : l.All (cmpLT cmp · v)) (vr : r.All (cmpLT cmp v ·))
    (hl : l.Ordered cmp) (hr : r.Ordered cmp) : (balLeft l v r).Ordered cmp

Proof state:
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
lv : All (fun x => cmpLT cmp x v) l
hl : Ordered cmp l
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
z✝ : α
c✝ : RBNode α
vr : All (fun x => cmpLT cmp v x) (node red (node black a✝ y✝ b✝) z✝ c✝)
hr : Ordered cmp (node red (node black a✝ y✝ b✝) z✝ c✝)
⊢ Ordered cmp (node red (node black l v a✝) y✝ (b✝.balance2 z✝ c✝.setRed))

Tactic:
have ⟨vy, va, _⟩ := vr.2.1

Result:
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
lv : All (fun x => cmpLT cmp x v) l
hl : Ordered cmp l
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
z✝ : α
c✝ : RBNode α
vr : All (fun x => cmpLT cmp v x) (node red (node black a✝ y✝ b✝) z✝ c✝)
hr : Ordered cmp (node red (node black a✝ y✝ b✝) z✝ c✝)
vy : (fun x => cmpLT cmp v x) y✝
va : All (fun x => cmpLT cmp v x) a✝
right✝ : All (fun x => cmpLT cmp v x) b✝
⊢ Ordered cmp (node red (node black l v a✝) y✝ (b✝.balance2 z✝ c✝.setRed))

Proof state:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (l.balLeft v r)

Tactic:
unfold balLeft

Result:
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp
    (match l with
    | node red a x b => node red (node black a x b) v r
    | l =>
      match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r)
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma norm_prime_cpow_le_one_half (p : Nat.Primes) {s : ℂ} (hs : 1 < s.re) :
    ‖(p : ℂ) ^ (-s)‖ ≤ 1 / 2

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ (-s).re ≤ 0

Tactic:
rw [neg_re]

Result:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≤ 0

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≠ 0

Tactic:
linarith only [hs]

Result:
no goals

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ 2 ^ (-s).re ≤ 2 ^ (-1)

Tactic:
exact Real.rpow_le_rpow_of_exponent_le one_le_two <| (neg_lt_neg hs).le

Result:
no goals

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≤ 0

Tactic:
linarith only [hs]

Result:
no goals

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ 2 ^ (-s).re ≤ 1 / 2

Tactic:
rw [one_div, ← Real.rpow_neg_one]

Result:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ 2 ^ (-s).re ≤ 2 ^ (-1)

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ↑↑p ^ (-s).re ≤ 1 / 2

Tactic:
refine (Real.rpow_le_rpow_of_nonpos zero_lt_two (Nat.cast_le.mpr p.prop.two_le) <|
  by rw [neg_re]; linarith only [hs]).trans ?_

Result:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ 2 ^ (-s).re ≤ 1 / 2

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ‖↑↑p ^ (-s)‖ ≤ 1 / 2

Tactic:
rw [norm_natCast_cpow_of_re_ne_zero p <| by rw [neg_re]; linarith only [hs]]

Result:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ ↑↑p ^ (-s).re ≤ 1 / 2

Proof state:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ (-s).re ≠ 0

Tactic:
rw [neg_re]

Result:
p : Nat.Primes
s : ℂ
hs : 1 < s.re
⊢ -s.re ≠ 0
-- Mathlib/Data/PNat/Basic.lean
theorem dvd_iff' {k m : ℕ+} : k ∣ m ↔ mod m k = k

Proof state:
case pos
k m : ℕ+
h : m.mod k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0

Tactic:
exact h'

Result:
no goals

Proof state:
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ m.mod k = k

Tactic:
rw [Nat.dvd_iff_mod_eq_zero]

Result:
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ m.mod k = k

Proof state:
case mp.a
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑(m.mod k) = ↑k

Tactic:
rw [mod_coe, if_pos h]

Result:
no goals

Proof state:
case neg
k m : ℕ+
h : m.mod k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0

Tactic:
replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h

Result:
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑(m.mod k) = ↑k
⊢ ↑m % ↑k = 0

Proof state:
case mpr
k m : ℕ+
h : m.mod k = k
⊢ ↑m % ↑k = 0

Tactic:
by_cases h' : (m : ℕ) % (k : ℕ) = 0

Result:
case pos
k m : ℕ+
h : m.mod k = k
h' : ↑m % ↑k = 0
⊢ ↑m % ↑k = 0

case neg
k m : ℕ+
h : m.mod k = k
h' : ¬↑m % ↑k = 0
⊢ ↑m % ↑k = 0

Proof state:
case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → m.mod k = k

Tactic:
intro h

Result:
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ m.mod k = k

Proof state:
k m : ℕ+
⊢ k ∣ m ↔ m.mod k = k

Tactic:
rw [dvd_iff]

Result:
k m : ℕ+
⊢ ↑k ∣ ↑m ↔ m.mod k = k

Proof state:
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑(m.mod k) = ↑k
⊢ ↑m % ↑k = 0

Tactic:
rw [mod_coe, if_neg h'] at h

Result:
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0

Proof state:
k m : ℕ+
⊢ ↑m % ↑k = 0 ↔ m.mod k = k

Tactic:
constructor

Result:
case mp
k m : ℕ+
⊢ ↑m % ↑k = 0 → m.mod k = k

case mpr
k m : ℕ+
⊢ m.mod k = k → ↑m % ↑k = 0

Proof state:
case neg
k m : ℕ+
h' : ¬↑m % ↑k = 0
h : ↑m % ↑k = ↑k
⊢ ↑m % ↑k = 0

Tactic:
exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

Result:
no goals

Proof state:
case mp
k m : ℕ+
h : ↑m % ↑k = 0
⊢ m.mod k = k

Tactic:
apply PNat.eq

Result:
case mp.a
k m : ℕ+
h : ↑m % ↑k = 0
⊢ ↑(m.mod k) = ↑k

Proof state:
case mpr
k m : ℕ+
⊢ m.mod k = k → ↑m % ↑k = 0

Tactic:
intro h

Result:
case mpr
k m : ℕ+
h : m.mod k = k
⊢ ↑m % ↑k = 0
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem isIrreducible_zeroLocus_iff_of_radical (I : Ideal R) (hI : I.IsRadical) :
    IsIrreducible (zeroLocus (I : Set R)) ↔ I.IsPrime

Proof state:
case h₂
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
trans ∀ x y : Ideal R, Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y)

Result:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsPreirreducible (zeroLocus ↑I) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Proof state:
case mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ {x y : R}, x * y ∈ I → x ∉ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : x ∉ I
y : R
hy : y ∈ t
⊢ y ∈ I

Tactic:
exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h :
  ∀ (x y : Ideal R),
    zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

Tactic:
exact h x y

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂

Tactic:
rintro h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩

Result:
case mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h :
  ∀ (x y : Ideal R),
    zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Proof state:
case h₁
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (zeroLocus ↑I).Nonempty ↔ I ≠ ⊤

Tactic:
rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_singleton : infDist x {y} = dist x y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ infDist x {y} = dist x y

Tactic:
simp [infDist, dist_edist]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem ge_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f)
    (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hx : 0 < x) (hn : n ≠ 0) :
    f 1 + logGammaSeq x n ≤ f x

Proof state:
case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) = f 1 + log ↑n ! + x * log ↑n

Tactic:
ring

Result:
no goals

Proof state:
case refine_2
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ 2 ≤ n + 1

Tactic:
omega

Result:
no goals

Proof state:
case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ n + 1 ≠ 0

Tactic:
exact Nat.succ_ne_zero _

Result:
no goals

Proof state:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + ↑m)) ≤ f x

Tactic:
rw [← add_sub_assoc, sub_le_iff_le_add, ← f_add_nat_eq (@hf_feq) hx, add_comm x _]

Result:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) ≤ f (↑(n + 1) + x)

Proof state:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) ≤ f (↑(n + 1) + x)

Tactic:
refine le_trans (le_of_eq ?_) (f_add_nat_ge hf_conv @hf_feq ?_ hx)

Result:
case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) = f ↑(n + 1) + x * log (↑(n + 1) - 1)

case refine_2
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ 2 ≤ n + 1

Proof state:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + logGammaSeq x n ≤ f x

Tactic:
dsimp [logGammaSeq]

Result:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + ↑m)) ≤ f x

Proof state:
case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) = f ↑(n + 1) + x * log (↑(n + 1) - 1)

Tactic:
rw [f_nat_eq @hf_feq, Nat.add_sub_cancel, Nat.cast_add_one, add_sub_cancel_right]

Result:
case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) = f 1 + log ↑n ! + x * log ↑n

case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ n + 1 ≠ 0
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem isCycle_cycleRange {n : ℕ} [NeZero n] {i : Fin n} (h0 : i ≠ 0) :
    IsCycle (cycleRange i)

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin n
h0 : i ≠ 0
⊢ i.cycleRange.IsCycle

Tactic:
obtain ⟨i, hi⟩ := i

Result:
case mk
n : ℕ
inst✝ : NeZero n
i : ℕ
hi : i < n
h0 : ⟨i, hi⟩ ≠ 0
⊢ ⟨i, hi⟩.cycleRange.IsCycle

Proof state:
case mk.zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.IsCycle

Tactic:
exact (h0 rfl).elim

Result:
no goals

Proof state:
case mk.succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.IsCycle

Tactic:
exact isCycle_finRotate.extendDomain _

Result:
no goals

Proof state:
case mk
n : ℕ
inst✝ : NeZero n
i : ℕ
hi : i < n
h0 : ⟨i, hi⟩ ≠ 0
⊢ ⟨i, hi⟩.cycleRange.IsCycle

Tactic:
cases i

Result:
case mk.zero
n : ℕ
inst✝ : NeZero n
hi : 0 < n
h0 : ⟨0, hi⟩ ≠ 0
⊢ ⟨0, hi⟩.cycleRange.IsCycle

case mk.succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.IsCycle
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem exists_iUnion_eq_diff (π : Prepartition I) :
    ∃ π' : Prepartition I, π'.iUnion = ↑I \ π.iUnion

Proof state:
case h
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ((splitMany I s).filter fun J => ¬↑J ⊆ π.iUnion).iUnion = ↑I \ π.iUnion

Tactic:
simp [← hs]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
⊢ ∃ π', π'.iUnion = ↑I \ π.iUnion

Tactic:
rcases π.eventually_splitMany_inf_eq_filter.exists with ⟨s, hs⟩

Result:
case intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ∃ π', π'.iUnion = ↑I \ π.iUnion

Proof state:
case intro
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ∃ π', π'.iUnion = ↑I \ π.iUnion

Tactic:
use (splitMany I s).filter fun J => ¬(J : Set (ι → ℝ)) ⊆ π.iUnion

Result:
case h
ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = (splitMany I s).filter fun J => ↑J ⊆ π.iUnion
⊢ ((splitMany I s).filter fun J => ¬↑J ⊆ π.iUnion).iUnion = ↑I \ π.iUnion
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem exists_pos_measure_of_cover [Countable ι] {U : ι → Set α} (hU : ⋃ i, U i = univ)
    (hμ : μ ≠ 0) : ∃ i, 0 < μ (U i)

Proof state:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ = 0

Tactic:
rw [← measure_univ_eq_zero, ← hU]

Result:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ (⋃ i, U i) = 0

Proof state:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
hμ : μ ≠ 0
⊢ ∃ i, 0 < μ (U i)

Tactic:
contrapose! hμ with H

Result:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ = 0

Proof state:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ (⋃ i, U i) = 0

Tactic:
exact measure_iUnion_null fun i => nonpos_iff_eq_zero.1 (H i)

Result:
no goals