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

Goal state before:
pp: 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)
⊢ (universalMulHom (↑f) fS ⋯) (0 /ₒ 1) = 0

Tactic:
universalMulHom_apply

Goal state after:
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)
⊢ ↑(fS 1)⁻¹ * ↑f 0 = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
let _sI : I → N := fun i ↦ ⟨s i.1, subset_span (mem_range_self i)⟩

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
⊢ (n : ℕ) × Basis (Fin n) R M
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:

Tactic:
(∏ j ∈ {i}ᶜ, a j) • a i • s i ∈ N := N.smul_mem _ (ha' i)
        _ = (∏ j, a j) • s i := by rw [Fintype.prod_eq_prod_compl_mul i, mul_smul]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ mk' (Localization M) ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m

Tactic:
mk'_eq_iff_eq_mul,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) =
    (algebraMap A (Localization M)) m * (algebraMap R (Localization M)) ↑1
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝²² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝²¹ : CommSemiring S
inst✝²⁰ : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : Rₘ
⊢ ((↑(algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ)) x = ((algebraMap Rₘ' Sₙ').comp ↑(algEquiv M Rₘ Rₘ')) x

Tactic:
algEquiv_comp_algebraMap M Rₘ Sₙ Rₘ'

Goal state after:
R : Type u_1
inst✝²² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝²¹ : CommSemiring S
inst✝²⁰ : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
x : Rₘ
⊢ ((algebraMap Rₘ' Sₙ').comp ↑(algEquiv M Rₘ Rₘ')) x = ((algebraMap Rₘ' Sₙ').comp ↑(algEquiv M Rₘ Rₘ')) x
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: case h₁
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝

Tactic:
simp only [star_star]

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

Goal state before:
pp: case h₂
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
x✝ : α
⊢ x✝⋆⋆ = x✝

Tactic:
simp only [star_star]

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Semiring β
mul : Mul α := e.mul
add_monoid_with_one : AddMonoidWithOne α := e.addMonoidWithOne
npow : Pow α ℕ := Equiv.pow ℕ e
⊢ Semiring α

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

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x y z : A ⊗[R] B
⊢ (LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul ∘ₗ mul =
    (((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B))
          ↑LinearMap.lflip)
        ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul.flip ∘ₗ mul)).flip

Tactic:
ext xa xb ya yb za zb

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalSemiring A
inst✝⁶ : Module R A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : IsScalarTower R A A
inst✝³ : NonUnitalSemiring B
inst✝² : Module R B
inst✝¹ : SMulCommClass R B B
inst✝ : IsScalarTower R B B
x y z : A ⊗[R] B
xa : A
xb : B
ya : A
yb : B
za : A
zb : B
⊢ ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((AlgebraTensorModule.curry
                      ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul ∘ₗ mul))
                    xa)
                  xb))
              ya)
            yb))
        za)
      zb =
    ((AlgebraTensorModule.curry
          (((AlgebraTensorModule.curry
                (((AlgebraTensorModule.curry
                      (((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
                              (A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B))
                            ↑LinearMap.lflip)
                          ((LinearMap.llcomp R (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B →ₗ[R] A ⊗[R] B)) mul.flip ∘ₗ mul)).flip)
                    xa)
                  xb))
              ya)
            yb))
        za)
      zb
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
r : R
a b c : A
h₁ : (↑ₐ r - a) * b = 1
h₂ : c * (↑ₐ r - a) = 1
⊢ b * (↑ₐ r - a) = 1

Tactic:
← left_inv_eq_right_inv h₂ h₁

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a b c : A
h₁ : (↑ₐ r - a) * b = 1
h₂ : c * (↑ₐ r - a) = 1
⊢ c * (↑ₐ r - a) = 1
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
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ resolvent a r - resolvent b r = resolvent a r * (a - b) * resolvent b r

Tactic:
rw [resolvent_eq ha, resolvent_eq hb, Units.eq_mul_inv_iff_mul_eq, Units.eq_inv_mul_iff_mul_eq,
    sub_mul, Units.inv_mul, mul_sub, ← mul_assoc, Units.mul_inv, one_mul, mul_one,
    hb.unit_spec, ha.unit_spec]
  abel

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:
by rw [Algebra.algebraMap_eq_smul_one, one_smul]

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✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
F : Type u_6
inst✝¹ : FunLike F (Unitization R A) B
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), φ ↑a = ψ ↑a
h' : ∀ (r : R), φ ((algebraMap R (Unitization R A)) r) = ψ ((algebraMap R (Unitization R A)) r)
⊢ φ = ψ

Tactic:
by
  refine DFunLike.ext φ ψ (fun x ↦ ?_)
  induction x
  simp only [map_add, ← algebraMap_eq_inl, h, h']

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a

Tactic:
simp_rw [IsStrictlyPositive.iff_of_unital, hu.star_right_conjugate_nonneg_iff]

Goal state after:
A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
u a : A
hu : IsUnit u
⊢ 0 ≤ a ∧ IsUnit (u * a * star u) ↔ 0 ≤ a ∧ IsUnit a
Module: Mathlib.Algebra.Algebra.StrictPositivity

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit (↑u * a * ↑(star u)) ↔ 0 ≤ a ∧ IsUnit a

Tactic:
Units.isUnit_mul_units,

Goal state after:
A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit (↑u * a) ↔ 0 ≤ a ∧ IsUnit a
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
inst✝² : Free R M
m : Type w
n : Type w'
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n M) = lift.{max v w', w} #m * lift.{max v w, w'} #n * lift.{max w w', v} (Module.rank R M)

Tactic:
cases nonempty_fintype m
  cases nonempty_fintype n
  obtain ⟨I, b⟩ := Module.Free.exists_basis (R := R) (M := M)
  rw [← (b.matrix m n).mk_eq_rank'']
  simp only [mk_prod, lift_mul, lift_lift, ← mul_assoc, b.mk_eq_rank'']

Goal state after:
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
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : ⊤ ≤ span K t
⊢ range ⇑(extendLe hs hst ht) = hs.extend hst

Tactic:
coe_extendLe,

Goal state after:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
ht : ⊤ ≤ span K t
⊢ range Subtype.val = hs.extend hst
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
s : Set A
hs : s = ↑S
x : A
hx : x ∈ s
⊢ star x ∈ (S.copy s hs).carrier

Tactic:
change star x ∈ s
      rw [hs] at hx ⊢
      exact S.star_mem' hx

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : NonUnitalSemiring A
inst✝² : StarRing A
inst✝¹ : Module R A
inst✝ : StarModule R A
S : NonUnitalSubalgebra R A
r : R
x : A
hx : x ∈ star S.carrier
⊢ r • x ∈ star S.carrier

Tactic:
by simpa only [Set.mem_star, NonUnitalSubalgebra.mem_carrier]
        using (star_smul r x).symm ▸ SMulMemClass.smul_mem (star r) hx

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ↑(iSup K) ⊆ ⋃ i, ↑(K i)

Tactic:
rw [coe_iSup_of_directed dir]

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
⊢ LinearIndepOn K _root_.id {v}

Tactic:
simpa using hv

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

Goal state before:
pp: K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
⊢ IsAtom S ↔ finrank K ↥S = 1

Tactic:
refine ⟨fun hS ↦ ?_, fun hS ↦ ⟨by aesop, fun T hT ↦ ?_⟩⟩
  · obtain ⟨v : V, hv : v ∈ S, hv_ne : v ≠ 0⟩ := S.ne_bot_iff.mp hS.ne_bot
    suffices K ∙ v = S by rw [← this, finrank_span_singleton hv_ne]
    have : K ∙ v ≠ ⊥ := by
      rw [Submodule.ne_bot_iff]
      exact ⟨v, mem_span_singleton_self v, hv_ne⟩
    rwa [← hS.le_iff_eq this, span_le, Set.singleton_subset_iff]
  · have : FiniteDimensional K S := .of_finrank_eq_succ hS
    have : FiniteDimensional K T := .of_injective (inclusion hT.le) (inclusion_injective hT.le)
    rw [← finrank_eq_zero (R := K)]
    by_contra h
    exact hT.ne <| eq_of_le_of_finrank_le hT.le <| by lia

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

Goal state before:
pp: case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ eval₂ f x ↑n + eval₂ f x 1 = ↑(n + 1)

Tactic:
ih,

Goal state after:
case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ ↑n + eval₂ f x 1 = ↑(n + 1)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case h
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
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
⊢ x ∈ (-f).domain ↔ x ∈ g.domain

Tactic:
have : (0 : E →ₛₗ.[σ] F).domain = ⊤ := zero_domain

Goal state after:
case h
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
f g : E →ₛₗ.[σ] F
h' : f + g = 0
x : E
this : domain 0 = ⊤
⊢ x ∈ (-f).domain ↔ x ∈ g.domain
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x * y ∈ S

Tactic:
| mul x y hx hy =>

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
⊢ (single x r * f).coeff.support = Finset.map (mulLeftEmbedding x) f.coeff.support

Tactic:
ext; simp [support_coeff_single_mul_eq_image f hr (.all x)]

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

Goal state before:
pp: n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1

Tactic:
exact (h m mlt hm).symm.eq_one_of_dvd mdvd

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

Goal state before:
pp: n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = n.minFac * 1
⊢ n.minFac ≤ n / n.minFac

Tactic:
rw [mul_one] at h1
    rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, _root_.or_false,
      not_le] at np
    rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]

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

Goal state before:
pp: k : ℕ
⊢ 1 < k + 2

Tactic:
apply Nat.succ_lt_succ

Goal state after:
k : ℕ
⊢ 0 < k + 1
Module: Mathlib.Algebra.Polynomial.Coeff

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

Tactic:
by
      grw [AddMonoidAlgebra.support_coeff_mul_subset]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ p.natDegree = q.natDegree

Tactic:
unfold natDegree; rw [h]

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

Goal state before:
pp: case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)

Tactic:
Finset.prod_empty,

Goal state after:
case refine_1
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D 1 ≤ ∑ i ∈ ∅, supDegree D (f i)
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
⊢ q ≠ 0

Tactic:
refine mt ?_ h; exact fun hq => by rw [hq, leadingCoeff_zero, mul_zero]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree

Tactic:
conv =>

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : (monomial p.natDegree) p.leadingCoeff + erase p.natDegree p = p
hq : (monomial q.natDegree) q.leadingCoeff + erase q.natDegree q = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (erase q.natDegree p + -erase q.natDegree q).degree
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hq0 : q ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
⊢ (-(p - q)).degree < q.degree

Tactic:
neg_sub

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hd : p.degree = q.degree
hq0 : q ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
⊢ (q - p).degree < q.degree
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
hpl : 0 < p.degree
h✝ : Subsingleton R
⊢ ¬IsUnit p

Tactic:
simp [Subsingleton.elim p 0] at hpl

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.degree < (p * X).degree

Tactic:
have : leadingCoeff p * leadingCoeff X ≠ 0 := by simpa

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
this✝ : Nontrivial R
this : p.leadingCoeff * X.leadingCoeff ≠ 0
⊢ p.degree < (p * X).degree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < (X ^ n).degree

Tactic:
degree_X_pow,

Goal state after:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < ↑n
Module: Mathlib.Algebra.MonoidAlgebra.Degree

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

Tactic:
ih,

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (C ((algebraMap R A) r)).toFinsupp = (algebraMap R (AddMonoidAlgebra A ℕ)) r

Tactic:
rw [toFinsupp_C]

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ AddMonoidAlgebra.single 0 ((algebraMap R A) r) = (algebraMap R (AddMonoidAlgebra A ℕ)) r
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
⊢ IsLowerSet (Set.range (embDomain f))

Tactic:
rintro _ y h ⟨z, rfl⟩
  obtain ⟨w, hw⟩ := exists_add_of_le h
  rw [mem_range_embDomain_iff]
  trans ↑(y + w).support
  · exact fun _ ↦ by simp; grind
  · simp [← hw]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
p q : R[X]
a b : R
inst✝ : Invertible a
⊢ p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟a * (X - C b)) ∣ q

Tactic:
by
  convert! map_dvd_iff <| algEquivCMulXAddC a b using 2
  simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (f + g) = g.support

Tactic:
rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ ∏ a ∈ s.support, (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a = 0

Tactic:
apply Finset.prod_eq_zero ha

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ (if h : a ∈ range f then X ((Equiv.ofInjective f hf).symm ⟨a, h⟩) else 0) ^ s a = 0