harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem constantCoeff_wittNSMul (m : ℕ) (n : ℕ) : constantCoeff (wittNSMul p m n) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ constantCoeff (m • X 0) = 0

Tactic:
simp only [smul_zero, map_nsmul, constantCoeff_X]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ constantCoeff (wittNSMul p m n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
⊢ constantCoeff (m • X 0) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_congr [LawfulBEq α] (h : m.1.WF) {a b : α} (hab : a == b) {h'} :
    get m a h' = get m b ((contains_congr _ h hab).symm.trans h')

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝ : LawfulBEq α
h : m.val.WF
a b : α
hab : (a == b) = true
h' : m.contains a = true
⊢ get m a h' = get m b ⋯

Tactic:
simp_to_model using List.getValue_congr

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.param_pow_mul (hf : SuperpolynomialDecay l k f) (n : ℕ) :
    SuperpolynomialDecay l k (k ^ n * f)

Proof state:
case zero
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ 0 * f)

Tactic:
simpa only [one_mul, pow_zero] using hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f)

Tactic:
induction n with
| zero => simpa only [one_mul, pow_zero] using hf
| succ n hn => simpa only [pow_succ', mul_assoc] using hn.param_mul

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f)
⊢ SuperpolynomialDecay l k (k ^ (n + 1) * f)

Tactic:
simpa only [pow_succ', mul_assoc] using hn.param_mul

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_extract {as : Array α} {start stop : Nat} :
    (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none

Proof state:
case isTrue.isFalse
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝¹ : i < min stop as.size - start
h✝ : ¬start + i < as.size
⊢ some as[start + i] = none

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝ : ¬i < min stop as.size - start
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝ : i < min stop as.size - start
⊢ some as[start + i] = if h : start + i < as.size then some as[start + i] else none

Tactic:
split

Result:
case isTrue.isTrue
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝¹ : i < min stop as.size - start
h✝ : start + i < as.size
⊢ some as[start + i] = some as[start + i]

case isTrue.isFalse
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝¹ : i < min stop as.size - start
h✝ : ¬start + i < as.size
⊢ some as[start + i] = none

Proof state:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
⊢ (if h : i < min stop as.size - start then some as[start + i] else none) =
    if i < min stop as.size - start then if h : start + i < as.size then some as[start + i] else none else none

Tactic:
split

Result:
case isTrue
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝ : i < min stop as.size - start
⊢ some as[start + i] = if h : start + i < as.size then some as[start + i] else none

case isFalse
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝ : ¬i < min stop as.size - start
⊢ none = none

Proof state:
case isTrue.isTrue
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h✝¹ : i < min stop as.size - start
h✝ : start + i < as.size
⊢ some as[start + i] = some as[start + i]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
⊢ (as.extract start stop)[i]? = if i < min stop as.size - start then as[start + i]? else none

Tactic:
simp only [getElem?_def, size_extract, getElem_extract]

Result:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
⊢ (if h : i < min stop as.size - start then some as[start + i] else none) =
    if i < min stop as.size - start then if h : start + i < as.size then some as[start + i] else none else none
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem MvPolynomial.algebraicIndependent_X (σ R : Type*) [CommRing R] :
    AlgebraicIndependent R (X (R := R) (σ := σ))

Proof state:
σ : Type u_7
R : Type u_8
inst✝ : CommRing R
⊢ Injective ⇑(AlgHom.id R (MvPolynomial σ R))

Tactic:
exact injective_id

Result:
no goals

Proof state:
σ : Type u_7
R : Type u_8
inst✝ : CommRing R
⊢ AlgebraicIndependent R X

Tactic:
rw [AlgebraicIndependent, aeval_X_left]

Result:
σ : Type u_7
R : Type u_8
inst✝ : CommRing R
⊢ Injective ⇑(AlgHom.id R (MvPolynomial σ R))
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_add : (p + q).smeval x = p.smeval x + q.smeval x

Proof state:
case refine_1
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝ : ℕ
⊢ smul_pow x x✝ 0 = 0

Tactic:
rw [smul_pow, zero_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
⊢ (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)

Tactic:
refine sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)

Result:
case refine_1
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝ : ℕ
⊢ smul_pow x x✝ 0 = 0

case refine_2
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝² : ℕ
x✝¹ x✝ : R
⊢ smul_pow x x✝² (x✝¹ + x✝) = smul_pow x x✝² x✝¹ + smul_pow x x✝² x✝

Proof state:
case refine_2
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝² : ℕ
x✝¹ x✝ : R
⊢ smul_pow x x✝² (x✝¹ + x✝) = smul_pow x x✝² x✝¹ + smul_pow x x✝² x✝

Tactic:
rw [smul_pow, smul_pow, smul_pow, add_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
⊢ (p + q).smeval x = p.smeval x + q.smeval x

Tactic:
simp only [smeval_eq_sum, smul_pow]

Result:
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
⊢ (p + q).sum (smul_pow x) = p.sum (smul_pow x) + q.sum (smul_pow x)
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_degree_three_le {n : ℕ} {v : Fin (n + 3)} :
    (cycleGraph (n + 3)).degree v = 2

Proof state:
n : ℕ
v : Fin (n + 3)
⊢ v - 1 ≠ v + 1

Tactic:
simp only [ne_eq, sub_eq_iff_eq_add, add_assoc v, self_eq_add_right]

Result:
n : ℕ
v : Fin (n + 3)
⊢ ¬1 + 1 = 0

Proof state:
n : ℕ
v : Fin (n + 3)
⊢ ¬1 + 1 = 0

Tactic:
exact ne_of_beq_false rfl

Result:
no goals

Proof state:
n : ℕ
v : Fin (n + 3)
⊢ (cycleGraph (n + 3)).degree v = 2

Tactic:
rw [cycleGraph_degree_two_le, Finset.card_pair]

Result:
n : ℕ
v : Fin (n + 3)
⊢ v - 1 ≠ v + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_last (x : BitVec w) :
    x.getLsbD (w-1) = decide (2 ^ (w-1) ≤ x.toNat)

Proof state:
case zero
x : BitVec 0
⊢ x.getLsbD (0 - 1) = decide (2 ^ (0 - 1) ≤ x.toNat)

Tactic:
simp [toNat_of_zero_length]

Result:
no goals

Proof state:
case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ x.toNat - 2 ^ w < 2 ^ w

Tactic:
omega

Result:
no goals

Proof state:
case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide True

Tactic:
rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]

Result:
case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ decide ((0 + 1) % 2 = 1) = decide True

case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ x.toNat - 2 ^ w < 2 ^ w

Proof state:
case succ
w : Nat
x : BitVec (w + 1)
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide (2 ^ w ≤ x.toNat)

Tactic:
rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h

Result:
case succ.inl
w : Nat
x : BitVec (w + 1)
h : x.toNat < 2 ^ w
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide (2 ^ w ≤ x.toNat)

case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide (2 ^ w ≤ x.toNat)

Proof state:
case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide (2 ^ w ≤ x.toNat)

Tactic:
simp only [h]

Result:
case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide True

Proof state:
case succ.inr
w : Nat
x : BitVec (w + 1)
h : x.toNat ≥ 2 ^ w
⊢ decide ((0 + 1) % 2 = 1) = decide True

Tactic:
simp

Result:
no goals

Proof state:
case succ.inl
w : Nat
x : BitVec (w + 1)
h : x.toNat < 2 ^ w
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide (2 ^ w ≤ x.toNat)

Tactic:
simp [Nat.div_eq_of_lt h, h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.getLsbD (w - 1) = decide (2 ^ (w - 1) ≤ x.toNat)

Tactic:
rcases w with rfl | w

Result:
case zero
x : BitVec 0
⊢ x.getLsbD (0 - 1) = decide (2 ^ (0 - 1) ≤ x.toNat)

case succ
w : Nat
x : BitVec (w + 1)
⊢ x.getLsbD (w + 1 - 1) = decide (2 ^ (w + 1 - 1) ≤ x.toNat)

Proof state:
case succ
w : Nat
x : BitVec (w + 1)
⊢ x.getLsbD (w + 1 - 1) = decide (2 ^ (w + 1 - 1) ≤ x.toNat)

Tactic:
simp only [getLsbD, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]

Result:
case succ
w : Nat
x : BitVec (w + 1)
⊢ decide (x.toNat / 2 ^ w % 2 = 1) = decide (2 ^ w ≤ x.toNat)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Gcd.lean
theorem gcd_dvd_right {a b : Int} : (gcd a b : Int) ∣ b

Proof state:
a b : Int
this : a.natAbs.gcd b.natAbs ∣ b.natAbs
⊢ ↑(a.gcd b) ∣ b

Tactic:
rw [← Int.ofNat_dvd] at this

Result:
a b : Int
this : ↑(a.natAbs.gcd b.natAbs) ∣ ↑b.natAbs
⊢ ↑(a.gcd b) ∣ b

Proof state:
a b : Int
⊢ ↑(a.gcd b) ∣ b

Tactic:
have := Nat.gcd_dvd_right a.natAbs b.natAbs

Result:
a b : Int
this : a.natAbs.gcd b.natAbs ∣ b.natAbs
⊢ ↑(a.gcd b) ∣ b

Proof state:
a b : Int
this : ↑(a.natAbs.gcd b.natAbs) ∣ ↑b.natAbs
⊢ ↑(a.gcd b) ∣ b

Tactic:
exact Int.dvd_trans this natAbs_dvd_self

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma c_relation : 1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 1728 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆)) =
    ((W.a₁ ^ 2 + 4 * W.a₂) ^ 2 - 24 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 3 -
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 3 + 36 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) -
          216 * (W.a₃ ^ 2 + 4 * W.a₆)) ^
        2

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 1728 * W.Δ = W.c₄ ^ 3 - W.c₆ ^ 2

Tactic:
simp only [b₂, b₄, b₆, b₈, c₄, c₆, Δ]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 1728 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆)) =
    ((W.a₁ ^ 2 + 4 * W.a₂) ^ 2 - 24 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 3 -
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 3 + 36 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) -
          216 * (W.a₃ ^ 2 + 4 * W.a₆)) ^
        2
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem leadingCoeff_one [MulZeroOneClass R] : (1 : HahnSeries Γ R).leadingCoeff = 1

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
⊢ leadingCoeff 1 = 1

Tactic:
simp [leadingCoeff_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem Splits.dvd_of_roots_le_roots {p q : K[X]} (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0)
    (hq : p.roots ≤ q.roots) : p ∣ q

Proof state:
K : Type v
inst✝ : Field K
p q : K[X]
hp : Splits (RingHom.id K) p
hp0 : p ≠ 0
hq : p.roots ≤ q.roots
⊢ p ∣ q

Tactic:
rw [eq_prod_roots_of_splits_id hp, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]

Result:
K : Type v
inst✝ : Field K
p q : K[X]
hp : Splits (RingHom.id K) p
hp0 : p ≠ 0
hq : p.roots ≤ q.roots
⊢ (Multiset.map (fun a => X - C a) p.roots).prod ∣ q

Proof state:
K : Type v
inst✝ : Field K
p q : K[X]
hp : Splits (RingHom.id K) p
hp0 : p ≠ 0
hq : p.roots ≤ q.roots
⊢ (Multiset.map (fun a => X - C a) p.roots).prod ∣ q

Tactic:
exact dvd_trans
  (Multiset.prod_dvd_prod_of_le (Multiset.map_le_map hq))
  (prod_multiset_X_sub_C_dvd _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.of_isNonZero (ctx : Context) {p : Poly} (h : isNonZero p = true) : p.denote ctx > 0

Proof state:
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
h : isNonZero ((k, v) :: p) = true
⊢ denote ctx ((k, v) :: p) > 0

Tactic:
by_cases he : v == fixedVar <;> simp [he, isNonZero] at h ⊢

Result:
case pos
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : 0 < k
⊢ 0 < denote ctx p + k * Var.denote ctx v

case neg
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
⊢ 0 < denote ctx p + k * Var.denote ctx v

Proof state:
case pos.h
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : 0 < k
⊢ succ 0 ≤ k + denote ctx p

Tactic:
exact Nat.le_trans h (Nat.le_add_right ..)

Result:
no goals

Proof state:
ctx : Context
p : Poly
h : isNonZero [] = true
⊢ denote ctx [] > 0

Tactic:
contradiction

Result:
no goals

Proof state:
case neg
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
⊢ 0 < denote ctx p + k * Var.denote ctx v

Tactic:
have ih := of_isNonZero ctx h

Result:
case neg
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
ih : denote ctx p > 0
⊢ 0 < denote ctx p + k * Var.denote ctx v

Proof state:
case neg
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
ih : denote ctx p > 0
⊢ 0 < denote ctx p + k * Var.denote ctx v

Tactic:
exact Nat.le_trans ih (Nat.le_add_right ..)

Result:
no goals

Proof state:
case pos
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : 0 < k
⊢ 0 < denote ctx p + k * Var.denote ctx v

Tactic:
simp [eq_of_beq he, Var.denote]

Result:
case pos
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : 0 < k
⊢ 0 < k + denote ctx p

Proof state:
case pos
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : 0 < k
⊢ 0 < k + denote ctx p

Tactic:
apply Nat.lt_of_succ_le

Result:
case pos.h
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : 0 < k
⊢ succ 0 ≤ k + denote ctx p
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_Ioi_mul_deriv_eq_deriv_mul
    (hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x) (hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x)
    (huv' : IntegrableOn (u * v') (Ioi a)) (hu'v : IntegrableOn (u' * v) (Ioi a))
    (h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')) (h_infty : Tendsto (u * v) atTop (𝓝 b')) :
    ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x

Proof state:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x

Tactic:
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]

Result:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (a : ℝ) in Ioi a, u a * v' a + u' a * v a ∂volume = b' - a'

Proof state:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (u * v') (Ioi a) volume
hu'v : IntegrableOn (u' * v) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x

Tactic:
rw [Pi.mul_def] at huv' hu'v

Result:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (x : ℝ) in Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Ioi a, u' x * v x

Proof state:
A : Type u_1
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst✝ : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (fun i => u i * v' i) (Ioi a) volume
hu'v : IntegrableOn (fun i => u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ ∫ (a : ℝ) in Ioi a, u a * v' a + u' a * v a ∂volume = b' - a'

Tactic:
simpa only [add_comm] using integral_Ioi_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
    coeff (p * Polynomial.X ^ n) (d + n) = coeff p d

Proof state:
case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0

Tactic:
exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (p * X ^ n).coeff (d + n) = p.coeff d

Tactic:
rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]

Result:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

case h₁
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (d, n) ∉ antidiagonal (d + n) → p.coeff (d, n).1 * (X ^ n).coeff (d, n).2 = 0

Proof state:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Tactic:
rw [mem_antidiagonal, add_right_cancel_iff] at h1

Result:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
d i j : ℕ
h1 : (i, j).1 = d
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Proof state:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
i j : ℕ
h2 : (i, j) ≠ ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, (i, j).2)

Tactic:
rfl

Result:
no goals

Proof state:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
d i j : ℕ
h1 : (i, j).1 = d
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Tactic:
subst h1

Result:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
i j : ℕ
h2 : (i, j) ≠ ((i, j).1, (i, j).2)
⊢ (i, j) = ((i, j).1, (i, j).2)

Proof state:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ False

Tactic:
apply h2

Result:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ (i, j) = (d, (i, j).2)

Proof state:
case h₀.mk
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ p.coeff (i, j).1 * (X ^ n).coeff (i, j).2 = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Result:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n

Proof state:
case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

Tactic:
rintro ⟨i, j⟩ h1 h2

Result:
case h₀.mk
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ p.coeff (i, j).1 * (X ^ n).coeff (i, j).2 = 0

Proof state:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).2 = n

Tactic:
rintro rfl

Result:
case h₀.mk.hnc
R : Type u
inst✝ : Semiring R
p : R[X]
d i j : ℕ
h1 : (i, j) ∈ antidiagonal (d + (i, j).2)
h2 : (i, j) ≠ (d, (i, j).2)
⊢ False
-- Mathlib/Data/List/OfFn.lean
theorem map_ofFn {β : Type*} {n : ℕ} (f : Fin n → α) (g : α → β) :
    map g (ofFn f) = ofFn (g ∘ f) :=
  ext_get (by simp) fun i h h' => by simp

Proof state:
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
i : ℕ
h : i < (map g (ofFn f)).length
h' : i < (ofFn (g ∘ f)).length
⊢ (map g (ofFn f)).get ⟨i, h⟩ = (ofFn (g ∘ f)).get ⟨i, h'⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
⊢ (map g (ofFn f)).length = (ofFn (g ∘ f)).length

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem induction_on {motive : M ⊗[R] N → Prop} (z : M ⊗[R] N)
    (zero : motive 0)
    (tmul : ∀ x y, motive <| x ⊗ₜ[R] y)
    (add : ∀ x y, motive x → motive y → motive (x + y)) : motive z :=
  AddCon.induction_on z fun x =>
    FreeAddMonoid.recOn x zero fun ⟨m, n⟩ y ih => by
      rw [AddCon.coe_add]
      exact add _ _ (tmul ..) ih

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : motive ↑y
m : M
n : N
⊢ motive (↑(FreeAddMonoid.of (m, n)) + ↑y)

Tactic:
exact add _ _ (tmul ..) ih

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : motive ↑y
m : M
n : N
⊢ motive ↑(FreeAddMonoid.of (m, n) + y)

Tactic:
rw [AddCon.coe_add]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
motive : M ⊗[R] N → Prop
z : M ⊗[R] N
zero : motive 0
tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)
add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)
x : FreeAddMonoid (M × N)
x✝ : M × N
y : FreeAddMonoid (M × N)
ih : motive ↑y
m : M
n : N
⊢ motive (↑(FreeAddMonoid.of (m, n)) + ↑y)