mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) = -r /ₒ s

Tactic:
by
  with_unfolding_all rfl

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

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
⊢ (r /ₒ s)⁻¹ = if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩

Tactic:
by
  with_unfolding_all rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') =
    blockDiagonal (fun x_1 ↦ (leftMulMatrix b) x) (i, k) (j, k')

Tactic:
rw [smulTower_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : S
i : m
k : n
j : m
k' : n
⊢ (leftMulMatrix b) (if (i, k).2 = (j, k').2 then (algebraMap S S) x else 0) (i, k).1 (j, k').1 =
    if (i, k).2 = (j, k').2 then (leftMulMatrix b) x (i, k).1 (j, k').1 else 0
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
f g : End A (ι → M)
i✝ j✝ : ι
x✝ : M
⊢ { toFun := fun x ↦ (f * g) (Pi.single j✝ x) i✝, map_add' := ⋯, map_smul' := ⋯ } x✝ =
    (((fun i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ }) * fun i j ↦
          { toFun := fun x ↦ g (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ })
        i✝ j✝)
      x✝

Tactic:
simp only [Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, Matrix.mul_apply,
      LinearMap.coe_sum, Finset.sum_apply]

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
f g : End A (ι → M)
i✝ j✝ : ι
x✝ : M
⊢ f (g (Pi.single j✝ x✝)) i✝ = ∑ x, f (Pi.single x (g (Pi.single j✝ x✝) x)) i✝
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₂ T) ((algebraMap R S₂) n) = (algebraMap R T) z * (algebraMap S₁ T) ↑hunit.unit⁻¹

Tactic:
rw [IsScalarTower.algebraMap_apply R S₂ T, ← hz, map_mul, ← hy]

Goal state after:
case h
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
⊢ a * (algebraMap S₂ T) ((algebraMap R S₂) n) =
    a * (algebraMap S₁ T) ((algebraMap R S₁) m) * (algebraMap S₂ T) ((algebraMap R S₂) ↑(z, ⟨n, hn⟩).2) *
      (algebraMap S₁ T) ↑hunit.unit⁻¹
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
⊢ Nontrivial R ↔ Nontrivial S

Tactic:
by_contra! ⟨_, _⟩ | ⟨_, _⟩

Goal state after:
case inl
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Nontrivial R
right✝ : Subsingleton S
⊢ False

case inr
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Subsingleton R
right✝ : Nontrivial S
⊢ False
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
⊢ Nontrivial R ↔ Nontrivial S

Tactic:
by
  by_contra! ⟨_, _⟩ | ⟨_, _⟩
  · obtain ⟨c, hc⟩ := h.exists_of_eq (x := 1) (y := 0) (Subsingleton.elim _ _)
    simp at hc
  · apply (h.map_units S 1).ne_zero
    rw [Subsingleton.eq_zero ((1 : nonZeroDivisors R) : R), map_zero]

Goal state after:
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ 1 ⊗ₜ[R] (a • (1 / f b)) = f a ⊗ₜ[R] (1 / f b)

Tactic:
← smul_tmul,

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Field A
inst✝¹ : Algebra R A
inst✝ : IsFractionRing R A
a b : R
f : R →+* A := algebraMap R A
hf : f = algebraMap R A
hb : f b ≠ 0
⊢ (a • 1) ⊗ₜ[R] (1 / f b) = f a ⊗ₜ[R] (1 / f b)
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
⊢ NonUnitalNonAssocSemiring α

Tactic:
by
  let zero := e.zero
  let add := e.add
  let mul := e.mul
  let nsmul := e.smul ℕ
  apply e.injective.nonUnitalNonAssocSemiring _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: case e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

Tactic:
Set.inter_eq_right.mpr,

Goal state after:
case e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ = quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ

case e'_4
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ {r | IsUnit r}ᶜ ⊆ quasispectrum R (a * b)
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
s : S
x✝ x y : S ⊗[R] S
hx : (LinearMap.mul' R S).toFun (s • x) = (RingHom.id S) s • (LinearMap.mul' R S).toFun x
hy : (LinearMap.mul' R S).toFun (s • y) = (RingHom.id S) s • (LinearMap.mul' R S).toFun y
⊢ (LinearMap.mul' R S).toFun (s • (x + y)) = (RingHom.id S) s • (LinearMap.mul' R S).toFun (x + y)

Tactic:
simp_all [mul_add]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = (Algebra.TensorProduct.map (centralizer R ↑⊤).val (AlgHom.id R B)).range

Tactic:
← centralizer_coe_map_includeLeft_eq_center_tensorProduct R A B ⊤

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Module.Free R B
⊢ centralizer R ↑includeLeft.range = centralizer R ↑(map includeLeft ⊤)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn : Module.rank R M = ↑n
this✝ : Nontrivial R
this : lift.{u, v} ↑n = lift.{v, u} ↑n
⊢ M ≃ₗ[R] Fin n → R

Tactic:
have hn := Cardinal.lift_inj.{v, u}.2 hn

Goal state after:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝¹¹ : Semiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Free R M
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Fintype η
n : ℕ
hn✝ : Module.rank R M = ↑n
this✝ : Nontrivial R
this : lift.{u, v} ↑n = lift.{v, u} ↑n
hn : lift.{u, v} (Module.rank R M) = lift.{u, v} ↑n
⊢ M ≃ₗ[R] Fin n → R
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)
j : n
⊢ ∀ (v : V), ((bW.sumQuot bQ).coord (Sum.inr j)) v = (bQ.coord j ∘ₗ W.mkQ) v

Tactic:
rw [← LinearMap.ext_iff]

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)
j : n
⊢ (bW.sumQuot bQ).coord (Sum.inr j) = bQ.coord j ∘ₗ W.mkQ
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case left
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ K ∙ v ≠ ⊥

Tactic:
Submodule.ne_bot_iff

Goal state after:
case left
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ∃ x ∈ K ∙ v, x ≠ 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : T ≠ ⊥
⊢ v ∈ T

Tactic:
Submodule.ne_bot_iff

Goal state after:
case right
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
T : Submodule K V
hT : T < K ∙ v
h : ∃ x ∈ T, x ≠ 0
⊢ v ∈ T
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 : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Tactic:
exact mem_top

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
rw [← rank_zero_iff (R := R), ← finrank_eq_rank]
  norm_cast

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c₁ : R
⊢ ∀ (c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y

Tactic:
c₂

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c₁ c₂ : R
⊢ c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
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
inst✝ : Free K V
⊢ finrank K V = 1 ↔ ∃ v, v ≠ 0 ∧ ∀ (w : V), ∃ c, c • v = w

Tactic:
rw [← rank_eq_one_iff]

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ finrank K V = 1 ↔ Module.rank K V = 1
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ Module.rank F ↥S = 1 ↔ S = ⊥

Tactic:
refine ⟨fun h ↦ Subalgebra.eq_bot_of_rank_le_one h.le, ?_⟩

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ S = ⊥ → Module.rank F ↥S = 1
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
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ K ∙ v ≠ ⊥

Tactic:
Submodule.ne_bot_iff

Goal state after:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
v : V
hv : v ∈ S
hv_ne : v ≠ 0
⊢ ∃ x ∈ K ∙ v, x ≠ 0
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
h : finrank K V = 1
x : V
hx : x ≠ 0
y : V
this : K ∙ x = ⊤
⊢ y ∈ ⊤

Tactic:
exact mem_top

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk.mul
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = F (Quot.mk (Rel R X) a)
hb : (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = F (Quot.mk (Rel R X) b)
⊢ (liftAux R ((fun F ↦ ⇑F ∘ ι R) F)) (Quot.mk (Rel R X) (a.mul b)) = F (Quot.mk (Rel R X) (a.mul b))

Tactic:
let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
        let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
        change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
        grind

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Algebra.adjoin R s = ((lift R) Subtype.val).range

Tactic:
← Algebra.adjoin_range_eq_range_freeAlgebra_lift,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Algebra.adjoin R s = Algebra.adjoin R (Set.range Subtype.val)
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ (Finsupp.single a r).support * x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support

Tactic:
support_single_subset

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ {a} * x.coeff.support ⊆ image (fun x ↦ a * x) x.coeff.support
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ x.coeff.support * (Finsupp.single a r).support ⊆ image (fun x ↦ x * a) x.coeff.support

Tactic:
support_single_subset

Goal state after:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
x : k[G]
r : k
a : G
⊢ x.coeff.support * {a} ⊆ image (fun x ↦ x * a) x.coeff.support
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m → m < p → ¬m ∣ p
l : m < p
d : m ∣ p
⊢ m = 1

Tactic:
rcases m with (_ | _ | m)

Goal state after:
case zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 → 0 < p → ¬0 ∣ p
l : 0 < p
d : 0 ∣ p
⊢ 0 = 1

case succ.zero
p : ℕ
p2 : 2 ≤ p
h : 2 ≤ 0 + 1 → 0 + 1 < p → ¬0 + 1 ∣ p
l : 0 + 1 < p
d : 0 + 1 ∣ p
⊢ 0 + 1 = 1

case succ.succ
p : ℕ
p2 : 2 ≤ p
m : ℕ
h : 2 ≤ m + 1 + 1 → m + 1 + 1 < p → ¬m + 1 + 1 ∣ p
l : m + 1 + 1 < p
d : m + 1 + 1 ∣ p
⊢ m + 1 + 1 = 1
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
h✝ : CharZero R
⊢ ∃ q, ExpChar R q

pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
p : ℕ
right✝ : CharP R p
hp : Nat.Prime p
⊢ ∃ q, ExpChar R q

Tactic:
exacts [⟨1, .zero⟩, ⟨p, .prime hp⟩]

Goal state after:
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
⊢ φ₁ = φ₂

Tactic:
by
  ext x
  induction x using induction_linear with
  | zero => simp
  | add => simp_all
  | single m a => simpa [← map_mul] using congr($(single_one_right m) * $single_one_left a)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m + C z * X ^ n).support = 3

Tactic:
rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_notMem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]

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

Goal state before:
pp: case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ n + 1 ≤ k → r ^ (n - k) * ↑(n.choose k) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).degree ≤ ↑n

Tactic:
by
  simpa only [C_1, one_mul] using degree_C_mul_X_pow_le n (1 : R)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
a : ℕ
⊢ (p * (X - C r)).coeff (a + 1) = p.coeff a - p.coeff (a + 1) * r

Tactic:
by simp [mul_sub]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), φ.coeff i = r * c i
c' : ℕ → R := fun i ↦ if i ∈ φ.support then c i else 0
ψ : R[X] := ∑ i ∈ φ.support, (monomial i) (c' i)
i : ℕ
hi : φ.coeff i = 0
⊢ φ.coeff i = r * 0

Tactic:
rwa [mul_zero]

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

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

Tactic:
simpa only [pow_one] using leadingCoeff_C_mul_X_pow a 1

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
h₁ : p.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
h₁,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
h₁ : p.leadingCoeff = 0
⊢ 0 * q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
h₁ : q.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
h₁,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
h₁ : q.leadingCoeff = 0
⊢ p.leadingCoeff * 0 = 0
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
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
hs : s.Nonempty
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
⊢ ⊥ < b

Tactic:
obtain ⟨i, hi⟩ := hs

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder B
inst✝ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
b : B
h : ∀ i ∈ s, supDegree D (f i) < b
i : ι
hi : i ∈ s
⊢ ⊥ < b
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ n * p.leadingCoeff = 0

Tactic:
h₁,

Goal state after:
R : Type u
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ 0 * p.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ n * p.leadingCoeff = 0

Tactic:
h₁,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ 0 * p.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff p.natDegree = 1
hfd : p.natDegree = 0
⊢ p = 1

Tactic:
hfd

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ p = 1
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p : (i : ι) → (R i)[X]
⊢ (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i))
      { toFinsupp := ofCoeff (Finsupp.ofSupportFinite (fun n i ↦ (p i).coeff n) ⋯) } =
    p

Tactic:
ext i n; exact coeff_map _ _

Goal state after: