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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * w +
        ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁) =
      z₂ ↔
    w +
        g ↑y *
          (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁)) =
      g ↑y * z₂

Tactic:
← mul_add,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * (w + ↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁) = z₂ ↔
    w +
        g ↑y *
          (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y)⁻¹ * (↑((IsUnit.liftRight ((↑g).domRestrict M) h) y) * z₁)) =
      g ↑y * z₂
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : A
y : ↥A⁰
⊢ mk' K x y = 1 ↔ x = ↑y

Tactic:
by
  have := (algebraMap A K).domain_nontrivial
  refine ⟨?_, fun hxy => by rw [hxy, mk'_self']⟩
  intro hxy
  have hy : (algebraMap A K) ↑y ≠ (0 : K) :=
    IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property
  rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy
  exact IsFractionRing.injective A K hxy

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑b * c + ↑d * a) (b * d)

Tactic:
add_comm (b * c) (d * a),

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑d * a + ↑b * c) (b * d)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ mk a b + mk c b = mk (a + c) b

Tactic:
rw [add_mk, mk_eq_mk_iff, r_eq_r']

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ (r' M) (↑b * c + ↑b * a, b * b) (a + c, b)
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
x : FB
⊢ (fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl) x = AlgEquiv.refl x

Tactic:
obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x

Goal state after:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
x y : B
⊢ (fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl) ((algebraMap B FB) x / (algebraMap B FB) y) =
    AlgEquiv.refl ((algebraMap B FB) x / (algebraMap B FB) y)
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
g : C ≃ₐ[A] D
x : FB
⊢ (fieldEquivOfAlgEquiv FA FB FD (f.trans g)) x =
    ((fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g)) x

Tactic:
obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x

Goal state after:
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
g : C ≃ₐ[A] D
x y : B
⊢ (fieldEquivOfAlgEquiv FA FB FD (f.trans g)) ((algebraMap B FB) x / (algebraMap B FB) y) =
    ((fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g))
      ((algebraMap B FB) x / (algebraMap B FB) y)
Module: Mathlib.RingTheory.Localization.FractionRing

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

Tactic:
apply (h.map_units S 1).ne_zero
    rw [Subsingleton.eq_zero ((1 : nonZeroDivisors R) : R), map_zero]

Goal state after:
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✝ : DecidableEq R
x y : FractionRing R
a c : R
b : ↥R⁰
⊢ (d : ↥R⁰) → Decidable (Localization.mk a b = Localization.mk c d)

Tactic:
d

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✝ : DecidableEq R
x y : FractionRing R
a c : R
b d : ↥R⁰
⊢ Decidable (Localization.mk a b = Localization.mk c d)
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
x y : A
⊢ ∃ s, 1 ⊗ₜ[R] s = x ⊗ₜ[R] y

Tactic:
use x * y

Goal state after:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := ⋯
h✝ : Nontrivial (A ⧸ R')
x y : A
⊢ 1 ⊗ₜ[R] (x * y) = x ⊗ₜ[R] y
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star s.centralizer = (star s).centralizer

Tactic:
by
  simp_rw [centralizer, ← commute_iff_eq]
  conv_lhs => simp only [← star_preimage, preimage_ofPred_eq, ← commute_star_comm]
  conv_rhs => simp only [← image_star, forall_mem_image]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
⊢ ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)

Tactic:
refine fun x y h => ⟨⟨1 - y * x, 1 + y * h.unit.inv * x, ?_, ?_⟩, rfl⟩

Goal state after:
case refine_1
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 - y * x) * (1 + y * h.unit.inv * x) = 1

case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ (1 + y * h.unit.inv * x) * (1 - y * x) = 1
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
m : M
⊢ 1 • m = m

Tactic:
simp only [(· • ·), Algebra.TensorProduct.one_def]
    simp only [moduleAux_apply, one_smul]

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

Goal state before:
pp: A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
a : A
b : B
⊢ spectrum R (a, b) = spectrum R a ∪ spectrum R b

Tactic:
apply compl_injective
  simp_rw [spectrum, Set.compl_union, compl_compl, resolventSet, ← Set.ofPred_and,
    Prod.isUnit_iff, algebraMap_apply, mk_sub_mk]

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
a : A
b : B
⊢ (map f g) (a ⊗ₜ[R] b) ∈ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)

Tactic:
rw [map_tmul, ← mul_one (f a), ← one_mul (g b), ← tmul_mul_tmul]

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
a : A
b : B
⊢ f a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] g b ∈ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)
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
a : R
ha : a ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
c x y : R
x✝¹ : x ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ : y ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hx : 0 ≤ star c * x * c
hy : 0 ≤ star c * y * c
⊢ star c * x * c + 0 ≤ star c * x * c + star c * y * c

Tactic:
gcongr

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
a : R
ha : 0 < a
c : R
hc : IsRegular c
⊢ 0 < star c * a * c

Tactic:
simpa only [mul_zero, zero_mul] using star_left_conjugate_lt_conjugate ha hc

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
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : (c.sum fun i a ↦ a • g i) ∈ M'
⊢ (c.sum fun i a ↦ a • g i) = 0

Tactic:
← Quotient.mk_eq_zero,

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
ι₁ : Type u_2
ι₂ : Type u_3
f : ι₁ → ↥M'
hf : LinearIndependent R f
g : ι₂ → M
hg : LinearIndependent R (Submodule.Quotient.mk ∘ g)
c : ι₂ →₀ R
h₁ : (c.sum fun i a ↦ a • g i) ∈ span R (range fun x ↦ ↑(f x))
h₂ : (c.sum fun i a ↦ a • g i) ∈ span R (range g)
this : Submodule.Quotient.mk (c.sum fun i a ↦ a • g i) = 0
⊢ (c.sum fun i a ↦ a • g i) = 0
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
rw [StarOrderedRing.le_iff] at hxy ⊢
  obtain ⟨p, hp, rfl⟩ := hxy
  refine ⟨f p, ?_, map_add f _ _⟩
  have hf : ∀ r, f (star r) = star (f r) := map_star _
  induction hp using AddSubmonoid.closure_induction
  all_goals aesop

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max v w u, w} #n

Tactic:
← lift_lift.{w, max u v},

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} #m * lift.{max u v, w} (lift.{w, w} #n)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ #ι < ℵ₀

Tactic:
apply Cardinal.lift_lt.1

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{?u.28, w} #ι < lift.{?u.28, w} ℵ₀
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:
rw [← 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.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
⊢ ∀ b < K ∙ v, b = ⊥

Tactic:
· intro T hT
    by_contra h
    apply hT.2
    change span K {v} ≤ T
    simp_rw [span_singleton_le_iff_mem, ← Ne.eq_def, Submodule.ne_bot_iff] at *
    rcases h with ⟨s, ⟨hs, hz⟩⟩
    rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
    rcases eq_or_ne a 0 with rfl | h
    · simp only [zero_smul, ne_eq, not_true] at hz
    · rwa [T.smul_mem_iff h] at hs

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
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 = b ⟨↑v, ⋯⟩

Tactic:
by simp [b]

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
a b✝ : A
s : Set A
hb✝ : b✝ ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
h_star : ∀ b ∈ s, Commute a (star b)
b : A
hb : b ∈ s ∪ star s
⊢ b ∈ star s → Commute a b

Tactic:
simpa using h_star (star b)

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
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ centralizer R ↑(centralizer R s)
h₂ : x✝ ∈ centralizer R ↑(centralizer R s)
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
rw [← SetLike.mem_coe, coe_centralizer_centralizer] at h₁ h₂

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
hcomm✝ : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x
hcomm_star : ∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a
this : adjoin R s ≤ centralizer R ↑(centralizer R s)
x✝¹ x✝ : A
hcomm : ∀ a ∈ s ∪ star s, ∀ b ∈ s ∪ star s, a * b = b * a
h₁ : x✝¹ ∈ (s ∪ star s).centralizer.centralizer
h₂ : x✝ ∈ (s ∪ star s).centralizer.centralizer
⊢ x✝¹ * x✝ = x✝ * x✝¹
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
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
c : R
z : ↥(R ∙ x)
⊢ σ (Classical.choose ⋯) • y = σ c • σ (Classical.choose ⋯) • y

Tactic:
rw [smul_smul, ← RingHom.map_mul, H]
        have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)
        simp only [mul_smul, this]
        apply coe_smul

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
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
x : V
hx : f x = 0
⊢ (g * f) x = 0

Tactic:
Module.End.mul_apply,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f g : V →ₗ[K] V
h : Commute f g
h' : Disjoint f.ker g.ker
x : V
hx : f x = 0
⊢ g (f x) = 0
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
inst✝¹ : Nontrivial E
inst✝ : Free F E
⊢ ⊥ = ⊤ ↔ finrank F E = 1

Tactic:
have := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
  rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]

Goal state after:
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
inst✝¹ : Nontrivial E
inst✝ : Free F E
⊢ ⊥ = ⊤ ↔ finrank F E = 1

Tactic:
by
  have := Module.Free.of_equiv (Subalgebra.topEquiv (R := F) (A := E)).toLinearEquiv.symm
  rw [← finrank_top, ← subalgebra_top_finrank_eq_submodule_top_finrank,
    Subalgebra.finrank_eq_one_iff, eq_comm]

Goal state after:
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
inst✝ : Free F E
⊢ finrank F E = 1 ↔ Function.Bijective ⇑(algebraMap F E)

Tactic:
refine ⟨?_, Module.finrank_of_bijective_algebraMap⟩

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
inst✝ : Free F E
⊢ finrank F E = 1 → Function.Bijective ⇑(algebraMap F E)
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ∀ (r : R), Quot.liftOn ((algebraMap R (FreeAlgebra R X)) r) (liftFun R X f) ⋯ = (algebraMap R A) r

Tactic:
by tauto

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x (p * q) = 0

Tactic:
by
  rw [eval₂_mul f x]
  exact mul_eq_zero_of_left hp (q.eval₂ f x)

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
n : ℕ
⊢ (p * (X - ↑n)).comp q = p.comp q * (q - ↑n)

Tactic:
by
  rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]

Goal state after:
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
x : E × F
⊢ x ∈ f.graph ↔ ∃ y, ↑y = x.1 ∧ ↑f y = x.2

Tactic:
cases x
  simp_rw [mem_graph_iff', Prod.mk_inj]

Goal state after:
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 g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
⊢ x ∈ f.domain ↔ x ∈ g.domain

Tactic:
by simp_rw [mem_domain_iff, h]

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

Goal state before:
pp: case single_add
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Monoid M
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f✝ : M →* A
a : M
b : R
f : R[M]
a✝¹ : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) f) = ((lift R A M) f✝) f
⊢ ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) (single a b + f)) = ((lift R A M) f✝) (single a b + f)

Tactic:
| single_add a b f _ _ ih =>

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✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
a : A
ha : a ∈ (coeff 1).support
⊢ degb a ≤ 0

Tactic:
by rwa [Finset.mem_singleton.mp (Finsupp.support_single_subset ha)]

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

Goal state before:
pp: case single_add
R : Type u_1
S : Type u_2
A : Type u_4
M : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddMonoid M
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring S
inst✝² : Algebra S A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
f✝ : Multiplicative M →* A
a : M
b : R
f : R[M]
a✝¹ : a ∉ f.coeff.support
a✝ : b ≠ 0
ih : ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) f) = ((lift R A M) f✝) f
⊢ ((lift S A M) f✝) ((mapRingHom M (algebraMap R S)) (single a b + f)) = ((lift R A M) f✝) (single a b + f)

Tactic:
| single_add a b f _ _ ih =>

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
n : ℕ
h : natDegree 0 < n
⊢ degree 0 < ↑n

Tactic:
exact WithBot.bot_lt_coe n

Goal state after: