-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum₂_mul_of_le [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α] [AddLeftMono α]
    [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x y : α} (hxy : x ≤ y) (n : ℕ) :
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

Proof state:
case h.e'_2.h.e'_5.a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ x ^ (n - 1 - x✝) * y ^ (n - 1 - (n - 1 - x✝)) = y ^ x✝ * x ^ (n - 1 - x✝)

Tactic:
rw [mul_comm]

Result:
case h.e'_2.h.e'_5.a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ y ^ (n - 1 - (n - 1 - x✝)) * x ^ (n - 1 - x✝) = y ^ x✝ * x ^ (n - 1 - x✝)

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n

Tactic:
rw [← Finset.sum_range_reflect]

Result:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n : ℕ
⊢ (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n

Proof state:
case h.e'_2.h.e'_5.a.e_a.e_a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ n - 1 - (n - 1 - x✝) = x✝

Tactic:
omega

Result:
no goals

Proof state:
case h.e'_2.h.e'_5.a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ x ^ (n - 1 - x✝) * y ^ (n - 1 - (n - 1 - x✝)) = y ^ x✝ * x ^ (n - 1 - x✝)

Tactic:
simp_all only [Finset.mem_range]

Result:
case h.e'_2.h.e'_5.a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ x ^ (n - 1 - x✝) * y ^ (n - 1 - (n - 1 - x✝)) = y ^ x✝ * x ^ (n - 1 - x✝)

Proof state:
case h.e'_2.h.e'_5.a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ y ^ (n - 1 - (n - 1 - x✝)) * x ^ (n - 1 - x✝) = y ^ x✝ * x ^ (n - 1 - x✝)

Tactic:
congr

Result:
case h.e'_2.h.e'_5.a.e_a.e_a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ n - 1 - (n - 1 - x✝) = x✝

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n : ℕ
⊢ (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n

Tactic:
convert geom_sum₂_mul_of_ge hxy n using 3

Result:
case h.e'_2.h.e'_5.a
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x y : α
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ x ^ (n - 1 - x✝) * y ^ (n - 1 - (n - 1 - x✝)) = y ^ x✝ * x ^ (n - 1 - x✝)