harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma coeff_minpolyDiv (i) : coeff (minpolyDiv R x) i =
    algebraMap R S (coeff (minpoly R x) (i + 1)) + coeff (minpolyDiv R x) (i + 1) * x

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
⊢ (minpolyDiv R x).coeff i = (minpolyDiv R x * (X - C x)).coeff (i + 1) + (minpolyDiv R x).coeff (i + 1) * x

Tactic:
simp [mul_sub]

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
⊢ (minpolyDiv R x).coeff i = (algebraMap R S) ((minpoly R x).coeff (i + 1)) + (minpolyDiv R x).coeff (i + 1) * x

Tactic:
rw [← coeff_map, ← minpolyDiv_spec R x]

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
⊢ (minpolyDiv R x).coeff i = (minpolyDiv R x * (X - C x)).coeff (i + 1) + (minpolyDiv R x).coeff (i + 1) * x
-- Mathlib/Data/Sym/Sym2.lean
theorem other_invol' [DecidableEq α] {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Mem.other' ha ∈ z) :
    Mem.other' hb = a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb = a

Tactic:
induction z

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
ha : a ∈ s(x✝, y✝)
hb : Mem.other' ha ∈ s(x✝, y✝)
⊢ Mem.other' hb = a

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a x✝ y✝ : α
ha : a ∈ s(x✝, y✝)
hb : Mem.other' ha ∈ s(x✝, y✝)
⊢ Mem.other' hb = a

Tactic:
aesop (rule_sets := [Sym2]) (add norm unfold [Sym2.rec, Quot.rec])

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma card_le_card_of_injOn (f : α → β) (hf : ∀ a ∈ s, f a ∈ t) (f_inj : (s : Set α).InjOn f) :
    #s ≤ #t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : Set.InjOn f ↑s
⊢ #s ≤ #t

Tactic:
calc
  #s = #(s.image f) := (card_image_of_injOn f_inj).symm
  _  ≤ #t           := card_le_card <| image_subset_iff.2 hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : Set.InjOn f ↑s
⊢ #s ≤ #t

Tactic:
classical
calc
  #s = #(s.image f) := (card_image_of_injOn f_inj).symm
  _  ≤ #t           := card_le_card <| image_subset_iff.2 hf

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem basicOpen_fromSpec_app :
    (Spec Γ(X, U)).basicOpen (hU.fromSpec.app U f) = PrimeSpectrum.basicOpen f

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ (Spec Γ(X, U)).basicOpen ((ConcreteCategory.hom (Scheme.Hom.app hU.fromSpec U)) f) = PrimeSpectrum.basicOpen f

Tactic:
rw [← hU.fromSpec_preimage_basicOpen, Scheme.preimage_basicOpen]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_neg_id (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommRing R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalRing R
inst✝⁷ : ContinuousStar R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : autoParam (p a) _auto✝
⊢ cfcₙ (fun x => -x) a = -a

Tactic:
rw [cfcₙ_neg .., cfcₙ_id' R a]

Result:
no goals
-- Mathlib/Algebra/Group/PNatPowAssoc.lean
theorem ppow_mul_assoc (k m n : ℕ+) (x : M) :
    (x ^ k * x ^ m) * x ^ n = x ^ k * (x ^ m * x ^ n)

Proof state:
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
k m n : ℕ+
x : M
⊢ x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)

Tactic:
simp only [← ppow_add, add_assoc]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem mem_sup_right {S T : Subsemigroup M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Proof state:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
have : T ≤ S ⊔ T := le_sup_right

Result:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Proof state:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T

Tactic:
tauto

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_smul_right (a : R) (x y : M) : polar Q x (a • y) = a • polar Q x y

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
a : R
x y : M
⊢ polar (⇑Q) x (a • y) = a • polar (⇑Q) x y

Tactic:
rw [polar_comm Q x, polar_comm Q x, polar_smul_left]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem multichoose_zero_right (n : ℕ) : multichoose n 0 = 1

Proof state:
n : ℕ
⊢ n.multichoose 0 = 1

Tactic:
cases n <;> simp [multichoose]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Basic.lean
theorem eq_zero_iff_dvd {R} [CommRing R] (x y : R) :
    Ideal.Quotient.mk (Ideal.span ({x} : Set R)) y = 0 ↔ x ∣ y

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ (mk (span {x})) y = 0 ↔ x ∣ y

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean
lemma factors_multiset_prod_of_irreducible {s : Multiset ℕ} (h : ∀ x : ℕ, x ∈ s → Irreducible x) :
    normalizedFactors s.prod = s

Proof state:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ 0 ∉ s

Tactic:
exact fun con ↦ not_irreducible_zero (h 0 con)

Result:
no goals

Proof state:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ s.prod ≠ 0

Tactic:
rw [Ne, Multiset.prod_eq_zero_iff]

Result:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ 0 ∉ s

Proof state:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ normalizedFactors s.prod = s

Tactic:
rw [← Multiset.rel_eq, ← associated_eq_eq]

Result:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ Multiset.Rel (fun x1 x2 => Associated x1 x2) (normalizedFactors s.prod) s

Proof state:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ Multiset.Rel (fun x1 x2 => Associated x1 x2) (normalizedFactors s.prod) s

Tactic:
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor h
  (prod_normalizedFactors _)

Result:
s : Multiset ℕ
h : ∀ x ∈ s, Irreducible x
⊢ s.prod ≠ 0
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma exactAt_iff :
    K.ExactAt i ↔ (K.sc i).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
⊢ K.ExactAt i ↔ (K.sc i).Exact

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_false_iff_forall_mem_keys [BEq α] [PartialEquivBEq α]
    {l : List ((a : α) × β a)} {a : α} :
    (containsKey a l) = false ↔ ∀ a' ∈ keys l, (a == a') = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = false ↔ ∀ (a' : α), a' ∈ keys l → (a == a') = false

Tactic:
simp only [Bool.eq_false_iff, ne_eq, containsKey_iff_exists, not_exists, not_and]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem isCompactlyGenerated_of_wellFoundedGT [h : WellFoundedGT α] :
    IsCompactlyGenerated α

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : WellFoundedGT α
⊢ IsCompactlyGenerated α

Tactic:
rw [wellFoundedGT_iff_isSupFiniteCompact, isSupFiniteCompact_iff_all_elements_compact] at h

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
⊢ IsCompactlyGenerated α

Tactic:
exact ⟨fun x => ⟨{x}, ⟨fun x _ => h x, sSup_singleton⟩⟩⟩

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem max_one_div_max_inv_one_eq_self (a : α) : max a 1 / max a⁻¹ 1 = a

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ (a ⊔ 1) / (a⁻¹ ⊔ 1) = a

Tactic:
rcases le_total a 1 with (h | h) <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.neg_add_eq_iff_eq_add (a b c : BitVec w) : ((~~~a + 1#w) + b == c) = (b == c + a)

Proof state:
w : Nat
a b c : BitVec w
⊢ (b + (~~~a + 1#w) == c) = (b == c + a)

Tactic:
exact BitVec.sub_eq_iff_eq_add _ _ _

Result:
no goals

Proof state:
w : Nat
a b c : BitVec w
⊢ (~~~a + 1#w + b == c) = (b == c + a)

Tactic:
rw [BitVec.add_comm]

Result:
w : Nat
a b c : BitVec w
⊢ (b + (~~~a + 1#w) == c) = (b == c + a)
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_succ_row_zero {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) :
    det A = ∑ j : Fin n.succ, (-1) ^ (j : ℕ) * A 0 j * det (A.submatrix Fin.succ j.succAbove)

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ)ᵀ.det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det

Tactic:
simp only [transpose_apply, transpose_submatrix, transpose_transpose]

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det

Tactic:
rw [← det_transpose]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ)ᵀ.det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ i : Fin n.succ, (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    ∑ j : Fin n.succ, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

Tactic:
refine Finset.sum_congr rfl fun i _ => ?_

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ A.det = ∑ j : Fin n.succ, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det

Tactic:
rw [← det_transpose A, det_succ_column_zero]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ i : Fin n.succ, (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    ∑ j : Fin n.succ, (-1) ^ ↑j * A 0 j * (A.submatrix Fin.succ j.succAbove).det
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem sub_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :
    (l₁ - l₂).eval v = l₁.eval v - l₂.eval v

Proof state:
l₁ l₂ : LinearCombo
v : Coeffs
⊢ (l₁ - l₂).eval v = l₁.eval v - l₂.eval v

Tactic:
simp [sub_eq_add_neg, Int.sub_eq_add_neg]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Period.lean
theorem period_bounded_of_exponent_pos (exp_pos : 0 < Monoid.exponent M) (m : M) :
    BddAbove (Set.range (fun a : α => period m a))

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ BddAbove (Set.range fun a => period m a)

Tactic:
use Monoid.exponent M

Result:
case h
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ Monoid.exponent M ∈ upperBounds (Set.range fun a => period m a)

Proof state:
case h
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
exp_pos : 0 < Monoid.exponent M
m : M
⊢ Monoid.exponent M ∈ upperBounds (Set.range fun a => period m a)

Tactic:
simpa [upperBounds] using period_le_exponent exp_pos _

Result:
no goals
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma mem_sup : x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊔ T ↔ x ∈ S ∨ x ∈ T

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany m l).getKeyD k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany m l).getKeyD k' fallback = k

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Algebra/Field/IsField.lean
theorem uniq_inv_of_isField (R : Type u) [Ring R] (hf : IsField R) :
    ∀ x : R, x ≠ 0 → ∃! y : R, x * y = 1

Proof state:
case hex
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1

Tactic:
exact hf.mul_inv_cancel hx

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = y * (x * z)

Tactic:
rw [hxz, mul_one]

Result:
no goals

Proof state:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂

Tactic:
intro y z hxy hxz

Result:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z

Proof state:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y = z

Tactic:
calc
  y = y * (x * z) := by rw [hxz, mul_one]
  _ = x * y * z := by rw [← mul_assoc, hf.mul_comm y x]
  _ = z := by rw [hxy, one_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ x * y * z = z

Tactic:
rw [hxy, one_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
hf : IsField R
⊢ ∀ (x : R), x ≠ 0 → ∃! y, x * y = 1

Tactic:
intro x hx

Result:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y, x * y = 1

Proof state:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃! y, x * y = 1

Tactic:
apply existsUnique_of_exists_of_unique

Result:
case hex
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∃ x_1, x * x_1 = 1

case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
⊢ ∀ (y₁ y₂ : R), x * y₁ = 1 → x * y₂ = 1 → y₁ = y₂

Proof state:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * (x * z) = x * y * z

Tactic:
rw [← mul_assoc, hf.mul_comm y x]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
/-- Basis vectors are eigenvectors of associated diagonal linear operator. -/
lemma hasEigenvector_toLin_diagonal (d : n → R) (i : n) (b : Basis n R M) :
    HasEigenvector (toLin b b (diagonal d)) (d i) (b i) :=
  ⟨mem_eigenspace_iff.mpr <| by simp [diagonal], Basis.ne_zero b i⟩

Proof state:
R : Type u_1
n : Type u_2
M : Type u_3
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : Nontrivial R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
d : n → R
i : n
b : Basis n R M
⊢ ((toLin b b) (diagonal d)) (b i) = d i • b i

Tactic:
simp [diagonal]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem support_scaleRoots_eq (p : R[X]) {s : R} (hs : s ∈ nonZeroDivisors R) :
    (scaleRoots p s).support = p.support :=
  le_antisymm (support_scaleRoots_le p s)
    (by intro i
        simp only [coeff_scaleRoots, Polynomial.mem_support_iff]
        intro p_ne_zero ps_zero
        have := pow_mem hs (p.natDegree - i) _ ps_zero
        contradiction)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ p.support → i ∈ (p.scaleRoots s).support

Tactic:
simp only [coeff_scaleRoots, Polynomial.mem_support_iff]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ p.coeff i ≠ 0 → p.coeff i * s ^ (p.natDegree - i) ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
⊢ False

Tactic:
have := pow_mem hs (p.natDegree - i) _ ps_zero

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
this : p.coeff i = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
⊢ p.support ≤ (p.scaleRoots s).support

Tactic:
intro i

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ i ∈ p.support → i ∈ (p.scaleRoots s).support

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
this : p.coeff i = 0
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
⊢ p.coeff i ≠ 0 → p.coeff i * s ^ (p.natDegree - i) ≠ 0

Tactic:
intro p_ne_zero ps_zero

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
hs : s ∈ nonZeroDivisors R
i : ℕ
p_ne_zero : p.coeff i ≠ 0
ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0
⊢ False
-- Mathlib/Algebra/MvPolynomial/Expand.lean
theorem expand_comp_bind₁ (p : ℕ) (f : σ → MvPolynomial τ R) :
    (expand p).comp (bind₁ f) = bind₁ fun i ↦ expand p (f i)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
⊢ (expand p).comp (bind₁ f) = bind₁ fun i => (expand p) (f i)

Tactic:
apply algHom_ext

Result:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
⊢ ∀ (i : σ), ((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i => (expand p) (f i)) (X i)

Proof state:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
⊢ ∀ (i : σ), ((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i => (expand p) (f i)) (X i)

Tactic:
intro i

Result:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ ((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i => (expand p) (f i)) (X i)

Proof state:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ ((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i => (expand p) (f i)) (X i)

Tactic:
simp only [AlgHom.comp_apply, bind₁_X_right]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyInjective.lean
lemma isLocallyInjective_sheafToPresheaf_map_iff :
    Presheaf.IsLocallyInjective J ((sheafToPresheaf J D).map φ) ↔ IsLocallyInjective φ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Sheaf J D
φ : F₁ ⟶ F₂
⊢ Presheaf.IsLocallyInjective J ((sheafToPresheaf J D).map φ) ↔ IsLocallyInjective φ

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDeriv_succ' : iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ deriv^[n + 1] f = deriv^[n] (deriv f)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)

Tactic:
rw [iteratedDeriv_eq_iterate, iteratedDeriv_eq_iterate]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ deriv^[n + 1] f = deriv^[n] (deriv f)
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma sinKernel_def (a x : ℝ) : ↑(sinKernel ↑a x) = jacobiTheta₂' a (I * x) / (-2 * π)

Proof state:
a x : ℝ
⊢ ↑(sinKernel (↑a) x) = jacobiTheta₂' (↑a) (I * ↑x) / (-2 * ↑π)

Tactic:
simp [sinKernel, re_eq_add_conj, jacobiTheta₂'_conj, map_ofNat]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_subset_Ico_union_Ico {a b c : α} : Ico a c ⊆ Ico a b ∪ Ico b c

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c

Tactic:
exact Set.Ico_subset_Ico_union_Ico

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c

Tactic:
rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]

Result:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem hasBasis_toFilter (l : IntegrationParams) (I : Box ι) :
    (l.toFilter I).HasBasis (fun r : ℝ≥0 → (ι → ℝ) → Ioi (0 : ℝ) => ∀ c, l.RCond (r c))
      fun r => { π | ∃ c, l.MemBaseSet I c (r c) π }

Proof state:
ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
⊢ (l.toFilter I).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π}

Tactic:
simpa only [setOf_exists] using hasBasis_iSup (l.hasBasis_toFilterDistortion I)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem lapMatrix_mulVec_apply [NonAssocRing R] (v : V) (vec : V → R) :
    (G.lapMatrix R *ᵥ vec) v = G.degree v * vec v - ∑ u ∈ G.neighborFinset v, vec u

Proof state:
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : NonAssocRing R
v : V
vec : V → R
⊢ (lapMatrix R G *ᵥ vec) v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u

Tactic:
simp_rw [lapMatrix, sub_mulVec, Pi.sub_apply, degMatrix_mulVec_apply, adjMatrix_mulVec_apply]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma inv_lt_one₀ (ha : 0 < a) : a⁻¹ < 1 ↔ 1 < a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
simpa using inv_mul_lt_one₀ ha (b := 1)

Result:
no goals