mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
g : B → A
f : F
h : Function.LeftInverse g ⇑f
x : ↥(NonUnitalStarAlgHom.range f)
x' : A
hx' : f x' = ↑x
⊢ f (g ↑x) = ↑x

Tactic:
← hx',

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
g : B → A
f : F
h : Function.LeftInverse g ⇑f
x : ↥(NonUnitalStarAlgHom.range f)
x' : A
hx' : f x' = ↑x
⊢ f (g (f x')) = f x'
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v : ι → V
s t : Set V
x y z : V
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
⊢ Nontrivial (V →ₗ[K] V')

Tactic:
obtain ⟨v, hv⟩ := exists_ne (0 : V)

Goal state after:
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
inst✝¹ : Nontrivial V
inst✝ : Nontrivial V'
v : V
hv : v ≠ 0
⊢ Nontrivial (V →ₗ[K] V')
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ ∀ (b : NonUnitalStarSubalgebra R A), adjoin R s ≤ b ↔ s ⊆ ↑b

Tactic:
S

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ⊆ ↑S
Module: Mathlib.RingTheory.Finiteness.Lattice

Goal state before:
pp: case intro
R : Type u_2
V : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup V
inst✝² : Module R V
ι : Sort u_1
inst✝¹ : Finite ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
val✝ : Fintype (PLift ι)
⊢ Module.Finite R ↥(⨆ i, S i)

Tactic:
rw [← iSup_plift_down, ← Finset.sup_univ_eq_iSup]

Goal state after:
case intro
R : Type u_2
V : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup V
inst✝² : Module R V
ι : Sort u_1
inst✝¹ : Finite ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
val✝ : Fintype (PLift ι)
⊢ Module.Finite R ↥(Finset.univ.sup fun i ↦ S i.down)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ ∃ n b i j, i ≠ j ∧ ↑v = b i ∧ f = b.coord j

Tactic:
refine ⟨n, b, ⟨v, by simp [n, hvs]⟩, ⟨w, by simp [n]⟩, ?_, by simp [b], ?_⟩

Goal state after:
case refine_1
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ ⟨↑v, ⋯⟩ ≠ ⟨w, ⋯⟩

case refine_2
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ f = b.coord ⟨w, ⋯⟩
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ r, r • v₀ = v
H : Module.rank K V < 1
⊢ False

Tactic:
Cardinal.lt_one_iff

Goal state after:
case refine_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Nontrivial K
x✝ : ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ r, r • v₀ = v
H : Module.rank K V = 0
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ < 1
⊢ False

Tactic:
Cardinal.lt_one_iff

Goal state after:
case refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
⊢ False
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f z₁ + ↑g 0 = ↑(f.sup g h) z₂

Tactic:
refine (sup_apply h _ _ _ ?_).symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥f.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑z₁ + ↑0 = ↑z₂
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑f 0 + ↑g z₁ = ↑(f.sup g h) z₂

Tactic:
refine (sup_apply h _ _ _ ?_).symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
z₁ : ↥g.domain
z₂ : ↥(f.sup g h).domain
hz : ↑z₁ = ↑z₂
⊢ ↑0 + ↑z₁ = ↑z₂
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case one_mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f (1 * a✝) = liftFun R X f a✝

Tactic:
change algebraMap _ _ _ * liftFun R X f _ = liftFun R X f _
        simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : ⇑f ∘ ι R = ⇑g ∘ ι R
⊢ f = g

Tactic:
by
  rw [← lift_symm_apply, ← lift_symm_apply] at w
  exact (lift R).symm.injective w

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
pp : Prime p
m : ℕ
hm : m ∣ p
⊢ m = 1 ∨ m = p

Tactic:
by
  obtain ⟨n, hn⟩ := hm
  have := pp.isUnit_or_isUnit hn
  rw [Nat.isUnit_iff, Nat.isUnit_iff] at this
  apply Or.imp_right _ this
  rintro rfl
  rw [hn, mul_one]

Goal state after:
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬2 ≤ n ∨ ¬n = n
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac

Tactic:
eq_self_iff_true,

Goal state after:
n : ℕ
pos : 0 < n
np : ¬2 ≤ n ∨ ¬True
h1 : n = n.minFac
⊢ n.minFac ≤ n / n.minFac
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case mp
n : ℕ
⊢ n.minFac = 2 → 2 ∣ n

pp: case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2

Tactic:
· intro h
    rw [← h]
    exact minFac_dvd n

Goal state after:
case mpr
n : ℕ
⊢ 2 ∣ n → n.minFac = 2
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
q : ℕ
h : ExpChar R q
⊢ ringExpChar R = q

Tactic:
by
  rcases h with _ | h
  · have := CharP.ofCharZero R
    rw [ringExpChar, ringChar.eq R 0]; rfl
  rw [ringExpChar, ringChar.eq R q]
  exact Nat.max_eq_left h.one_lt.le

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx✝⟩) ∈ f.graph

Tactic:
← image_iff hx

Goal state after:
case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ ↑f ⟨x, hx✝⟩ = ↑f ⟨y, hx⟩
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_4
B : Type u_5
M : Type u_7
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Monoid M
φ₁ φ₂ : A[M] →ₐ[R] B
single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1)
single_one_left : φ₁.comp singleOneAlgHom = φ₂.comp singleOneAlgHom
x : A[M]
⊢ φ₁ x = φ₂ x

Tactic:
induction x using induction_linear with

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
· exact h₁.trans h₂.symm

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
⊢ ∀ b ∈ p.coeff.support, b ≠ ap → (∑ x ∈ q.coeff.support, if b + x = ap + aq then p.coeff b * q.coeff x else 0) = 0

Tactic:
refine fun a ha hne => Finset.sum_eq_zero (fun a' ha' => if_neg <| fun he => ?_)

Goal state after:
case h₀
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : SemilatticeSup B
inst✝⁴ : OrderBot B
D : A → B
p q : R[A]
inst✝³ : AddZeroClass A
inst✝² : Add B
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
ap aq : A
hp : supDegree D p ≤ D ap
hq : supDegree D q ≤ D aq
a : A
ha : a ∈ p.coeff.support
hne : a ≠ ap
a' : A
ha' : a' ∈ q.coeff.support
he : a + a' = ap + aq
⊢ False
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
p : R[A]
D : A → B
hp : p ≠ 0
⊢ p.coeff.support.Nonempty

Tactic:
simpa [Finsupp.support_nonempty_iff]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
a✝ : ℕ
h : ↑0 < ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
WithBot.coe_lt_coe,

Goal state after:
case coe
a✝ : ℕ
h : 0 < a✝
⊢ 1 ≤ ↑a✝
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
h : ↑a✝¹ < ↑a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝

Tactic:
WithBot.coe_lt_coe,

Goal state after:
case coe.coe
a✝¹ a✝ : ℕ
h : a✝¹ < a✝
⊢ ↑a✝¹ + 1 ≤ ↑a✝
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff = 0
⊢ (p * q).leadingCoeff = 0

Tactic:
leadingCoeff_eq_zero.1 H,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff = 0
⊢ (0 * q).leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + (C b * X ^ 2 + (C c * X + C d))).degree = 3

Tactic:
← add_assoc (C b * X ^ 2),

Goal state after:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + (C b * X ^ 2 + C c * X + C d)).degree = 3
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + (C b * X ^ 2 + (C c * X + C d))).leadingCoeff = a

Tactic:
← add_assoc (C b * X ^ 2),

Goal state after:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + (C b * X ^ 2 + C c * X + C d)).leadingCoeff = a
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
rw [leadingCoeff_mul']

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
x✝ : ∃ a b, a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
⊢ embDomain f w + embDomain f z = embDomain f y

Tactic:
← embDomain_add,

Goal state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
x✝ : ∃ a b, a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
⊢ embDomain f (w + z) = embDomain f y
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_4
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
h : u + v = embDomain f y
⊢ embDomain f (comapDomain (⇑f) v ⋯) = v

Tactic:
· rw [embDomain_comapDomain ((mem_range_embDomain_iff ..).mp
      (isLowerSet_range_embDomain f (le_iff_exists_add'.mpr ⟨u, h.symm⟩) (by simp)))]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
⊢ p.coeff 0 = (aeval 0) p

Tactic:
simp [coeff_zero_eq_eval_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r (p * (X - C r)) = 0

Tactic:
rw [mul_sub, eval_sub, eval_mul_X, eval_mul_C_of_commute]

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r p * r - eval r p * r = 0

R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ Commute r r
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
x✝ : Invertible 1 := invertibleOne
⊢ p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

Tactic:
simpa using! dvd_comp_C_mul_X_add_C_iff p q 1 (-a)

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

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
hj : m < j
⊢ P.coeff i * Q.coeff j = 0

Tactic:
coeff_eq_zero_of_natDegree_lt hj,

Goal state after:
case inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
hj : m < j
⊢ P.coeff i * 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ C a * X s ^ n = (monomial (Finsupp.single s n)) a

Tactic:
← zero_add (Finsupp.single s n),

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
a : R
n : ℕ
⊢ C a * X s ^ n = (monomial (0 + Finsupp.single s n)) a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (X n).support = {Finsupp.single n 1}

Tactic:
classical rw [X, support_monomial, if_neg]; exact one_ne_zero

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (C r).coeffs ⊆ {r}

Tactic:
coeffs_C

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
⊢ (if r = 0 then ∅ else {r}) ⊆ {r}
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m ((map f) (C a)) = f (coeff m (C a))

Tactic:
clear p

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (a : R) (m : σ →₀ ℕ), coeff m ((map f) (C a)) = f (coeff m (C a))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))

Tactic:
clear p

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p * X n)) = f (coeff m (p * X n))

Tactic:
clear p

Goal state after:
case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      ∀ (m : σ →₀ ℕ), coeff m ((map f) (p * X n)) = f (coeff m (p * X n))
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)) →
      (∀ (m : σ →₀ ℕ), coeff m ((map f) q) = f (coeff m q)) →
        ∀ (m : σ →₀ ℕ), coeff m ((map f) (p + q)) = f (coeff m (p + q))

Tactic:
intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support

Tactic:
classical simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial τ R
f : σ → τ
hf : Injective f
⊢ {x ∈ p.support | x ∈ range (Finsupp.mapDomain f)} ⊆ p.support

Tactic:
exact Finset.filter_subset ..

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1

Tactic:
apply (Multiset.count_le_of_le j degrees_mul_le).trans

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f.degrees + (X j).degrees) ≤ Multiset.count j f.degrees + 1
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Tactic:
rw [le_antisymm_iff, Submodule.mul_le]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ degreesLE R σ s * degreesLE R σ t ∧
    ∀ m ∈ degreesLE R σ s, ∀ n ∈ degreesLE R σ t, m * n ∈ degreesLE R σ (s + t)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
⊢ toMultiset a ≤ s

Tactic:
simpa [a, add_comm (a := t)] using hi

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (C ai * C a * p).natDegree = (C ai * (C a * p)).natDegree

Tactic:
← mul_assoc

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (C ai * C a * p).natDegree = (C ai * C a * p).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * (C a * C ai)).natDegree = (p * C a * C ai).natDegree

Tactic:
← mul_assoc

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * C a * C ai).natDegree = (p * C a * C ai).natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ ((monomial i) r).eraseLead = 0

Tactic:
rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

Goal state after: