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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
⊢ Injective ⇑(Algebra.ofId R S)

Tactic:
intro x y hxy
    obtain ⟨c, eq⟩ := (IsLocalization.eq_iff_exists M S).mp hxy
    obtain ⟨u, hu⟩ := H c.prop
    rwa [← hu, Units.mul_right_inj] at eq

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ Function.Injective ⇑(algebraMap R K) ∧ Function.Surjective ⇑(algebraMap R K) ↔ Function.Surjective ⇑(algebraMap R K)

Tactic:
and_iff_right (IsFractionRing.injective R K)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ Function.Surjective ⇑(algebraMap R K) ↔ Function.Surjective ⇑(algebraMap R K)
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] (f a / f b) = (f a / f b) ⊗ₜ[R] 1

Tactic:
calc 1 ⊗ₜ[R] (f a / f b)
       = 1 ⊗ₜ[R] (a • (1 / f b)) := by rw [← smul_div_assoc, algebraMap_eq_smul_one a]
     _ = f a ⊗ₜ[R] (1 / f b) := by rw [← smul_tmul, algebraMap_eq_smul_one a]
     _ = (b • (f a / f b)) ⊗ₜ[R] (1 / f b) := by rw [smul_def, mul_div_cancel₀ _ hb]
     _ = (f a / f b) ⊗ₜ[R] (b • (1 / f b)) := by rw [smul_tmul]
     _ = (f a / f b) ⊗ₜ[R] 1 := by rw [smul_def, mul_div_cancel₀ _ hb]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : InvolutiveStar α
⊢ a⋆ ∈ s⋆ ↔ a ∈ s

Tactic:
by simp only [mem_star, star_star]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star {c | ∀ m ∈ s, Commute m c} = {c | ∀ m ∈ star s, Commute m c}

Tactic:
conv_lhs => simp only [← star_preimage, preimage_ofPred_eq, ← commute_star_comm]

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ {a | ∀ m ∈ s, Commute (star m) a} = {c | ∀ m ∈ star s, Commute m c}
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case a.add
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ y✝ : A ⊗[R] M
a✝¹ : (liftBaseChange A l) x✝ ∈ Submodule.span A ↑l.range
a✝ : (liftBaseChange A l) y✝ ∈ Submodule.span A ↑l.range
⊢ (liftBaseChange A l) (x✝ + y✝) ∈ Submodule.span A ↑l.range

Tactic:
· rw [map_add]
      exact add_mem ‹_› ‹_›

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

Goal state before:
pp: case tmul
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
⊢ r • x * a ⊗ₜ[R] b = r • (x * a ⊗ₜ[R] b)

Tactic:
| tmul a b =>

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

Goal state before:
pp: case tmul
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✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass S A A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
a : A
b : B
⊢ r • (x * a ⊗ₜ[R] b) = x * r • a ⊗ₜ[R] b

Tactic:
| tmul a b =>

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

pp: case refine_2
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 + y) * (1 + x) = 1

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

Goal state after:
case refine_2
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 + y) * (1 + x) = 1
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case h.right
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (↑hx.unit⁻¹ - 1 + 1) * (1 + x) - 1 = 0
⊢ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0

Tactic:
convert this

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (↑hx.unit⁻¹ - 1 + 1) * (1 + x) - 1 = 0
⊢ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = (↑hx.unit⁻¹ - 1 + 1) * (1 + x) - 1
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: case h.left
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * (↑hx.unit⁻¹ - 1 + 1) - 1 = 0
⊢ ↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0

Tactic:
convert this

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * (↑hx.unit⁻¹ - 1 + 1) - 1 = 0
⊢ ↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = (1 + x) * (↑hx.unit⁻¹ - 1 + 1) - 1
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:
by
  rw [spectrum.zero_mem_iff]
  rintro ⟨u, hu⟩
  simpa [-Units.mul_inv, hu] using congr($(u.mul_inv).fst)

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

Goal state before:
pp: 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
x : Unitization R A
⊢ s • x = ((inlRingHom R A).comp (algebraMap S R)) s * x

Tactic:
induction x with
    | inl_add_inr =>
      change _ = inl (algebraMap S R s) * _
      rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
| Module.rank R (M ⧸ M') + Module.rank R ↥M'

Tactic:
simp only [Module.rank_def]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
M' : Submodule R M
| (⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial R
| Module.rank R M + Module.rank R M₁

Tactic:
simp only [Module.rank_def]

Goal state after:
R : Type u
M M₁ : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : Nontrivial 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)
v : V
j : n
⊢ ((bW.sumQuot bQ).coord (Sum.inr j)) v = (bQ.coord j ∘ₗ W.mkQ) v

Tactic:
revert v

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

Goal state before:
pp: 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'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
⊢ ∃ g, g ∘ₗ f = id

Tactic:
let hB := Basis.ofVectorSpace K V

Goal state after:
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'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ ∃ g, g ∘ₗ f = id
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
p : Submodule K V
v : V
hv : v ∉ p
f : V →ₗ[K] K
hpf : f ∘ₗ p.subtype = 0
hfv : f v = 1
x : V
hx : x ∈ p
⊢ x ∈ f.ker

Tactic:
simpa using congr($hpf ⟨x, hx⟩)

Goal state after:
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
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
zero : p 0 ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯
star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯
a : A
ha : a ∈ adjoin R s
x : A
hx✝ : x ∈ s ∪ Star.star s
hx : Star.star x ∈ s
⊢ Star.star x ∈ s ∪ Star.star s

Tactic:
by simpa using Or.inl hx

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

Goal state before:
pp: case hx
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 := ⋯
s : Set V := ⋯
hs : span K s = f.ker
n : Set V := ⋯
⊢ v ∉ span K s

Tactic:
· simp [hs, hfv]

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
N : Submodule R M
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
have := nontrivial_of_invariantBasisNumber R
  have := rank_quotient_add_rank_le N
  rw [← finrank_eq_rank R M, ← finrank_eq_rank R, ← N.finrank_eq_rank] at this
  exact mod_cast this

Goal state after:
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
⊢ (adjoin R s).toNonUnitalSubalgebra ≤ (centralizer R ↑(centralizer R s)).toNonUnitalSubalgebra

Tactic:
centralizer_toNonUnitalSubalgebra,

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
⊢ (adjoin R s).toNonUnitalSubalgebra ≤ NonUnitalSubalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case pos
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
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
x : E
hx : x ∈ S
h1 : Unique κ
⊢ x ∈ range ⇑(algebraMap F E)

Tactic:
obtain ⟨y, hy⟩ := (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ
      Finsupp.uniqueLinearEquiv _ _ default).symm).surjective ⟨x, hx⟩

Goal state after:
case pos
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
h : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
x : E
hx : x ∈ S
h1 : Unique κ
y : F
hy : (algebraMap F ↥S) y = ⟨x, hx⟩
⊢ x ∈ range ⇑(algebraMap F E)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), 1 * a = a

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ 1 * Quot.mk (Rel R X) a✝ = Quot.mk (Rel R X) a✝
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), a * 1 = a

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝ * 1 = Quot.mk (Rel R X) a✝
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), 0 * a = 0

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ 0 * Quot.mk (Rel R X) a✝ = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), a * 0 = 0

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝ * 0 = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), 0 + a = a

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ 0 + Quot.mk (Rel R X) a✝ = Quot.mk (Rel R X) a✝
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), a + 0 = a

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝ + 0 = Quot.mk (Rel R X) a✝
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (x : FreeAlgebra R X), 0 • x = 0

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ 0 • Quot.mk (Rel R X) a✝ = 0
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type ?u.7
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x✝ : R
⊢ ∀ (x : FreeAlgebra A X),
    ({ toFun := fun r ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ }.comp
            (algebraMap R A))
          x✝ *
        x =
      x *
        ({ toFun := fun r ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                map_add' := ⋯ }.comp
            (algebraMap R A))
          x✝

Tactic:
rintro ⟨⟩

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type ?u.7
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x✝¹ : R
x✝ : FreeAlgebra A X
a✝ : Pre A X
⊢ ({ toFun := fun r ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
              map_add' := ⋯ }.comp
          (algebraMap R A))
        x✝¹ *
      Quot.mk (Rel A X) a✝ =
    Quot.mk (Rel A X) a✝ *
      ({ toFun := fun r ↦ Quot.mk (Rel A X) (Pre.ofScalar r), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
              map_add' := ⋯ }.comp
          (algebraMap R A))
        x✝¹
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
⊢ (((lift R) fun x ↦ (MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x)).comp
          ((MonoidAlgebra.lift R (FreeAlgebra R X) (FreeMonoid X)) (FreeMonoid.lift (ι R)))).comp
      MonoidAlgebra.singleOneAlgHom =
    (AlgHom.id R R[FreeMonoid X]).comp MonoidAlgebra.singleOneAlgHom

Tactic:
by ext

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

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

Tactic:
by rw [← C_1, C_comp]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
of : X → ↥s := Subtype.coind (ι R) grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
⊢ motive a

Tactic:
suffices a = lift R of a by
    rw [this]
    exact Subtype.prop (lift R of a)

Goal state after:
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
motive : FreeAlgebra R X → Prop
grade0 : ∀ (r : R), motive ((algebraMap R (FreeAlgebra R X)) r)
grade1 : ∀ (x : X), motive (ι R x)
mul : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a * b)
add : ∀ (a b : FreeAlgebra R X), motive a → motive b → motive (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := grade0 }
of : X → ↥s := Subtype.coind (ι R) grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
⊢ a = ↑(((lift R) of) a)
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
hab : a = a * b
⊢ b = 1

Tactic:
← mul_right_inj' (Nat.ne_zero_of_lt h1),

Goal state after:
a b : ℕ
h : 2 ≤ a * b ∧ ∀ (m : ℕ), m ∣ a * b → m = 1 ∨ m = a * b
h1 : 1 < a * b
hab : a = a * b
⊢ a * b * b = a * b * 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
p : E →ₛₗ.[σ] F
hpc : p ∈ c
⊢ p ≤ { domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }

Tactic:
refine ⟨le_sSup <| Set.mem_image_of_mem domain hpc, fun x y hxy => Eq.symm ?_⟩

Goal state after:
case h
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
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
p : E →ₛₗ.[σ] F
hpc : p ∈ c
x : ↥p.domain
y : ↥{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } }.domain
hxy : ↑x = ↑y
⊢ ↑{ domain := sSup (domain '' c), toFun := { toFun := f, map_add' := ⋯, map_smul' := ⋯ } } y = ↑p x
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: 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 : E →ₗ.[R] F
hf : f.toFun.ker = ⊥
x : F × E
hv : x ∈ Submodule.map (↑(LinearEquiv.prodComm R E F)) f.graph
hv' : x.1 = 0
⊢ x.2 = 0

Tactic:
rcases x with ⟨x, y⟩
  subst hv'
  simp only [Submodule.map_equiv_eq_comap_symm, Submodule.mem_comap, LinearEquiv.symm_prodComm,
    LinearEquiv.coe_coe, LinearEquiv.prodComm_apply, mem_graph_iff, Prod.swap] at hv
  rcases hv with ⟨z, rfl, hz⟩
  rw [LinearMap.ker_eq_bot'] at hf
  simp [hf z hz]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (if k = n then x else 0) = if n = k then x else 0

Tactic:
simp [eq_comm]

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (C a * X ^ n).degree = ↑n

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ max p.degree ↑n

Tactic:
rw [max_insert, max_comm]
    exact le_rfl

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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : AddCommMonoid S
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
n : ℕ
p : R[X]
hn : p.degree < ↑n
hp : p = 0
i : Fin n
a✝ : i ∈ univ
⊢ f (↑i) (coeff 0 ↑i) = 0

Tactic:
exact hf i

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
n : ℕ
⊢ #(C c * X ^ n).support ≤ 1

Tactic:
← card_singleton n

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
n : ℕ
⊢ #(C c * X ^ n).support ≤ #{n}
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hp : Monic 0
⊢ False

Tactic:
simp [Monic] at hp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : n = 0
⊢ (p ^ n).natDegree = n * p.natDegree

Tactic:
by simp [*]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
u : R[X]ˣ
⊢ (↑u).natDegree = 0

Tactic:
by
  nontriviality R
  exact natDegree_eq_of_degree_eq_some (degree_coe_units u)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support, b ≠ p.natDegree → (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0

Tactic:
case =>

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    (fun a b ↦ (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0

Tactic:
case =>

Goal state after: