mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ R ∙ generator (span R {a, ψ ⟨y, ⋯⟩}) = R ∙ generator (ϕ.submoduleImage N)

Tactic:
have : span R {d} ≤ ψ'.submoduleImage N := by
      rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]
      refine ⟨y, yN, ?_⟩
      change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d
      rw [d_eq, ϕy_eq]

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ R ∙ generator (span R {a, ψ ⟨y, ⋯⟩}) = R ∙ generator (ϕ.submoduleImage N)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) S
x : K
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
have : Nonempty S := Sne.to_subtype
  simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
⊢ r /ₒ s + r' /ₒ s' = r' /ₒ s' + r /ₒ s

Tactic:
| _ r' s'
   => 

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
⊢ r /ₒ s + r' /ₒ s' = r' /ₒ s' + r /ₒ s
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c
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₃' : r₁ /ₒ s₁ + r₂ /ₒ s₂ = (s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)
⊢ (universalMulHom (↑f) fS ⋯) ((s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)) =
    (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) (r₂ /ₒ s₂)

Tactic:
clear h₃'

Goal state after:
case c.c
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₂
⊢ (universalMulHom (↑f) fS ⋯) ((s₃ • r₁ + r₃ • r₂) /ₒ (s₃ * s₁)) =
    (universalMulHom (↑f) fS ⋯) (r₁ /ₒ s₁) + (universalMulHom (↑f) fS ⋯) (r₂ /ₒ s₂)
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
⊢ (toMatrix b b) ((lmul R S) 0) = 0

Tactic:
rw [map_zero, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
⊢ basisOfPid b ⊥ = ⟨0, Basis.empty ↥⊥⟩

Tactic:
by
  obtain ⟨n, b'⟩ := Submodule.basisOfPid b ⊥
  let e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty _ : Basis (Fin 0) R (⊥ : Submodule R M))
  obtain rfl : n = 0 := by simpa using Fintype.card_eq.mpr ⟨e⟩
  exact Sigma.eq rfl (Basis.eq_of_apply_eq <| finZeroElim)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι✝ : Type u_1
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : DecidableEq ι✝
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
ι : Type u_5
inst✝¹ : Finite ι
inst✝ : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (End A (ι → A))

Tactic:
← MulOpposite.isStablyFiniteRing_iff,

Goal state after:
ι✝ : Type u_1
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : DecidableEq ι✝
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
ι : Type u_5
inst✝¹ : Finite ι
inst✝ : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (End A (ι → A))ᵐᵒᵖ
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case exists_of_eq
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ ((algebraMap R S).comp h.symm.toRingHom) x = ((algebraMap R S).comp h.symm.toRingHom) y → ∃ c, ↑c * x = ↑c * y

Tactic:
RingHom.comp_apply,

Goal state after:
case exists_of_eq
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (algebraMap R S) (h.symm.toRingHom x) = ((algebraMap R S).comp h.symm.toRingHom) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case exists_of_eq
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (algebraMap R S) (h.symm.toRingHom x) = ((algebraMap R S).comp h.symm.toRingHom) y → ∃ c, ↑c * x = ↑c * y

Tactic:
RingHom.comp_apply,

Goal state after:
case exists_of_eq
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
x y : P
⊢ (algebraMap R S) (h.symm.toRingHom x) = (algebraMap R S) (h.symm.toRingHom y) → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
⊢ ∃ n₀, ∀ n ≥ n₀, (r ^ n • l.sum fun i c ↦ c • ↑i) ∈ B'

Tactic:
choose n₁ n₂ using fun x : Submonoid.closure s => Submonoid.pow_smul_mem_closure_smul r s x.prop

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
⊢ ∃ n₀, ∀ n ≥ n₀, (r ^ n • l.sum fun i c ↦ c • ↑i) ∈ B'
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ Function.Injective ⇑(algebraMap R (FractionRing A))

Tactic:
IsScalarTower.algebraMap_eq R A

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ Function.Injective ⇑((algebraMap A (FractionRing A)).comp (algebraMap R A))
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
p q : R
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hqp : q * p = p
⊢ p * q = p

Tactic:
by simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))

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

Goal state before:

Tactic:
(1 + y * (IsUnit.unit h).inv * x) * (1 - y * x) =
            1 - y * x + y * (h.unit.inv * (1 - x * y)) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.val_inv_mul, mul_one, sub_add_cancel]

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

Goal state before:
pp: 𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
⊢ σ 1 = σ (↑ₐ 1)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, one_smul]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ (algebraMap R S) x ⊗ₜ[R] y ∈ ↑((mk R S M) 1).range

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_tmul]

Goal state after:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ 1 ⊗ₜ[R] (x • y) ∈ ↑((mk R S M) 1).range
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
s : S
r : R
⊢ s ⊗ₜ[R] (r • 1) ∈ ↑((mk R S T).flip 1).range

Tactic:
← smul_tmul

Goal state after:
R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
s : S
r : R
⊢ (r • s) ⊗ₜ[R] 1 ∈ ↑((mk R S T).flip 1).range
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv.symm (equiv x * equiv y) = equiv.symm 1

Tactic:
assumption

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

Goal state before:
pp: case mpr.refine_2
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv.symm (equiv y * equiv x) = equiv.symm 1

Tactic:
assumption

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + x) * (1 + y) = 1

Tactic:
convert congr(1 + $(hy₁)) <;> [noncomm_ring; simp]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
x y : R
inst✝ : IsCancelAdd R
⊢ x ≠ y ∧ x ≤ y ↔ ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p

Tactic:
StarOrderedRing.le_iff,

Goal state after:
R : Type u_1
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
x y : R
inst✝ : IsCancelAdd R
⊢ (x ≠ y ∧ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p) ↔
    ∃ p, p ≠ 0 ∧ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s) ∧ y = x + p
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ unop x ≤ unop y ↔ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p

Tactic:
StarOrderedRing.le_iff,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : StarRing R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x y : Rᵐᵒᵖ
⊢ (∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), unop y = unop x + p) ↔
    ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
classical
  refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le

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
j : n
⊢ ((bW.sumQuot bQ).coord (Sum.inr j)) v = (bQ.coord j) (W.mkQ v)

Tactic:
← LinearMap.comp_apply

Goal state after:
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
j : n
⊢ ((bW.sumQuot bQ).coord (Sum.inr j)) v = (bQ.coord j ∘ₗ W.mkQ) 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
⊢ ⊥.toNonUnitalSubalgebra = ⊥

Tactic:
ext x
  simp only [mem_bot, NonUnitalStarSubalgebra.mem_toNonUnitalSubalgebra, NonUnitalAlgebra.mem_bot]

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

Goal state before:
pp: case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : K ∙ v₀ = ⊤
⊢ Module.rank K ↥(K ∙ v₀) ≤ 1

Tactic:
refine (rank_span_le _).trans_eq ?_

Goal state after:
case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ r, r • v₀ = v
h : K ∙ v₀ = ⊤
⊢ #↑{v₀} = 1
Module: Mathlib.Algebra.Polynomial.Eval.Defs

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

Tactic:
exact sum_monomial_eq _

Goal state after:
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
p q : R[X]
⊢ ∀ (n : ℕ) (a : R),
    map f ((C a * X ^ n).comp q) = (map f (C a * X ^ n)).comp (map f q) →
      map f ((C a * X ^ (n + 1)).comp q) = (map f (C a * X ^ (n + 1))).comp (map f q)

Tactic:
by
      simp +contextual only [pow_succ, ← mul_assoc, comp, forall_const,
        eval₂_mul_X, imp_true_iff, map_X, Polynomial.map_mul]

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

Goal state before:
pp: n a✝ : ℕ
k : ℕ := a✝
h✝¹ : ¬n < k * k
h✝ : ¬k ∣ n
⊢ ¬n < k * k

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
inst✝ : CharZero R
⊢ CharZero R

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
⊢ ExpChar R (ringExpChar R)

Tactic:
by
  obtain ⟨q, _⟩ := ExpChar.exists R
  rwa [ringExpChar.eq R q]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.natDegree + (X ^ n).natDegree = p.natDegree + n

Tactic:
natDegree_X_pow

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ p.natDegree + n = p.natDegree + n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (X ^ n * p).natDegree = p.natDegree + n

Tactic:
commute_X_pow,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p * X ^ n).natDegree = p.natDegree + n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hmax
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this : AddLeftMono B
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q

Tactic:
have := addRightMono_of_addRightStrictMono B

Goal state after:
case hmax
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
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
this✝ : AddLeftMono B
this : AddRightMono B
⊢ ∀ a ∈ (p * q).coeff.support, D a ≤ supDegree D p + supDegree D q
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
i : ℕ
⊢ f 0 * x ^ i = 0

Tactic:
rw [f.map_zero, zero_mul]

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h✝ : p
⊢ 1 ≤ a

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h✝ : ¬p
⊢ 1 ≤ b

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
h✝ : p
⊢ a ≤ 1

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : a ≤ 1
hb : b ≤ 1
h✝ : ¬p
⊢ b ≤ 1

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 1 < a
hb : 1 < b
h✝ : p
⊢ 1 < a

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 1 < a
hb : 1 < b
h✝ : ¬p
⊢ 1 < b

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : a < 1
hb : b < 1
h✝ : p
⊢ a < 1

Tactic:
assumption

Goal state after:
Module: Mathlib.Algebra.Notation.Lemmas

Goal state before:
pp: case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : a < 1
hb : b < 1
h✝ : ¬p
⊢ b < 1

Tactic:
assumption

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
⊢ p = p'

Tactic:
simpa using congr($h X)

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Type u_3
T : Type u_4
U : Type u_5
inst✝⁴ : Semiring S
inst✝³ : CommSemiring T
inst✝² : Semiring U
inst✝¹ : Algebra R S
inst✝ : Algebra T U
φ : R →+* T
ψ : S →+* U
h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)
p : R[X]
a : S
⊢ ψ ((aeval a) p) = (aeval (ψ a)) (map φ p)

Tactic:
by
  conv_rhs => rw [← eval_map_algebraMap]
  rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]

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

Goal state before:
pp: case h
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
i : ℕ
hi : i > P.natDegree
⊢ P.coeff i • Q = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
a✝ : σ →₀ ℕ
⊢ p.coeff a✝ = q.coeff a✝

Tactic:
exact h _

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

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

Tactic:
classical
    rw [coeffs, Finset.image_subset_iff]
    simp_all [coeff_one]

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

Goal state before:
pp: case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d p ≠ 0

Tactic:
assumption

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

Goal state before:
pp: case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ coeff d q ≠ 0

Tactic:
assumption

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s : Finset σ
q : MvPolynomial (↥s) R
n : ℕ := Fintype.card ↥s
e : ↥s ≃ Fin (Fintype.card ↥s) := Fintype.equivFin ↥s
⊢ (rename Subtype.val) q = (rename Subtype.val) ((rename (⇑e.symm ∘ ⇑e)) q)

Tactic:
simp only [Function.comp_def, Equiv.symm_apply_apply, rename_rename]

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₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔ ∀ (m : σ →₀ ℕ), coeff m ((map q) φ) = coeff m 0

Tactic:
simp only [coeff_map, coeff_zero, hr]

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

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : 0 < s i
⊢ s i ≤ degreeOf i p

Tactic:
rw [degreeOf_eq_sup, Finset.le_sup_iff si]

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : 0 < s i
⊢ ∃ b ∈ p.support, s i ≤ b i