mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
⊢ False

Tactic:
have : ({r} : Set M) ⊆ closure (S \ {r}) := by
      simp only [hr, pow_zero, one_mul] at hr'
      rw [hr', Set.singleton_subset_iff]
      refine mul_mem ?_ ?_ <;> refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _ <;>
        rw [← hr'] <;> simpa using hs

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
this : {r} ⊆ ↑(closure (↑S \ {r}))
⊢ False
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + z = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + z)

Tactic:
induction z with

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
⊢ r₁ /ₒ s₁ + r₂ /ₒ s₂ + r₃ /ₒ s₃ = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ z • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = z • (r₁ /ₒ s₁) + z • (r₂ /ₒ s₂)

Tactic:
induction z with

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : R
s₃ : ↥S
⊢ (r₃ /ₒ s₃) • (r₁ /ₒ s₁ + r₂ /ₒ s₂) = (r₃ /ₒ s₃) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₂ /ₒ s₂)
Module: Mathlib.RingTheory.OreLocalization.Basic

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

Tactic:
rcases oreDivAddChar' r r' s s' with ⟨ra, sa, ha, ha'⟩

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : DistribMulAction R X
r : X
s : ↥S
r' : X
s' : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s = ra * ↑s'
ha' : r /ₒ s + r' /ₒ s' = (sa • r + ra • r') /ₒ (sa * s)
⊢ r /ₒ s + r' /ₒ s' = r' /ₒ s' + r /ₒ s
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrix v₁ v₁) (f ∘ₗ g) = (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g

Tactic:
LinearMap.toMatrix_comp v₁ v₁ v₁ f g

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g = (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g
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
x : OreLocalization S X
⊢ -x + x = 0

Tactic:
by
  induction x with | _ r s; simp

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

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
z : OreLocalization S R
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₂ /ₒ s₂ + z) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + z • (r₁ /ₒ s₁)

Tactic:
induction z with

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
⊢ (r₂ /ₒ s₂ + r₃ /ₒ s₃) • (r₁ /ₒ s₁) = (r₂ /ₒ s₂) • (r₁ /ₒ s₁) + (r₃ /ₒ s₃) • (r₁ /ₒ s₁)
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)
x y : OreLocalization S R
⊢ (↑(universalMulHom (↑f) fS hf)).toFun (x + y) =
    (↑(universalMulHom (↑f) fS hf)).toFun x + (↑(universalMulHom (↑f) fS hf)).toFun y

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe]
      induction x with | _ r₁ s₁
      induction y with | _ r₂ s₂
      rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨r₃, s₃, h₃, h₃'⟩
      rw [h₃']
      clear h₃'
      simp only [smul_eq_mul, universalMulHom_apply, MonoidHom.coe_coe,
        Submonoid.smul_def]
      simp only [mul_inv_rev, map_mul, map_add, map_mul, Units.val_mul]
      rw [mul_add, mul_assoc, ← mul_assoc _ (f s₃), hf, ← Units.val_mul]
      simp only [one_mul, inv_mul_cancel, Units.val_one]
      congr 1
      rw [← mul_assoc]
      congr 1
      norm_cast at h₃
      have h₃' := Subtype.coe_eq_of_eq_mk h₃
      rw [← Units.val_mul, ← mul_inv_rev, ← fS.map_mul, h₃']
      rw [Units.inv_mul_eq_iff_eq_mul, Units.eq_mul_inv_iff_mul_eq, ← hf, ← hf]
      simp only [map_mul]

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

Goal state before:
pp: case pos
ι : 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, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
i : ι
hi : i ∈ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ N

pp: case neg
ι : 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, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
i : ι
hi : i ∉ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ N

Tactic:
· use 1, zero_ne_one.symm
        rw [one_smul]
        exact subset_span (mem_range_self (⟨i, hi⟩ : I))

Goal state after:
case neg
ι : 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, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
i : ι
hi : i ∉ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ N
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
s : ↥S
hs :
  ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
    ↑s * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
⊢ update 0 i ↑s ∈ T

Tactic:
apply update_self i s.1 0 ▸ s.2

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r : R i
s : ↥S
⊢ update 0 i ↑s ∈ T

Tactic:
apply update_self i s.1 0 ▸ s.2

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

Goal state before:
pp: case e'_3.hf
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map (↑h) M) S
⊢ Injective ⇑↑h

Tactic:
exact h.toEquiv.injective

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

Goal state before:
pp: 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
⊢ ∃ x, a * (algebraMap S₁ T) ↑x.2 = (algebraMap S₁ T) x.1

Tactic:
by
    obtain ⟨⟨y, -, m, hm, rfl⟩, hy⟩ := surj (M := Algebra.algebraMapSubmonoid S₂ M₁) a
    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₁ T] at hy
    obtain ⟨⟨z, n, hn⟩, hz⟩ := IsLocalization.surj (M := M₂) y
    have hunit : IsUnit (algebraMap R S₁ m) := map_units _ ⟨m, hm⟩
    use ⟨algebraMap R S₁ z * hunit.unit⁻¹, ⟨algebraMap R S₁ n, n, hn, rfl⟩⟩
    rw [map_mul, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T]
    conv_rhs => rw [← IsScalarTower.algebraMap_apply]
    rw [IsScalarTower.algebraMap_apply R S₂ T, ← hz, map_mul, ← hy]
    convert_to _ = a * (algebraMap S₂ T) ((algebraMap R S₂) n) *
        (algebraMap S₁ T) (((algebraMap R S₁) m) * hunit.unit⁻¹.val)
    · rw [map_mul]
      ring
    simp

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

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

Tactic:
by
  let mul := e.mul
  let add_monoid_with_one := e.addMonoidWithOne
  let npow := e.pow ℕ
  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✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight) = ⊤

Tactic:
rw [← top_le_iff]

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ⊤ ≤ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)
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
n : R
r : A
x✝¹ : B
x✝ : M
⊢ (((n • r) • (Algebra.lsmul R R M).toLinearMap) x✝¹) x✝ =
    (((RingHom.id R) n • r • (Algebra.lsmul R R M).toLinearMap) x✝¹) x✝

Tactic:
simp only [RingHom.id_apply, LinearMap.smul_apply, smul_assoc]

Goal state after:
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
n : R
r : A
⊢ (n • r) • (Algebra.lsmul R R M).toLinearMap = (RingHom.id R) n • r • (Algebra.lsmul R R M).toLinearMap

Tactic:
ext
        simp only [RingHom.id_apply, LinearMap.smul_apply, smul_assoc]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts a f

Tactic:
by rfl

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
⊢ ((inlRingHom R A).comp (algebraMap S R)) s * x = x * ((inlRingHom R A).comp (algebraMap S R)) s

Tactic:
by
    induction x with
    | inl_add_inr =>
      change inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
      rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective ⇑φ
r : R
a : A
⊢ (starMap φ) (mk (r, a)) = inl r + ↑(φ a)

Tactic:
by rfl

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

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
ha : ∀ (x y : R), y = x + x✝ → x ≤ y
hb : ∀ (x y : R), y = x + y✝ → x ≤ y
x : R
⊢ x ≤ x + (x✝ + y✝)

Tactic:
rw [← add_assoc]

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
h_le_iff : ∀ (x y : R), x ≤ y ↔ ∃ s, y = x + star s * s
p : R
hp : p ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
x✝ y✝ : R
hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s ↦ star s * s)
ha : ∀ (x y : R), y = x + x✝ → x ≤ y
hb : ∀ (x y : R), y = x + y✝ → x ≤ y
x : R
⊢ x ≤ x + x✝ + y✝
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
⊢ 0 ≤ star c * x * c

Tactic:
exact hx

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✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
⊢ (∀ (x : M), (∃ x, x ≠ 0) ∧ x = 0) ↔ ∀ (x : M), x = 0

Tactic:
and_iff_right (exists_ne (0 : R))

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✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
obtain ⟨g, sum, z, nonzero⟩ := Fintype.not_linearIndependent_iff.mp
    (mt LinearIndependent.finset_card_le_finrank h.not_ge)
  refine ⟨Subtype.val.extend g 0, ?_, z, z.2, by rwa [Subtype.val_injective.extend_apply]⟩
  rw [← Finset.sum_finset_coe]; convert! sum; apply Subtype.val_injective.extend_apply

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
v : V
hfv : f v ≠ 0
b₁ : Basis (↑(Basis.ofVectorSpaceIndex K ↥f.ker)) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
x : V
⊢ ∃ a, x + a • v ∈ span K s

Tactic:
use -f x / f v

Goal state after:
case h
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 := ⋯
H₁ : LinearIndepOn K _root_.id n
x : V
⊢ x + (-f x / f v) • v ∈ span K s
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
ι : Type u_1
⊢ Module.Finite R (ι →₀ M) → Nonempty ι → Nontrivial M → Module.Finite R M ∧ Finite ι

Tactic:
rintro h ⟨i⟩ _

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
h : Module.Finite R (ι →₀ M)
i : ι
a✝ : Nontrivial M
⊢ Module.Finite R M ∧ Finite ι
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
ι : Type u_1
inst✝ : IsEmpty ι
hV : Module.rank K V = 0
⊢ Subsingleton V

Tactic:
by
    obtain ⟨_, b⟩ := Module.Free.exists_basis (R := K) (M := V)
    have := mk_eq_zero_iff.1 (hV ▸ b.mk_eq_rank'')
    exact b.repr.toEquiv.subsingleton

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x ((monomial n) r) = f r * x ^ n

Tactic:
by
  simp [eval₂_eq_sum]

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

Goal state before:
pp: case add
R : Type u
inst✝ : Semiring R
p✝ r p q : R[X]
hp : (p * X).comp r = p.comp r * r
hq : (q * X).comp r = q.comp r * r
⊢ ((p + q) * X).comp r = (p + q).comp r * r

Tactic:
simp only [hp, hq, add_mul, add_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)
this : a = ↑(((lift R) of) a)
⊢ motive ↑(((lift R) of) a)

Tactic:
exact Subtype.prop (lift R of a)

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

Goal state before:
pp: case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
pp : Prime n
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
simpa only [k, h] using
        ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
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
x : F
hx : x✝ ∈ f.domain
h✝ : ↑f ⟨x✝, ⋯⟩ = x
⊢ x✝ ∈ f.domain

Tactic:
exact hx

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x

Tactic:
by
  let : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).1
  exact CharP.cast_eq_zero_iff R (ringChar R)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (X * p).coeff (n + 1) = p.coeff n

Tactic:
by
  rw [(commute_X p).eq, coeff_mul_X]

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, f (↑i) (coeff 0 ↑i) = sum 0 f

Tactic:
sum_zero_index,

Goal state after:
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, f (↑i) (coeff 0 ↑i) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
a : WithBot ℕ
b : ℕ
hp : p.degree ≤ a
⊢ (p ^ b).degree ≤ ↑b * a

Tactic:
induction b with

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✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ supDegree D (p + q) = supDegree D p

Tactic:
apply (supDegree_add_le.trans <| sup_le le_rfl h.le).antisymm
  obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D (ne_zero_of_not_supDegree_le h.not_ge)
  rw [he] at h ⊢
  apply Finset.le_sup
  simpa [coeff_eq_zero_of_not_le_supDegree h.not_ge] using ha

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

Goal state before:
pp: case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ (p.coeff - q.coeff) (Function.invFun D (supDegree D p)) = 0

Tactic:
Finsupp.sub_apply,

Goal state after:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : Ring R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q).coeff (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ p.coeff (Function.invFun D (supDegree D p)) - q.coeff (Function.invFun D (supDegree D p)) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).coeff = ⇑f ∘ p.coeff

Tactic:
by
  ext n; exact coeff_map ..

Goal state after: