harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addZ_smul (P Q : Fin 3 → R) (u v : R) :
    W'.addZ (u • P) (v • Q) = (u * v) ^ 2 * W'.addZ P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q z) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P z) +
                        (u * P y) ^ 2 * (v * Q z) ^ 2 -
                      (v * Q y) ^ 2 * (u * P z) ^ 2 +
                    W'.a₁ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
                  W'.a₁ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 -
                W'.a₂ * (u * P x) ^ 2 * (v * Q z) ^ 2 +
              W'.a₂ * (v * Q x) ^ 2 * (u * P z) ^ 2 +
            W'.a₃ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
          W'.a₃ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) -
        W'.a₄ * (u * P x) * (u * P z) * (v * Q z) ^ 2 +
      W'.a₄ * (v * Q x) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
                      W'.a₁ * P x * P y * Q z ^ 2 -
                    W'.a₁ * Q x * Q y * P z ^ 2 -
                  W'.a₂ * P x ^ 2 * Q z ^ 2 +
                W'.a₂ * Q x ^ 2 * P z ^ 2 +
              W'.a₃ * P y * P z * Q z ^ 2 -
            W'.a₃ * Q y * P z ^ 2 * Q z -
          W'.a₄ * P x * P z * Q z ^ 2 +
        W'.a₄ * Q x * P z ^ 2 * Q z)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.addZ (u • P) (v • Q) = (u * v) ^ 2 * W'.addZ P Q

Tactic:
simp only [addZ, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q z) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P z) +
                        (u * P y) ^ 2 * (v * Q z) ^ 2 -
                      (v * Q y) ^ 2 * (u * P z) ^ 2 +
                    W'.a₁ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
                  W'.a₁ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 -
                W'.a₂ * (u * P x) ^ 2 * (v * Q z) ^ 2 +
              W'.a₂ * (v * Q x) ^ 2 * (u * P z) ^ 2 +
            W'.a₃ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
          W'.a₃ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) -
        W'.a₄ * (u * P x) * (u * P z) * (v * Q z) ^ 2 +
      W'.a₄ * (v * Q x) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-3 * P x ^ 2 * Q x * Q z + 3 * P x * Q x ^ 2 * P z + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * P z ^ 2 +
                      W'.a₁ * P x * P y * Q z ^ 2 -
                    W'.a₁ * Q x * Q y * P z ^ 2 -
                  W'.a₂ * P x ^ 2 * Q z ^ 2 +
                W'.a₂ * Q x ^ 2 * P z ^ 2 +
              W'.a₃ * P y * P z * Q z ^ 2 -
            W'.a₃ * Q y * P z ^ 2 * Q z -
          W'.a₄ * P x * P z * Q z ^ 2 +
        W'.a₄ * Q x * P z ^ 2 * Q z)
-- Mathlib/Data/Nat/Bits.lean
lemma bodd_bit (b n) : bodd (bit b n) = b

Proof state:
b : Bool
n : ℕ
⊢ (2 * n + b.toNat).bodd = b

Tactic:
simp only [Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul, bodd_succ, bodd_zero, Bool.not_false,
  Bool.not_true, Bool.and_false, Bool.xor_false]

Result:
b : Bool
n : ℕ
⊢ b.toNat.bodd = b

Proof state:
b : Bool
n : ℕ
⊢ (bit b n).bodd = b

Tactic:
rw [bit_val]

Result:
b : Bool
n : ℕ
⊢ (2 * n + b.toNat).bodd = b

Proof state:
b : Bool
n : ℕ
⊢ b.toNat.bodd = b

Tactic:
cases b <;> cases bodd n <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem interpolate_one (hvs : Set.InjOn v s) (hs : s.Nonempty) : interpolate s v 1 = 1

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ (interpolate s v) 1 = 1

Tactic:
simp_rw [interpolate_apply, Pi.one_apply, map_one, one_mul]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∑ x ∈ s, Lagrange.basis s v x = 1

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
hvs : Set.InjOn v ↑s
hs : s.Nonempty
⊢ ∑ x ∈ s, Lagrange.basis s v x = 1

Tactic:
exact sum_basis hvs hs

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma term_welldef {n : ℕ} (hn : 0 < n) {s : ℝ} (hs : 0 < s) :
    IntervalIntegrable (fun x : ℝ ↦ (x - n) / x ^ (s + 1)) volume n (n + 1)

Proof state:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntervalIntegrable (fun x => (x - ↑n) / x ^ (s + 1)) volume (↑n) (↑n + 1)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith)]

Result:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntegrableOn (fun x => (x - ↑n) / x ^ (s + 1)) (Icc (↑n) (↑n + 1)) volume

Proof state:
case refine_1
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ ContinuousAt (fun x => x - ↑n) x

Tactic:
fun_prop

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ 0 ≤ s + 1

Tactic:
linarith

Result:
no goals

Proof state:
case refine_3
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ x ^ (s + 1) ≠ 0

Tactic:
exact (rpow_pos_of_pos ((Nat.cast_pos.mpr hn).trans_le hx.1) _).ne'

Result:
no goals

Proof state:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntegrableOn (fun x => (x - ↑n) / x ^ (s + 1)) (Icc (↑n) (↑n + 1)) volume

Tactic:
refine (continuousOn_of_forall_continuousAt fun x hx ↦ ContinuousAt.div ?_ ?_ ?_).integrableOn_Icc

Result:
case refine_1
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ ContinuousAt (fun x => x - ↑n) x

case refine_2
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ ContinuousAt (fun x => x ^ (s + 1)) x

case refine_3
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ x ^ (s + 1) ≠ 0

Proof state:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ ↑n ≤ ↑n + 1

Tactic:
linarith

Result:
no goals

Proof state:
case refine_2
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n) (↑n + 1)
⊢ ContinuousAt (fun x => x ^ (s + 1)) x

Tactic:
apply continuousAt_id.rpow_const (Or.inr <| by linarith)

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_add (f g : M₁ →ₗ[R] M₂) :
    (f + g).toMvPolynomial b₁ b₂ = f.toMvPolynomial b₁ b₂ + g.toMvPolynomial b₁ b₂

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
⊢ toMvPolynomial b₁ b₂ (f + g) = toMvPolynomial b₁ b₂ f + toMvPolynomial b₁ b₂ g

Tactic:
unfold toMvPolynomial

Result:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
⊢ (fun i => ((toMatrix b₁ b₂) (f + g)).toMvPolynomial i) =
    (fun i => ((toMatrix b₁ b₂) f).toMvPolynomial i) + fun i => ((toMatrix b₁ b₂) g).toMvPolynomial i

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
⊢ (fun i => ((toMatrix b₁ b₂) (f + g)).toMvPolynomial i) =
    (fun i => ((toMatrix b₁ b₂) f).toMvPolynomial i) + fun i => ((toMatrix b₁ b₂) g).toMvPolynomial i

Tactic:
simp only [map_add, Matrix.toMvPolynomial_add]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp]
lemma insidePart_nest : p.nest.insidePart = p

Proof state:
case h.e'_2.h.e'_1
p : DyckWord
⊢ ↑(p.nest.take ((↑p).length + 1 + 1) ⋯) = ↑p.nest

Tactic:
apply take_of_length_le

Result:
case h.e'_2.h.e'_1.h
p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1

Proof state:
case h.e'_2.h.e'_1.h
p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_2.h.e'_1
p : DyckWord
⊢ p.nest.take ((↑p).length + 1 + 1) ⋯ = p.nest

Tactic:
rw [DyckWord.ext_iff]

Result:
case h.e'_2.h.e'_1
p : DyckWord
⊢ ↑(p.nest.take ((↑p).length + 1 + 1) ⋯) = ↑p.nest

Proof state:
case h.e'_2.h.e'_1.h
p : DyckWord
⊢ (↑p.nest).length ≤ (↑p).length + 1 + 1

Tactic:
simp_rw [nest, length_append, length_singleton]

Result:
case h.e'_2.h.e'_1.h
p : DyckWord
⊢ 1 + (↑p).length + 1 ≤ (↑p).length + 1 + 1

Proof state:
p : DyckWord
⊢ p.nest.insidePart = p

Tactic:
simp_rw [insidePart, nest_ne_zero, dite_false, firstReturn_nest]

Result:
p : DyckWord
⊢ (p.nest.take ((↑p).length + 1 + 1) ⋯).denest ⋯ = p

Proof state:
p : DyckWord
⊢ (p.nest.take ((↑p).length + 1 + 1) ⋯).denest ⋯ = p

Tactic:
convert p.denest_nest

Result:
case h.e'_2.h.e'_1
p : DyckWord
⊢ p.nest.take ((↑p).length + 1 + 1) ⋯ = p.nest
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma u₄_eq_one_or_neg_one : S.u₄ = 1 ∨ S.u₄ = -1

Proof state:
case hcong.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
⊢ ∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n

Tactic:
rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd hζ S.lambda_not_dvd_Y with
  HY | HY <;> rcases lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd
    hζ S.lambda_not_dvd_Z with HZ | HZ <;> replace HY := this.trans HY <;> replace HZ :=
    this.trans HZ <;> rcases HY with ⟨Y, hY⟩ <;> rcases HZ with ⟨Z, hZ⟩

Result:
case hcong.intro.inl.inl.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n

case hcong.intro.inl.inr.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 - 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n

case hcong.intro.inr.inl.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 - 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n

case hcong.intro.inr.inr.intro.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX :
  ↑(FermatLastTheoremForThreeGen.Solution.u₅ S) *
      (λ ^ (S.multiplicity - 1) * FermatLastTheoremForThreeGen.Solution.X S) ^ 3 =
    λ ^ 2 * X
Y : 𝓞 K
hY : FermatLastTheoremForThreeGen.Solution.Y S ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : FermatLastTheoremForThreeGen.Solution.Z S ^ 3 + 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑(FermatLastTheoremForThreeGen.Solution.u₄ S) - ↑n
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem support_symmDiff_support_subset_support_add [DecidableEq σ] (p q : MvPolynomial σ R) :
    p.support ∆ q.support ⊆ (p + q).support

Proof state:
case hs
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊆ (p + q).support

Tactic:
exact support_sdiff_support_subset_support_add p q

Result:
no goals

Proof state:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (q + p).support

Tactic:
exact support_sdiff_support_subset_support_add q p

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support

Tactic:
apply Finset.union_subset

Result:
case hs
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊆ (p + q).support

case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (p + q).support

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support ∆ q.support ⊆ (p + q).support

Tactic:
rw [symmDiff_def, Finset.sup_eq_union]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ∪ q.support \ p.support ⊆ (p + q).support

Proof state:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (p + q).support

Tactic:
rw [add_comm]

Result:
case a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ q.support \ p.support ⊆ (q + p).support
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero {p : MvPolynomial σ R} :
    IsWeightedHomogeneous w p 0 ↔ p.weightedTotalDegree w = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ s ∈ p.support, (weight w) s = 0

Tactic:
apply forall_congr'

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ), coeff a p ≠ 0 → (weight w) a = 0 ↔ a ∈ p.support → (weight w) a = 0

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ), coeff a p ≠ 0 → (weight w) a = 0 ↔ a ∈ p.support → (weight w) a = 0

Tactic:
intro m

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → (weight w) m = 0 ↔ m ∈ p.support → (weight w) m = 0

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
m : σ →₀ ℕ
⊢ coeff m p ≠ 0 → (weight w) m = 0 ↔ m ∈ p.support → (weight w) m = 0

Tactic:
rw [mem_support_iff]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous w p 0 ↔ weightedTotalDegree w p = 0

Tactic:
rw [weightedTotalDegree, ← bot_eq_zero, Finset.sup_eq_bot_iff, bot_eq_zero, IsWeightedHomogeneous]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : LinearOrderedAddCommMonoid M
inst✝ : CanonicallyOrderedAdd M
w : σ → M
p : MvPolynomial σ R
⊢ (∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ s ∈ p.support, (weight w) s = 0
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toBasicOpen_surjective (f : R) : Function.Surjective (toBasicOpen R f)

Proof state:
case h.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ y ∈ PrimeSpectrum.basicOpen (f ^ (n + 1))

Tactic:
rw [PrimeSpectrum.basicOpen_pow f (n + 1) (by omega)]

Result:
case h.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ y ∈ PrimeSpectrum.basicOpen f

Proof state:
case h.h.mk.hv
R : Type u
inst✝ : CommRing R
f : R
s : ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen f)))
ι : Type u := ↥(PrimeSpectrum.basicOpen f)
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ PrimeSpectrum.basicOpen f
ah_ha : ∀ i ∈ t, ∀ j ∈ t, a i * h j = h i * a j
s_eq :
  ∀ i ∈ t,
    (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s =
      const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯
ht_cover : ↑(PrimeSpectrum.basicOpen f) ⊆ ⋃ i ∈ t, ↑(PrimeSpectrum.basicOpen (h i))
n : ℕ
b : ι →₀ R
b_supp : b ∈ Finsupp.supported R R ↑t
hb : ∑ i ∈ t, b i * h i = f ^ (n + 1)
tt : Type u := ↑↑t
i : ι
hi : i ∈ ↑t
y : ↑(PrimeSpectrum.Top R)
hy : y ∈ PrimeSpectrum.basicOpen (h i)
⊢ y ∈ PrimeSpectrum.basicOpen f

Tactic:
exact (leOfHom (iDh i) :) hy

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive] lemma one_mem_pow (hs : 1 ∈ s) : 1 ∈ s ^ n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
simpa using pow_mem_pow hs

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem mvPolynomial_aeval_of_surjective_of_closure [AddCommMonoid M] [CommSemiring R] {S : Set M}
    (hS : closure S = ⊤) :
    Function.Surjective
      (MvPolynomial.aeval fun s : S => of' R M ↑s : MvPolynomial S R → R[M])

Proof state:
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : MvPolynomial (↑S) R
⊢ ∃ a,
    (MvPolynomial.aeval fun s => of' R M ↑s) a =
      (MvPolynomial.aeval fun s => of' R M ↑s) P + (MvPolynomial.aeval fun s => of' R M ↑s) Q

Tactic:
exact ⟨P + Q, map_add _ _ _⟩

Result:
no goals

Proof state:
case hM
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)

Tactic:
refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this

Result:
case hM.refine_1
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m✝ : M
this : m✝ ∈ closure S
m : M
hm : m ∈ S
⊢ ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)

case hM.refine_2
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd 0)

case hM.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : R[M]
ihf : ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = f
ihg : ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = g
⊢ ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = f + g

Tactic:
rcases ihf with ⟨P, rfl⟩

Result:
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : R[M]
ihg : ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = g
P : MvPolynomial (↑S) R
⊢ ∃ a, (MvPolynomial.aeval fun s => of' R M ↑s) a = (MvPolynomial.aeval fun s => of' R M ↑s) P + g
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem tendsto_zero_of_tendsto_zero_mass {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    (mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)) : Tendsto μs F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))

Tactic:
convert tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f

Result:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0

Proof state:
case h.e'_5.h.e'_3
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0

Tactic:
rw [zero_testAgainstNN_apply]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))

Tactic:
intro f

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
⊢ Tendsto μs F (𝓝 0)

Tactic:
rw [tendsto_iff_forall_testAgainstNN_tendsto]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))