harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionOf_eq_bot_iff_of_noZeroSMulDivisors [Nontrivial R] [NoZeroSMulDivisors R M] (m : M) :
    torsionOf R M m = ⊥ ↔ m ≠ 0

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : torsionOf R M m = ⊥
contra : m = 0
⊢ False

Tactic:
rw [contra, torsionOf_zero] at h

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : ⊤ = ⊥
contra : m = 0
⊢ False

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0

Tactic:
rw [mem_torsionOf_iff, smul_eq_zero] at hr

Result:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : ⊤ = ⊥
contra : m = 0
⊢ False

Tactic:
exact bot_ne_top.symm h

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0

Tactic:
tauto

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
⊢ torsionOf R M m = ⊥ ↔ m ≠ 0

Tactic:
refine ⟨fun h contra => ?_, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => ?_⟩

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : torsionOf R M m = ⊥
contra : m = 0
⊢ False

case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0
-- Mathlib/Topology/Metrizable/Basic.lean
theorem IsSeparable.secondCountableTopology [PseudoMetrizableSpace X] {s : Set X}
    (hs : IsSeparable s) : SecondCountableTopology s

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
⊢ SecondCountableTopology ↑s

Tactic:
letI := pseudoMetrizableSpacePseudoMetric X

Result:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ SecondCountableTopology ↑s

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this✝ : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
this : SeparableSpace ↑s
⊢ SecondCountableTopology ↑s

Tactic:
exact UniformSpace.secondCountable_of_separable s

Result:
no goals

Proof state:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
⊢ SecondCountableTopology ↑s

Tactic:
have := hs.separableSpace

Result:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this✝ : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
this : SeparableSpace ↑s
⊢ SecondCountableTopology ↑s
-- Mathlib/Data/Fin/Basic.lean
theorem succ_castPred_eq_add_one {a : Fin (n + 1)} (ha : a ≠ last n) :
    (a.castPred ha).succ = a + 1

Proof state:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ = a + 1

Tactic:
cases a using lastCases

Result:
case last
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1

case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1

Proof state:
case last
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1

Tactic:
exact (ha rfl).elim

Result:
no goals

Proof state:
case cast
n : ℕ
i✝ : Fin n
ha : i✝.castSucc ≠ last n
⊢ (i✝.castSucc.castPred ha).succ = i✝.castSucc + 1

Tactic:
rw [castPred_castSucc, coeSucc_eq_succ]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem norm_le_dual_bound (x : E) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ f : Dual 𝕜 E, ‖f x‖ ≤ M * ‖f‖) :
    ‖x‖ ≤ M

Proof state:
case neg
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : ¬x = 0
⊢ ‖x‖ ≤ M

Tactic:
obtain ⟨f, hf₁, hfx⟩ : ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ := exists_dual_vector 𝕜 x h

Result:
case neg.intro.intro
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : f x = ↑‖x‖
⊢ ‖x‖ ≤ M

Proof state:
case neg.intro.intro
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : f x = ↑‖x‖
⊢ ‖x‖ ≤ M

Tactic:
calc
  ‖x‖ = ‖(‖x‖ : 𝕜)‖ := RCLike.norm_coe_norm.symm
  _ = ‖f x‖ := by rw [hfx]
  _ ≤ M * ‖f‖ := hM f
  _ = M := by rw [hf₁, mul_one]

Result:
no goals

Proof state:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : x = 0
⊢ ‖x‖ ≤ M

Tactic:
simp only [h, hMp, norm_zero]

Result:
no goals

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M

Tactic:
by_cases h : x = 0

Result:
case pos
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : x = 0
⊢ ‖x‖ ≤ M

case neg
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : ¬x = 0
⊢ ‖x‖ ≤ M

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : f x = ↑‖x‖
⊢ M * ‖f‖ = M

Tactic:
rw [hf₁, mul_one]

Result:
no goals

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : f x = ↑‖x‖
⊢ ‖↑‖x‖‖ = ‖f x‖

Tactic:
rw [hfx]

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_assoc (a b c : Nimber) : a + b + c = a + (b + c)

Proof state:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ a + y + c ≠ a + (b + c)

case a.h₂
a b c x : Nimber
hx : x < c
⊢ a + b + x ≠ a + (b + c)

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Tactic:
on_goal 2 => rw [Nimber.add_assoc _ y, add_ne_add_right, add_ne_add_left]

Result:
case a.h₁.inl.intro.intro
a b c y : Nimber
hy : y < a
hx : y + b < a + b
⊢ y ≠ a

case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

case a.h₂
a b c x : Nimber
hx : x < c
⊢ a + b + x ≠ a + (b + c)

case a.h₁
a b c x : Nimber
hx : x < a
⊢ x + (b + c) ≠ a + b + c

case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ a + (b + y) ≠ a + b + c

Proof state:
case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ a + y + c ≠ a + (b + c)

Tactic:
rw [Nimber.add_assoc _ y, add_ne_add_right, add_ne_add_left]

Result:
case a.h₁.inr.intro.intro
a b c y : Nimber
hy : y < b
hx : a + y < a + b
⊢ y ≠ b

Proof state:
case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ a + (y + c) ≠ a + b + c

Tactic:
rw [← Nimber.add_assoc _ y, add_ne_add_left, add_ne_add_right]

Result:
case a.h₂.inl.intro.intro
a b c y : Nimber
hy : y < b
hx : y + c < b + c
⊢ y ≠ b

Proof state:
case a.h₂.inr.intro.intro
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ y ≠ c

Tactic:
apply ne_of_lt

Result:
case a.h₂.inr.intro.intro.h
a b c y : Nimber
hy : y < c
hx : b + y < b + c
⊢ y < c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_flatten (xs : Vector (Vector α m) n) (p : α → Bool) :
    xs.flatten.find? p = xs.findSome? (·.find? p)

Proof state:
α : Type
m n : Nat
xs : Vector (Vector α m) n
p : α → Bool
⊢ find? p xs.flatten = findSome? (fun x => find? p x) xs

Tactic:
cases xs using vector₂_induction

Result:
case of
α : Type
m n : Nat
p : α → Bool
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ find? p
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    findSome? (fun x => find? p x)
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }

Proof state:
case of
α : Type
m n : Nat
p : α → Bool
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ find? p
      {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten =
    findSome? (fun x => find? p x)
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
            xss✝.attach,
        size_toArray := ⋯ }

Tactic:
simp [Array.findSome?_map, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem vector₂_induction (P : Vector (Vector α n) m → Prop)
    (of : ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ xs ∈ xss, xs.size = n),
      P (mk (xss.attach.map (fun ⟨xs, m⟩ => mk xs (h₂ xs m))) (by simpa using h₁)))
    (ass : Vector (Vector α n) m) : P ass

Proof state:
α : Type u_1
n m : Nat
P : Vector (Vector α n) m → Prop
ass : Vector (Vector α n) m
of :
  P
    {
      toArray :=
        Array.map
          (fun x =>
            match x with
            | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
          (map toArray ass).attach,
      size_toArray := ⋯ }
⊢ P ass

Tactic:
simpa [Array.map_attach, Array.pmap_map] using of

Result:
no goals

Proof state:
α : Type ?u.193782
n m : Nat
P : Vector (Vector α n) m → Prop
xss : Array (Array α)
h₁ : xss.size = m
h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = n
⊢ (Array.map
        (fun x =>
          match x with
          | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
        xss.attach).size =
    m

Tactic:
simpa using h₁

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
P : Vector (Vector α n) m → Prop
of :
  ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = n),
    P
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
            xss.attach,
        size_toArray := ⋯ }
ass : Vector (Vector α n) m
⊢ P ass

Tactic:
specialize of (ass.map toArray).toArray (by simp) (by simp)

Result:
α : Type u_1
n m : Nat
P : Vector (Vector α n) m → Prop
ass : Vector (Vector α n) m
of :
  P
    {
      toArray :=
        Array.map
          (fun x =>
            match x with
            | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
          (map toArray ass).attach,
      size_toArray := ⋯ }
⊢ P ass

Proof state:
α : Type u_1
n m : Nat
P : Vector (Vector α n) m → Prop
of :
  ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = n),
    P
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
            xss.attach,
        size_toArray := ⋯ }
ass : Vector (Vector α n) m
⊢ (map toArray ass).size = m

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
P : Vector (Vector α n) m → Prop
of :
  ∀ (xss : Array (Array α)) (h₁ : xss.size = m) (h₂ : ∀ (xs : Array α), xs ∈ xss → xs.size = n),
    P
      {
        toArray :=
          Array.map
            (fun x =>
              match x with
              | ⟨xs, m⟩ => { toArray := xs, size_toArray := ⋯ })
            xss.attach,
        size_toArray := ⋯ }
ass : Vector (Vector α n) m
⊢ ∀ (xs : Array α), xs ∈ (map toArray ass).toArray → xs.size = n

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem IsPGroup.isNilpotent [Finite G] {p : ℕ} [hp : Fact (Nat.Prime p)] (h : IsPGroup p G) :
    IsNilpotent G

Proof state:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card (G ⧸ center G) * card ↥(center G)

Tactic:
apply lt_mul_of_one_lt_right

Result:
case ha
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 0 < card (G ⧸ center G)

case h
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card ↥(center G)

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
⊢ IsNilpotent G

Tactic:
cases nonempty_fintype G

Result:
case intro
G : Type u_1
hG : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val✝ : Fintype G
⊢ IsNilpotent G
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_subset_iff_left : image₂ f s t ⊆ u ↔ ∀ a ∈ s, (t.image fun b => f a b) ⊆ u

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ a ∈ s, image (fun b => f a b) t ⊆ u

Tactic:
simp_rw [image₂_subset_iff, image_subset_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem variance {n : ℕ} (h : 0 < (n : ℝ)) (x : I) :
    (∑ k : Fin (n + 1), (x - k/ₙ : ℝ) ^ 2 * bernstein n k x) = (x : ℝ) * (1 - x) / n

Proof state:
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
this :
  (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) =
    (Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X))
⊢ ∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n

Tactic:
simp only [nsmul_eq_mul, Finset.sum_range, map_sum, Polynomial.coe_aeval_eq_eval,
  Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_sub, Polynomial.eval_natCast,
  Polynomial.eval_X, Polynomial.eval_one] at this

Result:
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n

Proof state:
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ (↑x - ↑↑k / ↑n) ^ 2 * (bernstein n ↑k) x * ↑n * ↑n =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)

Tactic:
rw [mul_comm _ (n : ℝ), mul_comm _ (n : ℝ), ← mul_assoc, ← mul_assoc]

Result:
case h.e'_2.e_f.h
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
k : Fin (n + 1)
⊢ ↑n * ↑n * (↑x - ↑↑k / ↑n) ^ 2 * (bernstein n ↑k) x =
    (↑n * ↑x - ↑↑k) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑k)

Proof state:
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
this :
  ∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν =
    n • Polynomial.X * (1 - Polynomial.X)
⊢ ∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n

Tactic:
apply_fun fun p => Polynomial.aeval (x : ℝ) p at this

Result:
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
this :
  (Polynomial.aeval ↑x) (∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial ℝ n ν) =
    (Polynomial.aeval ↑x) (n • Polynomial.X * (1 - Polynomial.X))
⊢ ∑ i : Fin (n + 1), (↑x - ↑↑i / ↑n) ^ 2 * (bernstein n ↑i) x * ↑n * ↑n = ↑x * (1 - ↑x) * ↑n

Proof state:
case h.e'_3
n : ℕ
h : 0 < ↑n
x : ↑I
h' : ↑n ≠ 0
this :
  ∑ x_1 : Fin (n + 1), (↑n * ↑x - ↑↑x_1) ^ 2 * Polynomial.eval (↑x) (bernsteinPolynomial ℝ n ↑x_1) = ↑n * ↑x * (1 - ↑x)
⊢ ↑x * (1 - ↑x) * ↑n = ↑n * ↑x * (1 - ↑x)

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Group/Ext.lean
@[to_additive]
lemma Group.toDivInvMonoid_injective {G : Type*} : Injective (@Group.toDivInvMonoid G)

Proof state:
G : Type u_1
⊢ Injective (@toDivInvMonoid G)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩

Result:
case mk.mk.refl
G : Type u_1
toDivInvMonoid✝ : DivInvMonoid G
inv_mul_cancel✝¹ inv_mul_cancel✝ : ∀ (a : G), a⁻¹ * a = 1
⊢ mk inv_mul_cancel✝¹ = mk inv_mul_cancel✝

Proof state:
case mk.mk.refl
G : Type u_1
toDivInvMonoid✝ : DivInvMonoid G
inv_mul_cancel✝¹ inv_mul_cancel✝ : ∀ (a : G), a⁻¹ * a = 1
⊢ mk inv_mul_cancel✝¹ = mk inv_mul_cancel✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem leadingCoeff_eraseLead_eq_nextCoeff (h : f.nextCoeff ≠ 0) :
    f.eraseLead.leadingCoeff = f.nextCoeff

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.leadingCoeff = f.nextCoeff

Tactic:
rw [leadingCoeff, nextCoeff, natDegree_eraseLead h, if_neg,
  eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne]

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < f.natDegree

R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ 0 < 1

case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Tactic:
all_goals positivity

Result:
no goals

Proof state:
case hnc
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ ¬f.natDegree = 0

Tactic:
positivity

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.leadingCoeff = f.nextCoeff

Tactic:
have := natDegree_pos_of_nextCoeff_ne_zero h

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.leadingCoeff = f.nextCoeff
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem rename_isHomogeneous_iff {f : σ → τ} (hf : f.Injective) :
    (rename f φ).IsHomogeneous n ↔ φ.IsHomogeneous n

Proof state:
case h.e'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) (mapDomain f d) = (weight 1) d

Tactic:
simp only [weight_apply, Pi.one_apply, smul_eq_mul, mul_one]

Result:
case h.e'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ((mapDomain f d).sum fun i c => c) = d.sum fun i c => c

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ coeff (mapDomain f d) ((rename f) φ) ≠ 0

Tactic:
rwa [coeff_rename_mapDomain f hf]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d = n

Tactic:
convert ← @h (d.mapDomain f) _

Result:
case h.e'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) (mapDomain f d) = (weight 1) d

σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ coeff (mapDomain f d) ((rename f) φ) ≠ 0

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
⊢ ((rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n

Tactic:
refine ⟨fun h d hd ↦ ?_, rename_isHomogeneous⟩

Result:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d = n

Proof state:
case h.e'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ((mapDomain f d).sum fun i c => c) = d.sum fun i c => c

Tactic:
exact Finsupp.sum_mapDomain_index_inj (h := fun _ ↦ id) hf

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem inverse_zero : inverse (0 : M₀) = 0

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
⊢ inverse 0 = 0

Tactic:
nontriviality

Result:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a✝ : Nontrivial M₀
⊢ inverse 0 = 0

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a✝ : Nontrivial M₀
⊢ inverse 0 = 0

Tactic:
exact inverse_non_unit _ not_isUnit_zero

Result:
no goals