mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝¹ : (i : κ) → Lattice (π i)
inst✝ : Nonempty κ
⊢ (pi univ fun x ↦ ⊥) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom i) (L i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (monomial n) 1 = X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
s : Finset (Submodule R M)
hsS : ↑s ⊆ S
hs : m ∈ ⨆ i ∈ s, i
⊢ ⨆ i, ⨆ (_ : i ∈ S ∧ i ∈ s), i = ⨆ i ∈ s, i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
⊢ X ≠ C a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ X * p = p * X

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ sSup S ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ X ^ n * p = p * X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * X ^ n * q = p * q * X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X = (monomial (n + 1)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
⊢ (monomial n) r * X ^ k = (monomial (n + k)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ X * (monomial n) r = (monomial (n + 1)) r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ ((lsum R) fun x ↦ f x • φ).range = Set.range f • φ.range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k n : ℕ
r : R
⊢ X ^ k * (monomial n) r = (monomial (n + k)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[ℕ]
⊢ { toFinsupp := p }.coeff = ⇑p.coeff

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set σ
f : σ → R
⊢ f '' s • ⊤ = ((lsum R) fun i ↦ f ↑i • LinearMap.id).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Injective coeff

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ f.toFinsupp.coeff i = f.coeff i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
m n : ℕ
inst✝ : Semiring R
⊢ ((monomial n) a).coeff m = if n = m then a else 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ s • ⊤ = ((lsum R) fun i ↦ ↑i • LinearMap.id).range

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ coeff 1 n = if n = 0 then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ coeff 1 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
this : ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ ((monomial (n + 1)) a).coeff 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ X.coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ n ∈ p.support ↔ p.coeff n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ n ∉ p.support ↔ p.coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
⊢ (C a).coeff n = if n = 0 then a else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
h : n ≠ 0
⊢ (C a).coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
n : ℕ
⊢ (C r).coeff (n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
m n : ℕ
inst✝ : Semiring R
⊢ (↑m).coeff n = ↑(if n = 0 then m else 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ (OfNat.ofNat a).coeff (n + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ C a * X ^ (n + 1) = (monomial (n + 1)) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ (C a * X ^ n).toFinsupp = single n a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
⊢ C a * X = (monomial 1) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).toFinsupp = single 1 a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ Subsingleton R → Subsingleton R[X]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a} = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : Type u_1
inst✝ : AddZeroClass M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)
⊢ Set.EqOn ⇑f ⇑g {p | ∃ n a, p = (monomial n) a}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ p = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ ((monomial n) a).support = {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
⊢ (C c * X).support ⊆ {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
h : c ≠ 0
⊢ (C c * X ^ n).support = {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
⊢ (C c * X ^ n).support ⊆ {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).toFinsupp = single n 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ a • X ^ n = (monomial n) a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).support = {n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ X.support = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.support = {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
i j : ℕ
⊢ (monomial i) a = (monomial j) a ↔ i = j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ C u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p * q = ∑ i ∈ p.support, q.sum fun j a ↦ (monomial (i + j)) (p.coeff i * a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ p.sum (f + g) = p.sum f + p.sum g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun n a ↦ C a * X ^ n) = p

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : GeneralLinearGroup R M
⊢ (f * g).toLinearEquiv = f.toLinearEquiv * g.toLinearEquiv

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ f⁻¹.toLinearEquiv = f.toLinearEquiv⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M ≃ₗ[R] M
⊢ ofLinearEquiv (f * g) = ofLinearEquiv f * ofLinearEquiv g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
⊢ ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
⊢ ofLinearEquiv f⁻¹ = (ofLinearEquiv f)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : GeneralLinearGroup R M
⊢ (x * y).toLinearEquiv = x.toLinearEquiv * y.toLinearEquiv

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ ↑((generalLinearEquiv R M) f) = ↑f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ ∀ (s : Finset ℕ), motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
p : Submodule R M
hp : p ∈ {p | p ≤ Submodule.comap f p}
q : Submodule R M
hq : q ∈ {p | p ≤ Submodule.comap f p}
⊢ p ⊓ q ∈ {p | p ≤ Submodule.comap f p}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: M : Type u_2
inst✝⁷ : AddCommMonoid M
R : Type u_3
S : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : DistribSMul S R
inst✝¹ : SMulCommClass R S M
inst✝ : IsScalarTower S R M
f : End R M
c : Sˣ
⊢ (c • f).invtSubmodule = f.invtSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
⊢ ⊤ ∈ f.invtSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
⊢ ⊥ ∈ f.invtSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
x✝ : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⟨p, hp⟩ ≤ ⟨⊤, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
⊢ motive p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : End R M
x✝ : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⟨⊥, ⋯⟩ ≤ ⟨p, hp⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : Submodule R M
⊢ x ∈ ⊤ → x ∈ invtSubmodule 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : Submodule R M
⊢ x ∈ ⊤ → x ∈ invtSubmodule LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⊥ ∈ f.invtSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
⊢ ⊤ ∈ f.invtSubmodule

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n) a)
n : ℕ
a : R
_h : motive (C a * X ^ n)
⊢ motive (C a * X ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).toFinsupp = AddMonoidAlgebra.erase n p.toFinsupp

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[ℕ]
n : ℕ
⊢ { toFinsupp := AddMonoidAlgebra.erase n p } = erase n { toFinsupp := p }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).support = p.support.erase n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (monomial n) (p.coeff n) + erase n p = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
⊢ (erase n p).coeff i = if i = n then 0 else p.coeff i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (erase n 0).toFinsupp = toFinsupp 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ (erase n ((monomial n) a)).toFinsupp = toFinsupp 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).coeff n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
h : i ≠ n
⊢ (erase n p).coeff i = p.coeff i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
⊢ (p.update n a).coeff i = if i = n then a else p.coeff i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ Disjoint p q ↔ Disjoint ↑p ↑q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff n = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
a : R
h : i ≠ n
⊢ (p.update n a).coeff i = p.coeff i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.update n 0 = erase n p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint p q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ Codisjoint p q ↔ Codisjoint ↑p ↑q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl p q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.update n 0).support = p.support.erase n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : ↥f.invtSubmodule
⊢ IsCompl p q ↔ IsCompl ↑p ↑q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
simp_rw [coeffs, Finset.image_subset_iff]

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ ∀ x ∈ support 1, coeff 1 x ∈ {1}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ coeffs 1 ⊆ {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ p.coeff n ∈ p.coeffs

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ p.coeffs = ∅

Tactic:
by

Goal state after: