mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) x * (lmul R S) y) = (toMatrix b b) ((lmul R S) x) * (toMatrix b b) ((lmul R S) y)

Tactic:
LinearMap.toMatrix_mul

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b) ((lmul R S) x) * (toMatrix b b) ((lmul R S) y) =
    (toMatrix b b) ((lmul R S) x) * (toMatrix b b) ((lmul R S) y)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ ↑((fS s₁)⁻¹ * (fS s₃)⁻¹) * f r₃ = ↑(fS s₂)⁻¹

Tactic:
← mul_inv_rev,

Goal state after:
case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ ↑(fS s₃ * fS s₁)⁻¹ * f r₃ = ↑(fS s₂)⁻¹
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
⊢ ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))

Tactic:
by
  cases nonempty_fintype ι
  induction O using inductionOnRank b generalizing N with | ih M0 ih =>
  obtain ⟨m, b'M⟩ := M0.basisOfPid b
  by_cases N_bot : N = ⊥
  · subst N_bot
    exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩
  obtain ⟨y, hy, a, _, M', M'_le_M, N', _, N'_le_M', y_ortho, _, h⟩ :=
    Submodule.basis_of_pid_aux M0 N b'M N_bot N_le_O
  obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M'
  obtain ⟨bN, h'⟩ := h n' bN'
  obtain ⟨hmn, bM, h''⟩ := h' m' hn'm' bM'
  obtain ⟨as, has⟩ := h'' as' has'
  exact ⟨_, _, hmn, bM, bN, as, has⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
hxy : mk' S x y ≠ 0
⊢ x ≠ 0

Tactic:
by
  rintro rfl
  exact hxy (IsLocalization.mk'_zero _)

Goal state after:
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
⊢ IsRegular (mk' S r m) ↔ IsRegular r

Tactic:
have (n : M) (x y : R) : n * x = n * y ↔ x = y := (hM _ n.2).1.eq_iff

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), ↑n * x = ↑n * y ↔ x = y
⊢ IsRegular (mk' S r m) ↔ IsRegular r
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ a * ↑d - ↑b * c = 0

Tactic:
apply hu'

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
x✝ : ∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)
u : R
hu : u ∈ M
h : u * (↑d * a) = u * (↑b * c)
hu' : ∀ (x : R), u * x = 0 → x = 0
⊢ u * (a * ↑d - ↑b * c) = 0
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add : Add α := e.add
⊢ Sort ?u.13

Tactic:
let mul := Equiv.mul e

Goal state after:
α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add : Add α := e.add
mul : Mul α := e.mul
⊢ Sort ?u.13
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalCommRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
⊢ NonUnitalCommRing α

Tactic:
apply e.injective.nonUnitalCommRing _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x y : (Unitization R A)ˣ
hx : (↑x).toProd.1 = 1
hy : (↑y).toProd.1 = 1
⊢ x * y ∈ {x | (↑x).toProd.1 = 1}

Tactic:
simp [hx, hy]

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ (∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x

Tactic:
rintro ⟨y, hy₁, hy₂⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ IsQuasiregular x
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ 0 ∈ spectrum R ↑a

Tactic:
rw [spectrum.zero_mem_iff]

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ ¬IsUnit ↑a
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
s : S
r✝ : R
a✝ : A
⊢ inl ((algebraMap S R) s) * (inl r✝ + ↑a✝) = (inl r✝ + ↑a✝) * inl ((algebraMap S R) s)

Tactic:
rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
η : Type u₁'
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
inst✝ : Fintype η
⊢ Module.rank R (η → R) = ↑(Fintype.card η)

Tactic:
by
  rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
v : V
hv : v ∈ W
j : n
this : W.mkQ v = 0
⊢ ((bW.sumQuot bQ).repr v) (Sum.inr j) = 0

Tactic:
by simp [sumQuot_repr_inr, this]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: case neg
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : ¬finrank R M = 0
⊢ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val

Tactic:
exact exists_finset_linearIndependent_of_le_rank
    ((Nat.cast_le.mpr hn).trans_eq (cast_toNat_of_lt_aleph0 (toNat_ne_zero.mp h).2))

Goal state after:
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
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
⊢ ⊤ ≤ span K (Set.range fun x ↦ _root_.id ↑x)

Tactic:
by simpa using H₂

Goal state after:
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : NonUnitalSemiring A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module R A
inst✝¹² : NonUnitalSemiring B
inst✝¹¹ : StarRing B
inst✝¹⁰ : Module R B
inst✝⁹ : FunLike F A B
inst✝⁸ : NonUnitalAlgHomClass F R A B
inst✝⁷ : StarHomClass F A B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
ι : Sort u_1
inst✝³ : Nonempty ι
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalStarSubalgebra R A
⊢ map f (⨅ i, S i) = ⨅ i, map f (S i)

Tactic:
apply SetLike.coe_injective

Goal state after:
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : NonUnitalSemiring A
inst✝¹⁴ : StarRing A
inst✝¹³ : Module R A
inst✝¹² : NonUnitalSemiring B
inst✝¹¹ : StarRing B
inst✝¹⁰ : Module R B
inst✝⁹ : FunLike F A B
inst✝⁸ : NonUnitalAlgHomClass F R A B
inst✝⁷ : StarHomClass F A B
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
ι : Sort u_1
inst✝³ : Nonempty ι
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalStarSubalgebra R A
⊢ ↑(map f (⨅ i, S i)) = ↑(⨅ i, map f (S i))
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
⊢ ⊤ ≤ span K (Set.range fun x ↦ _root_.id ↑x)

Tactic:
by simpa using H₂

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: 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, ⋯⟩

Tactic:
apply_fun (f ∘ (↑))

Goal state after:
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 := ⋯
w : V
hw : f w = 1
s : Set V := ⋯
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := ⋯
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := ⋯
⊢ (⇑f ∘ Subtype.val) ⟨↑v, ⋯⟩ ≠ (⇑f ∘ Subtype.val) ⟨w, ⋯⟩
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀

Tactic:
simp_rw [rank_eq_one_iff, le_span_singleton_iff]

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ r, r • v₀ = v
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ finrank K ↥(K ∙ v) ≤ 1

Tactic:
exact finrank_span_le_card ({v} : Set V)

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

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
w : V
hS : finrank K ↥S = 1
hw : w ∈ S
hw0 : w ≠ 0
this : FiniteDimensional K ↥S
⊢ finrank K ↥S ≤ finrank K ↥(K ∙ w)

Tactic:
hS,

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
w : V
hS : finrank K ↥S = 1
hw : w ∈ S
hw0 : w ≠ 0
this : FiniteDimensional K ↥S
⊢ 1 ≤ finrank K ↥(K ∙ w)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
ps : List R[X]
hf : ∀ p ∈ ps, ∀ (k : ℕ), Commute (f (p.coeff k)) x
⊢ eval₂ f x ps.prod = (List.map (eval₂ f x) ps).prod

Tactic:
induction ps using List.reverseRecOn with

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

Goal state before:
pp: p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ¬∃ m n, m < p ∧ n < p ∧ m * n = p

Tactic:
push Not

Goal state after:
p : ℕ
⊢ Prime p ↔ 2 ≤ p ∧ ∀ (m n : ℕ), m < p → n < p → m * n ≠ p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
⊢ ↑a = 0 ↔ ↑p ∣ a

Tactic:
rcases lt_trichotomy a 0 with (h | rfl | h)
  · rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]
    lift -a to ℕ using Int.neg_nonneg.mpr (le_of_lt h) with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
  · simp
  · lift a to ℕ using le_of_lt h with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

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

Goal state before:
pp: case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ n.minFacProp 2

pp: case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)

Tactic:
· exact ⟨le_rfl, d2, fun k k2 _ => k2⟩

Goal state after:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ n.minFacProp (n.minFacAux 3)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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
y : F
hx : (x, y) ∈ f.graph
⊢ (x, y) ∈ g.graph

Tactic:
exact h hx

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case hc
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
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ ∀ x ∈ g, x.1 = 0 → x.2 = 0

Tactic:
· exact hg

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ #(p * q).support ≤ #p.support * #q.support

Tactic:
calc #(p * q).support
    _ = #(p.toFinsupp * q.toFinsupp).coeff.support := by rw [← support_toFinsupp, toFinsupp_mul]
    _ ≤ #(p.toFinsupp.coeff.support + q.toFinsupp.coeff.support) := by
      grw [AddMonoidAlgebra.support_coeff_mul_subset]
    _ ≤ #p.support * #q.support := Finset.card_image₂_le ..

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
_fd : A
fds : _fd ∈ f.coeff.support
_gd : A
gds : _gd ∈ g.coeff.support
⊢ degb (_fd + _gd) ≤ f.coeff.support.sup degb + g.coeff.support.sup degb

Tactic:
degbm,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : Add A
inst✝² : Add B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
f g : R[A]
_fd : A
fds : _fd ∈ f.coeff.support
_gd : A
gds : _gd ∈ g.coeff.support
⊢ degb _fd + degb _gd ≤ f.coeff.support.sup degb + g.coeff.support.sup degb
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).coeff.support.inf degt =
    (Multiset.map (fun f ↦ f.coeff.support.inf degt) (Multiset.map (fun i ↦ f i) s.val)).sum

Tactic:
Multiset.map_map

Goal state after:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).coeff.support.inf degt = (Multiset.map ((fun f ↦ f.coeff.support.inf degt) ∘ fun i ↦ f i) s.val).sum
Module: Mathlib.Algebra.Polynomial.Degree.Defs

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

Tactic:
by
  rw [Nat.cast_withBot]
  exact Finset.le_sup (mem_support_iff.2 h)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p = C (p.coeff 0)

Tactic:
ext (_ | n)

Goal state after:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
⊢ p.coeff 0 = (C (p.coeff 0)).coeff 0

case succ
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree ≤ 0
n : ℕ
⊢ p.coeff (n + 1) = (C (p.coeff 0)).coeff (n + 1)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (p + q).coeff p.natDegree ≠ 0

Tactic:
by
      rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]
      exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p ^ 0).degree ≤ 0 • p.degree

Tactic:
pow_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ degree 1 ≤ 0 • p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.leadingCoeff ^ 0 ≠ 0
⊢ (p ^ 0).degree = 0 • p.degree

Tactic:
pow_zero,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : 1 ≠ 0
⊢ degree 1 = 0 • p.degree
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 q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q

Tactic:
← he,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬D (Function.invFun D (D a)) ≤ supDegree D q
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (p - q).degree = p.degree

Tactic:
by
  rw [← degree_neg q] at h
  rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]

Goal state after:
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 q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hq : Monic D q
hp : p ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
by
  cases subsingleton_or_nontrivial R; · exact (hp (Subsingleton.elim _ _)).elim
  apply supDegree_mul hD hadd ?_ hp hq.ne_zero
  simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
this : f.coeff i = 0
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
simp [this, Ne.symm hi, coeff_monomial]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D (p ^ 0) = 0 • supDegree D p

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
inst✝⁷ : Semiring R
A : Type u_8
B : Type u_9
inst✝⁶ : AddMonoid A
inst✝⁵ : AddMonoid B
inst✝⁴ : LinearOrder B
inst✝³ : OrderBot B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
D : A → B
p : R[A]
n : ℕ
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hD : Function.Injective D
inst✝ : Nontrivial R
hp : Monic D p
⊢ supDegree D 1 = 0 • supDegree D p
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case add
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
k : ℕ
x y : S ⊗[R] N
hx : X ^ k • (rTensor N (↑R (monomial 0))) x = (rTensor N (↑R (monomial k))) x
hy : X ^ k • (rTensor N (↑R (monomial 0))) y = (rTensor N (↑R (monomial k))) y
⊢ X ^ k • (rTensor N (↑R (monomial 0))) (x + y) = (rTensor N (↑R (monomial k))) (x + y)

Tactic:
simp [hx, hy]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g (p ^ 0) = eval₂ f g p ^ 0

Tactic:
pow_zero,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ eval₂ f g 1 = eval₂ f g p ^ 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0

Tactic:
push Not

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∃ d, coeff d p ≠ 0) ↔ ∃ d, coeff d p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
h : i ≠ j
⊢ degreeOf i (X j ^ 0) = 0

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
h : i ≠ j
⊢ degreeOf i 1 = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
⊢ degreeOf i (p * X i ^ 0) = degreeOf i p + 0

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
⊢ degreeOf i (p * 1) = degreeOf i p + 0