awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ hA.eigenvalues) *
        (↑(star hA.eigenvectorUnitary) : Matrix n n 𝕜)).rank =
    (diagonal hA.eigenvalues).rank

Tactic:
simp [-isUnit_iff_ne_zero, -coe_star, rank_diagonal]

Premises used: isUnit_iff_ne_zero, Matrix.rank_diagonal, Unitary.coe_star
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
rw : (diagonal hA.eigenvalues).rank = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }
rw₁ rw₂ : Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 } = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }
⊢ A.rank = Fintype.card.{u_2} { i : n // hA.eigenvalues i ≠ 0 }

Tactic:
rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]

Premises used: Matrix.IsHermitian.rank_eq_rank_diagonal, Matrix.rank_diagonal
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : 𝕜
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [hA.spectral_theorem]

Premises used: Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : 𝕜
conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x ∈ spectrum 𝕜 A ↔ Membership.mem (γ := Set 𝕜) (RCLike.ofReal '' Set.range hA.eigenvalues) x

Tactic:
conv_lhs => rw [hA.spectral_theorem]

Premises used: Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : ℝ
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [hA.spectral_theorem, ← spectrum.algebraMap_mem_iff 𝕜]

Premises used: spectrum.algebraMap_mem_iff, Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : ℝ
conv_lhs : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x ∈ spectrum ℝ A ↔ x ∈ Set.range hA.eigenvalues

Tactic:
conv_lhs => rw [hA.spectral_theorem, ← spectrum.algebraMap_mem_iff 𝕜]

Premises used: spectrum.algebraMap_mem_iff, Matrix.IsHermitian.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : ℝ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
h : A = 0
h₁ : ∀ (x : n), hA.eigenvalues x = 0 x
⊢ hA.eigenvalues = 0

Tactic:
ext
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
h : A = 0
x : n
⊢ hA.eigenvalues x = 0 x

Tactic:
simp [h, eigenvalues_eq]

Premises used: Matrix.IsHermitian.eigenvalues_eq
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
refine : ∀ (h : hA.eigenvalues = 0), A = 0
⊢ hA.eigenvalues = 0 ↔ A = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by ext; simp [h, eigenvalues_eq]⟩
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
contrapose : ∀ (h_ne : hA.eigenvalues = 0), A = 0
⊢ hA.eigenvalues ≠ 0

Tactic:
contrapose h_ne
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := hA.spectral_theorem
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : hA.eigenvalues = 0
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := n → 𝕜) (Function.const n 0) fun (x : n) ↦ 0

Tactic:
rfl
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
⊢ hA.eigenvalues ≠ 0

Tactic:
have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
obtain : ∀ (i : n) (hi : hA.eigenvalues i ≠ 0 i), ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp this

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
i : n
hi : hA.eigenvalues i ≠ 0 i
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
⟨_, _, hi, (ofLp_eq_zero 2).ne.2 <| hA.eigenvectorBasis.orthonormal.ne_zero i,
    hA.mulVec_eigenvectorBasis i⟩

Premises used: Iff.mpr, Orthonormal.ne_zero, WithLp.ofLp_eq_zero, Matrix.IsHermitian.eigenvectorBasis, OrthonormalBasis.orthonormal, And.intro, Iff.ne, Exists.intro, OfNat.ofNat, Matrix.IsHermitian.mulVec_eigenvectorBasis
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
this : hA.eigenvalues ≠ 0
i : n
hi : hA.eigenvalues i ≠ 0 i
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
exact ⟨_, _, hi, (ofLp_eq_zero 2).ne.2 <| hA.eigenvectorBasis.orthonormal.ne_zero i,
    hA.mulVec_eigenvectorBasis i⟩
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
hA : A.IsHermitian
h_ne : A ≠ 0
have : hA.eigenvalues ≠ 0
have₁ : ∀ (this : hA.eigenvalues ≠ 0), ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have₂ : hA.eigenvalues ≠ 0
have₃ have₄ : ∀ (this : hA.eigenvalues ≠ 0), ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
have₅ :
  ∀ (this : hA.eigenvalues ≠ 0) (i : n) (hi : hA.eigenvalues i ≠ 0 i),
    ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v
⊢ ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v

Tactic:
classical
  have : hA.eigenvalues ≠ 0 := by
    contrapose h_ne
    have := hA.spectral_theorem
    rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0),
      diagonal_zero, map_zero] at this
  obtain ⟨i, hi⟩ := Function.ne_iff.mp this
  exact ⟨_, _, hi, (ofLp_eq_zero 2).ne.2 <| hA.eigenvectorBasis.orthonormal.ne_zero i,
    hA.mulVec_eigenvectorBasis i⟩
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ A.trace = ∑ i : n, (↑(hA.eigenvalues i) : 𝕜)

Tactic:
simp [trace_eq_sum_roots_charpoly_of_splits hA.splits_charpoly, hA.roots_charpoly_eq_eigenvalues]

Premises used: Matrix.IsHermitian.roots_charpoly_eq_eigenvalues, Matrix.IsHermitian.splits_charpoly, Matrix.trace_eq_sum_roots_charpoly_of_splits
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
pos : ∀ (A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0), LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
neg : ∀ (A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0), LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
by_cases! A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
pos : ∀ (i : ι) (his : i ∈ s) (hzi : z i = 0) (hwi : w i ≠ 0), LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
rcases A with ⟨i, his, hzi, hwi⟩
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
pos : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)
pos₁ : z i ^ w i = 0
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
rw [prod_eq_zero his]

Premises used: Finset.prod_eq_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)

Tactic:
sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)

Premises used: mul_nonneg, Finset.sum_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)

Tactic:
exact sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)

Premises used: mul_nonneg, Finset.sum_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
pos : HPow.hPow (α := ℝ) 0 (w i) = 0
⊢ z i ^ w i = 0

Tactic:
rw [hzi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ HPow.hPow (α := ℝ) 0 (w i) = 0

Tactic:
zero_rpow hwi

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ HPow.hPow (α := ℝ) 0 (w i) = 0

Tactic:
exact zero_rpow hwi

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
⊢ rexp (∑ i ∈ s, w i • log (z i)) ≤ ∑ i ∈ s, w i • rexp (log (z i))

Tactic:
have := convexOn_exp.map_sum_le hw hw' fun i _ => Set.mem_univ <| log (z i)
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : rexp (∑ i ∈ s, w i • log (z i)) ≤ ∑ i ∈ s, w i • rexp (log (z i))
⊢ LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))

Tactic:
simp only [exp_sum, smul_eq_mul, mul_comm (w _) (log _)] at this

Premises used: Real.log, mul_comm, smul_eq_mul, Real.exp_sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
⊢ LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))

Tactic:
this
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
h : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))
h₁ : Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
convert! this using 1
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
h : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
h : ∀ x ∈ s, w x * z x = w x * rexp (log (z x))
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
h : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
h₁ : ∀ x ∈ s, w x * z x = w x * rexp (log (z x))
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
convert! this using 1 <;> [apply prod_congr rfl; apply sum_congr rfl]

Premises used: Finset.prod_congr, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
h : ∀ (hz : 0 = z i), z i ^ w i = rexp (log (z i) * w i)
h₁ : ∀ (hz : 0 < z i), z i ^ w i = rexp (log (z i) * w i)
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
rcases eq_or_lt_of_le (hz i hi) with hz | hz

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz_1 : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
simp [A i hi hz.symm]

Premises used: Eq.symm
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz_1 : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
rpow_def_of_pos hz _

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz_1 : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
exact rpow_def_of_pos hz _

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
h : ∀ (hz : 0 = z i), w i * z i = w i * rexp (log (z i))
h₁ : ∀ (hz : 0 < z i), w i * z i = w i * rexp (log (z i))
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
rcases eq_or_lt_of_le (hz i hi) with hz | hz

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz_1 : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
simp [A i hi hz.symm]

Premises used: Eq.symm
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz_1 : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
this : LE.le (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
i : ι
hi : i ∈ s
hz : 0 < z i
h h₁ : w i * z i = w i * z i
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
rw [exp_log hz]

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ LE.le (α := ℝ) (∏ i ∈ s, HPow.hPow (β := ℝ) (z i) ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i))
    (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i * z i)

Tactic:
geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz

Premises used: HDiv.hDiv, Finset.sum, Real.geom_mean_le_arith_mean_weighted
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)
h₁ : HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
convert_1 : ∀ i ∈ s, LE.le (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)
convert_2 : Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ ≤
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)

Tactic:
convert! geom_mean_le_arith_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z ?_ ?_ hz using 2

Premises used: HDiv.hDiv, Finset.sum, Real.geom_mean_le_arith_mean_weighted
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : Eq (α := ℝ) (∏ i ∈ s, HPow.hPow (β := ℝ) (z i ^ w i) (∑ i ∈ s, w i)⁻¹) (∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i))
⊢ HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹ = ∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i)

Tactic:
rw [← finsetProd_rpow _ _ (fun i hi => rpow_nonneg (hz _ hi) _) _]

Premises used: Real.rpow_nonneg, Real.finsetProd_rpow
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ Eq (α := ℝ) (∏ i ∈ s, HPow.hPow (β := ℝ) (z i ^ w i) (∑ i ∈ s, w i)⁻¹) (∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i))

Tactic:
Finset.prod_congr rfl (fun _ ih => ?_)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ (x : ι) (ih : x ∈ s), HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x / ∑ i ∈ s, w i)
⊢ Eq (α := ℝ) (∏ i ∈ s, HPow.hPow (β := ℝ) (z i ^ w i) (∑ i ∈ s, w i)⁻¹) (∏ i ∈ s, z i ^ (w i / ∑ i ∈ s, w i))

Tactic:
refine Finset.prod_congr rfl (fun _ ih => ?_)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
x : ι
ih : x ∈ s
h : HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x * (∑ i ∈ s, w i)⁻¹)
h₁ h₂ : HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹
⊢ HPow.hPow (β := ℝ) (z x ^ w x) (∑ i ∈ s, w i)⁻¹ = z x ^ (w x / ∑ i ∈ s, w i)

Tactic:
rw [div_eq_mul_inv, rpow_mul (hz _ ih)]

Premises used: div_eq_mul_inv, Real.rpow_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ * z x
h₁ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * ((∑ i ∈ s, w i)⁻¹ * z x)
h₂ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = ∑ x ∈ s, w x * (z x * (∑ i ∈ s, w i)⁻¹)
h₃ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = ∑ x ∈ s, w x * z x * (∑ i ∈ s, w i)⁻¹
h₄ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i

Tactic:
simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]

Premises used: mul_assoc, div_eq_mul_inv, mul_comm, Finset.sum_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∀ i ∈ s, LE.le (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)

Tactic:
fun _ hi => div_nonneg (hw _ hi) (le_of_lt hw')

Premises used: le_of_lt, div_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∀ i ∈ s, LE.le (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)

Tactic:
exact fun _ hi => div_nonneg (hw _ hi) (le_of_lt hw')

Premises used: le_of_lt, div_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
convert_2 : HMul.hMul (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i)⁻¹ = 1
⊢ Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1

Tactic:
simp_rw [div_eq_mul_inv, ← Finset.sum_mul]

Premises used: div_eq_mul_inv, Finset.sum_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
linarith : Eq (α := ℝ) (∑ i ∈ s, w i) 0 → HSub.hSub (α := ℝ) 0 (∑ i ∈ s, w i) + HSub.hSub (α := ℝ) (∑ i ∈ s, w i) 0 = 0
⊢ Ne (α := ℝ) (∑ i ∈ s, w i) 0

Tactic:
linarith
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ HMul.hMul (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i)⁻¹ = 1

Tactic:
exact mul_inv_cancel₀ (by linarith)

Premises used: mul_inv_cancel₀