mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
⊢ (fun i j ↦ (c • f) ((single R (fun x ↦ R) i) 1) j) = (RingHom.id Rᵐᵒᵖ) c • fun i j ↦ f ((single R (fun x ↦ R) i) 1) j

Tactic:
by
    ext i j
    simp only [Pi.smul_apply, LinearMap.smul_apply, RingHom.id_apply, Matrix.smul_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (toLinearMapRight' 1) x = x

Tactic:
Matrix.toLinearMapRight'_one,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ LinearMap.id x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (toLinearMapRight' 1) x = x

Tactic:
Matrix.toLinearMapRight'_one,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ LinearMap.id x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst✝⁵ : Finite m
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
this : Fintype m
⊢ ((toLin v₁ v₂) A) x = 0 ↔ ∀ (j : m), (A *ᵥ ⇑(v₁.repr x)) j = 0

Tactic:
toLin_apply

Goal state after:
m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
R : Type u_7
M₁ : Type u_8
M₂ : Type u_9
inst✝⁵ : Finite m
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
A : Matrix m n R
x : M₁
this : Fintype m
⊢ ∑ j, (A *ᵥ ⇑(v₁.repr x)) j • v₂ j = 0 ↔ ∀ (j : m), (A *ᵥ ⇑(v₁.repr x)) j = 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✝¹ : Module.Finite R M
inst✝ : IsTorsionFree R M
⊢ Free R M

Tactic:
obtain ⟨n, b⟩ : Σ n, Basis (Fin n) R M := Module.basisOfFiniteTypeTorsionFree'
  exact Module.Free.of_basis b

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
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
M0 : Submodule R M
ih :
  ∀ N' ≤ M0,
    ∀ x ∈ M0,
      (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) →
        ∀ N ≤ N', ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
N : Submodule R M
N_le_O : N ≤ M0
m : ℕ
b'M : Basis (Fin m) R ↥M0
N_bot : N = ⊥
⊢ ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))

Tactic:
subst N_bot
    exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩

Goal state after:
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⁰
this : Nontrivial A
hxy : mk' K x y = 1
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y

Tactic:
IsFractionRing.mk'_eq_div,

Goal state after:
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⁰
this : Nontrivial A
hxy : (algebraMap A K) x / (algebraMap A K) ↑y = 1
hy : (algebraMap A K) ↑y ≠ 0
⊢ x = ↑y
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ n • l a • ↑a ∈ Subalgebra.toSubmodule B'

Tactic:
← tsub_add_cancel_of_le this,

Goal state after:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ (n - n₁ a + n₁ a) • l a • ↑a ∈ Subalgebra.toSubmodule B'
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
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy :
  (algebraMap S₁ T) x * (algebraMap S₁ T) ((algebraMap R S₁) ↑d) =
    (algebraMap S₁ T) y * (algebraMap S₁ T) ((algebraMap R S₁) ↑d)
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
simp_rw [← map_mul, hr, hs, ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R S₂ T] at hxy

Goal state after:
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
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
⊢ ∃ c, ↑c * x = ↑c * y
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
Sₘ : Type u_5
inst✝³ : CommSemiring Sₘ
inst✝² : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra R Sₘ
inst✝ : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit ((algebraMap R Sₘ) ↑y)

Tactic:
by
  rw [IsScalarTower.algebraMap_apply _ S]
  exact IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
⊢ Algebra.IsEpi R A

Tactic:
refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun a ↦ ?_

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : Surjective ⇑(algebraMap R A)
a : A
⊢ 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
Module: Mathlib.Algebra.Ring.TransferInstance

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

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

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

Goal state before:
pp: R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑(n + 1) ⊗ₜ[R] 1 = ↑n ⊗ₜ[R] 1 + 1

Tactic:
by simp [add_tmul, one_def]

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
inst✝ : Nontrivial A
r : R
a : A
⊢ r ∈ σ a ↔ resolvent a r = 0

Tactic:
refine ⟨resolvent_zero_of_mem_spectrum, fun hr ↦ ?_⟩
  simpa [mem_iff, Ring.not_isUnit_iff_inverse_eq_zero]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Ring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : EquivLike F A B
inst✝ : AlgEquivClass F R A B
f : F
a : A
⊢ spectrum R a ⊆ spectrum R (f a)

Tactic:
simpa only [AlgEquiv.coe_toAlgHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
      AlgHom.spectrum_apply_subset (AlgEquivClass.toAlgEquiv f : A ≃ₐ[R] B).symm (f a)

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ (∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x

Tactic:
· rintro ⟨y, hy₁, hy₂⟩
    refine ⟨⟨equiv x, equiv y, ?_, ?_⟩, rfl⟩
    all_goals
      apply equiv.symm.injective
      assumption

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ IsQuasiregular x ↔ IsUnit (1 + ↑x)

Tactic:
refine ⟨?_, fun hx ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ IsQuasiregular x → IsUnit (1 + ↑x)

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ IsQuasiregular x
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : IsQuasiregular ↑a
⊢ IsQuasiregular a

Tactic:
rw [isQuasiregular_iff] at ha ⊢

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : ∃ y, y + ↑a + ↑a * y = 0 ∧ ↑a + y + y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0
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
hf : Function.LeftInverse f ⇑(algebraMap R S)
h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)
s : S
hs : s ∈ quasispectrum S a
⊢ (algebraMap R S) (f s) = s

Tactic:
rw [mem_quasispectrum_iff] at hs
    obtain (rfl | hs) := hs
    · simpa using hf 0
    · obtain ⟨r, rfl⟩ := h hs
      rw [hf r]

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

Goal state before:
pp: case inl_add_inr
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
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = inl (s • r✝) + ↑((s • 1) • a✝)

Tactic:
inl_smul,

Goal state after:
case inl_add_inr
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
r✝ : R
a✝ : A
⊢ s • inl r✝ + s • ↑a✝ = s • inl r✝ + ↑((s • 1) • a✝)
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
⊢ (includeLeft.comp f).range ⊔ (includeRight.comp g).range ≤ (map f g).range

Tactic:
rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]

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
⊢ ((map f g).comp includeLeft).range ⊔ ((map f g).comp includeRight).range ≤ (map f g).range
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
inst✝ : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
⊢ #ι ≤ ↑(finrank R M)

Tactic:
rw [← lift_le.{max v w}]
  simpa only [← finrank_eq_rank, lift_natCast, lift_le_nat_iff] using h.cardinal_lift_le_rank

Goal state after:
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
ι : Type u_2
inst✝ : Fintype ι
v : ι → M
hv : span R (range v) = ⊤
⊢ (range v).toFinset.card ≤ Fintype.card ι

Tactic:
convert! Fintype.card_range_le v; rw [Set.toFinset_card]

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

Goal state before:
pp: case pos
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val

Tactic:
rw [le_zero_iff.mp (hn.trans_eq h)]
    exact ⟨∅, rfl, by convert! linearIndependent_empty R M using 2 <;> aesop⟩

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

Goal state before:
pp: case refine_2
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₁ ⋯
i : ↑n
⊢ f (b i) = (Finsupp.single i 1) ⟨w, ⋯⟩

Tactic:
simp only [b]

Goal state after:
case refine_2
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₁ ⋯
i : ↑n
⊢ f ((Basis.mk H₁ ⋯) i) = (Finsupp.single i 1) ⟨w, ⋯⟩
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ finrank K V = 1 ↔ Module.rank K V = 1

Tactic:
exact toNat_eq_iff one_ne_zero

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
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
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
⊢ ∀ (x y : ↥(f.domain ⊔ g.domain)), fg (x + y) = fg x + fg y

Tactic:
rintro ⟨z₁, hz₁⟩ ⟨z₂, hz₂⟩
    rw [← add_assoc, add_right_comm (f _), ← map_add, add_assoc, ← map_add]
    apply fg_eq
    simp only [coe_add, ← add_assoc]
    rw [add_right_comm (x _), hxy, add_assoc, hxy, coe_mk, coe_mk]

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
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ finrank F ↥S = 1 ↔ Module.rank F ↥S = 1

Tactic:
exact toNat_eq_iff one_ne_zero

Goal state after:
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:
by
    rintro ⟨⟩
    exact Quot.sound Rel.mul_one

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add_assoc
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
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ + liftFun R X f c✝ = liftFun R X f a✝ + (liftFun R X f b✝ + liftFun R X f c✝)

Tactic:
rw [add_assoc]

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
p : T[X]
g : ℕ → T → R[X]
x : S
⊢ eval₂ f x (p.sum g) = p.sum fun n a ↦ eval₂ f x (g n a)

Tactic:
let T : R[X] →+ S :=
    { toFun := eval₂ f x
      map_zero' := eval₂_zero _ _
      map_add' := fun p q => eval₂_add _ _ }
  have A : ∀ y, eval₂ f x y = T y := fun y => rfl
  simp only [A]
  rw [sum, map_sum, sum]

Goal state after:
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
⊢ liftAux R f = (lift R) f

Tactic:
rw [lift]

Goal state after:
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
⊢ liftAux R f = { toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f
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 : FreeAlgebra R X →ₐ[R] A
⊢ (lift R).symm F = ⇑F ∘ ι R

Tactic:
rw [lift]

Goal state after:
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ { toFun := liftAux R, invFun := fun F ↦ ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm F = ⇑F ∘ ι R
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case monomial
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
n : ℕ
b : R
⊢ eval x (C a * (monomial n) b) = a * eval x ((monomial n) b)

Tactic:
simp only [mul_assoc, C_mul_monomial, eval_monomial]

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
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
have pp : Prime n :=
        prime_def_le_sqrt.2
          ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩

Goal state after:
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))
Module: Mathlib.Algebra.MonoidAlgebra.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Mul M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : M →ₙ* A
t' : R
a : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun (t' • a) =
    (MonoidHom.id R) t' •
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f x)).comp coeffAddEquiv.toAddMonoidHom)).toFun a

Tactic:
simp [Finsupp.smul_sum, sum_smul_index', mul_smul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
t' : R
a : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
      (t' • a) =
    (MonoidHom.id R) t' •
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
              coeffAddEquiv.toAddMonoidHom)).toFun
        a

Tactic:
simp [Finsupp.smul_sum, sum_smul_index', mul_smul]

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
f : R[A]
fs : List R[A]
⊢ (f * fs.prod).coeff.support.sup degb ≤ f.coeff.support.sup degb + (List.map (fun f ↦ f.coeff.support.sup degb) fs).sum

Tactic:
sup_support_coeff_mul_le degbm,

Goal state after:
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
f : R[A]
fs : List R[A]
⊢ f.coeff.support.sup degb + fs.prod.coeff.support.sup degb ≤
    f.coeff.support.sup degb + (List.map (fun f ↦ f.coeff.support.sup degb) fs).sum
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
T : Type u_4
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
l : List R[A]
⊢ (List.map (fun f ↦ f.coeff.support.inf degt) l).sum ≤ l.prod.coeff.support.inf degt

Tactic:
by
  refine OrderDual.ofDual_le_ofDual.mpr ?_
  refine sup_support_list_prod_le ?_ ?_ l
  · refine (OrderDual.ofDual_le_ofDual.mp ?_)
    exact degt0
  · refine (fun a b => OrderDual.ofDual_le_ofDual.mp ?_)
    exact degtm a b

Goal state after: