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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ f ∘ₗ g₁.coprod g₂ = LinearMap.id

Tactic:
LinearMap.comp_coprod,

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ (f ∘ₗ g₁).coprod (f ∘ₗ g₂) = LinearMap.id
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = LinearMap.id

Tactic:
classical
      choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
      replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ DFunLike.congr_fun (hg i)
      refine ⟨DFinsupp.coprodMap g, ?_⟩
      ext i x j
      simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]

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

Goal state before:
pp: R✝ : Type u
R : Type u_1
inst✝² : MulOneClass R
inst✝¹ : StarMul R
r : R
inst✝ : Invertible r
⊢ star ⅟r * star r = 1

Tactic:
rw [← star_mul, mul_invOf_self, star_one]

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

Goal state before:
pp: R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)

Tactic:
unfold mkFinCons

Goal state after:
R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(have span_b := ⋯;
      Basis.mk ⋯ ⋯) =
    Fin.cons y (Subtype.val ∘ ⇑b)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
⊢ (M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)

Tactic:
ext
  rw [updateRow_apply, map_apply, map_apply, updateRow_apply]
  exact apply_ite f _ _ _

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (blockDiagonal' M)ᵀ ⟨ii, ix⟩ ⟨ji, jx⟩ = blockDiagonal' (fun k ↦ (M k)ᵀ) ⟨ii, ix⟩ ⟨ji, jx⟩

Tactic:
simp only [transpose_apply, blockDiagonal'_apply]

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (if h : ji = ii then M ji jx (cast ⋯ ix) else 0) = if h : ii = ji then M ii (cast ⋯ jx) ix else 0
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
r : R
b : B
⊢ e.symm.toFun (r • b) = r • e.symm.toFun b

Tactic:
by
      simpa only [apply_inv_apply, inv_apply_apply] using!
        congr_arg (inv e) (map_smul e r (inv e b)).symm

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ span A ↑(map ((TensorProduct.mk R A M) 1) p) ≤ baseChange A p

Tactic:
refine span_le.2 fun _ ⟨m, hm, h⟩ ↦ h ▸ ⟨1 ⊗ₜ[R] ⟨m, hm⟩, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ ⇑M.vecMulLinear = ⇑(Fintype.linearCombination R M.row)

Tactic:
exact funext fun _ => Matrix.vecMul_eq_sum _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ Mᵀ.vecMulLinear = M.mulVecLin

Tactic:
ext; simp [vecMul_transpose]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ toMatrix' id i✝ j✝ = if i✝ = j✝ then 1 else 0

Tactic:
LinearMap.toMatrix'_apply,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ id (Pi.single j✝ 1) i✝ = if i✝ = j✝ then 1 else 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝⁴ : Fintype m
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
⊢ (toMatrix v₁ v₃) ((toLin v₁ v₃) (A * B)) = (toMatrix v₁ v₃) ((toLin v₂ v₃) A ∘ₗ (toLin v₁ v₂) B)

Tactic:
have : DecidableEq l := fun _ _ ↦ Classical.propDecidable _

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝⁴ : Fintype m
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
this : DecidableEq l
⊢ (toMatrix v₁ v₃) ((toLin v₁ v₃) (A * B)) = (toMatrix v₁ v₃) ((toLin v₂ v₃) A ∘ₗ (toLin v₁ v₂) B)
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: 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
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * (rb * ↑s₁) + ↑sc * (↑sb * (ra * r₃))) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
← mul_assoc _ ra,

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
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * (↑sa * r₂) = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra * r₃) = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((↑sc * (rb * ↑s₁) + ↑sc * (↑sb * ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsPrincipalIdealRing R
inst✝¹ : IsDomain R
ι : Type u_4
inst✝ : Finite ι
b : Basis ι R M
n : ℕ
b' : Basis (Fin n) R ↥⊥
e : Fin n ≃ Fin 0 := b'.indexEquiv (Basis.empty ↥⊥)
⊢ n = 0

Tactic:
simpa using Fintype.card_eq.mpr ⟨e⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ (addEquiv R S M).symm ((r • s) • x) = r • (addEquiv R S M).symm (s • x)

Tactic:
rw [Algebra.smul_def, mul_smul]
  rfl

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

Goal state before:
pp: case exists_of_eq
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
inst✝ : IsLocalization M S
h : R ≃+* P
this : Algebra P S := ⋯
⊢ ∀ {x y : P}, (algebraMap P S) x = (algebraMap P S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
· intro x y
    rw [RingHom.algebraMap_toAlgebra, RingHom.comp_apply, RingHom.comp_apply,
      IsLocalization.eq_iff_exists M S]
    simp [← h.toEquiv.apply_eq_iff_eq]

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

Goal state before:
pp: case e_x
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
inst✝ : Subsingleton R
a : Localization M
x✝ : R × ↥M
⊢ x✝.1 = 1

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: case e_y
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
inst✝ : Subsingleton R
a : Localization M
x✝ : R × ↥M
⊢ x✝.2 = 1

Tactic:
apply Subsingleton.elim

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ IsLocalization R⁰ S ↔ IsLocalization P⁰ S

Tactic:
convert! isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h

Goal state after:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ P⁰ = Submonoid.map h R⁰
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ Surjective ⇑(LinearMap.toSpanSingleton R (M ⧸ N) x)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : ⊤ = R ∙ x
⊢ (LinearMap.toSpanSingleton R (M ⧸ N) x).range = ⊤
Module: Mathlib.Algebra.Algebra.Epi

Goal state before:
pp: case tmul
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 s : A
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
this : R'.mkQ 1 = 0
⊢ R'.mkQ x ⊗ₜ[R] R'.mkQ y = 0

Tactic:
← map_tmul R'.mkQ R'.mkQ,

Goal state after:
case tmul
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 s : A
hs : 1 ⊗ₜ[R] s = x ⊗ₜ[R] y
this : R'.mkQ 1 = 0
⊢ (map R'.mkQ R'.mkQ) (x ⊗ₜ[R] y) = 0
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✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Semiring C
inst✝³ : Algebra R C
inst✝² : CommSemiring S
inst✝¹ : Algebra S A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • 1 ⊗ₜ[R] 1 * x = x * r • 1 ⊗ₜ[R] 1

Tactic:
← one_def,

Goal state after:
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✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Semiring C
inst✝³ : Algebra R C
inst✝² : CommSemiring S
inst✝¹ : Algebra S A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • 1 * x = x * r • 1
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✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Semiring C
inst✝³ : Algebra R C
inst✝² : CommSemiring S
inst✝¹ : Algebra S A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • x = r • (1 ⊗ₜ[R] 1 * x)

Tactic:
← one_def,

Goal state after:
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✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Semiring C
inst✝³ : Algebra R C
inst✝² : CommSemiring S
inst✝¹ : Algebra S A
inst✝ : SMulCommClass R S A
r : S
x : A ⊗[R] B
⊢ r • x = r • (1 * x)
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 : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ ↑a * (r • ↑a⁻¹ - 1) = r • 1 - ↑a

Tactic:
rw [mul_sub, mul_smul_comm, a.mul_inv, mul_one]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Function.Surjective ⇑((mk R S M) 1)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ ((mk R S M) 1).range = ⊤
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ Function.Surjective ⇑((mk R S T).flip 1)

Tactic:
← LinearMap.range_eq_top,

Goal state after:
R : Type u_1
S : Type u_3
T : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Ring T
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
⊢ ((mk R S T).flip 1).range = ⊤
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) = quasispectrum R (b * a)

Tactic:
rw [← Set.inter_union_compl (quasispectrum R (a * b)) {r | IsUnit r},
    ← Set.inter_union_compl (quasispectrum R (b * a)) {r | IsUnit r}]

Goal state after:
R : Type u_3
A : Type u_4
inst✝⁴ : CommRing R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a b : A
⊢ quasispectrum R (a * b) ∩ {r | IsUnit r} ∪ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ =
    quasispectrum R (b * a) ∩ {r | IsUnit r} ∪ quasispectrum R (b * a) ∩ {r | IsUnit r}ᶜ
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: case refine_1
R : Type u
M : Type v
ι : Type w
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hst : Disjoint s t
h : LinearIndepOn R f (s ∪ t)
⊢ LinearIndepOn R f s

Tactic:
exact h.mono subset_union_left

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
s : Set M
⊢ Module.rank R ↥(span R s) ≤ #↑s

Tactic:
by
  rw [Finsupp.span_eq_range_linearCombination, ← lift_strictMono.le_iff_le]
  refine (lift_rank_range_le _).trans ?_
  rw [rank_finsupp_self]
  simp only [lift_lift, le_refl]

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

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
⊢ lift.{v, w} #{ i // V i ≠ ⊥ } ≤ lift.{w, v} (Module.rank R M)

Tactic:
set I := { i : ι // V i ≠ ⊥ }

Goal state after:
ι : Type w
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i // V i ≠ ⊥ }
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case neg
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
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
i : ↑n := ⟨v, ⋯⟩
hi : b i = v
j : ↑n
h : ¬i = j
⊢ f (b j) = (f (b i) • b.coord i) (b j)

Tactic:
· suffices f (b j) = 0 by
      simp [Finsupp.single_eq_of_ne h, this]
    rw [← mem_ker, ← hs, Basis.coe_mk]
    apply subset_span
    apply Or.resolve_left (Set.mem_insert_iff.mpr j.prop)
    simp [← hi, b, Subtype.coe_inj, Ne.symm h]

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

Goal state before:
pp: case mp.inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
⊢ ∃ v₀, ∀ (v : V), ∃ r, r • v₀ = v

Tactic:
use 0
      have h' : ∀ v : V, v = 0 := by
        simpa [range_eq_empty, Submodule.eq_bot_iff] using b.span_eq.symm
      intro v
      simp [h' v]

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

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))

pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)

Tactic:
· rw [add_comm, pow_add]
      apply LinearMap.ker_le_ker_comp

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = p.sum fun e a ↦ f a * x ^ e

Tactic:
eval₂_def

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ (p.sum fun e a ↦ f a * x ^ e) = p.sum fun e a ↦ f a * x ^ e
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
hp✝ : 2 ≤ p
m : ℕ
h : m < p
n : ℕ
hp : p = m * n
hpn : p ≤ n
this : m ≠ 0 ∧ n ≠ 0
⊢ m = 1

Tactic:
exact (Nat.mul_eq_right (by lia)).mp
    (hp.symm.trans (hpn.antisymm (hp ▸ Nat.le_mul_of_pos_left _ (by lia))))

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

Goal state before:
pp: case mp
n : ℕ
⊢ n.minFac = 1 → n = 1

pp: case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1

Tactic:
· intro h
    by_contra hn
    have := minFac_prime hn
    rw [h] at this
    exact not_prime_one this

Goal state after:
case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m).support = 2

Tactic:
by
  rw [support_binomial h hx hy, card_insert_of_notMem (mt mem_singleton.mp h), card_singleton]

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

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
q : S[X]
h : p.degree = q.degree
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 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
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
⊢ p.natDegree = q.natDegree

Tactic:
unfold natDegree

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
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: n : ℕ
⊢ 0 ≤ ↑n

Tactic:
← WithBot.coe_zero,

Goal state after:
n : ℕ
⊢ ↑0 ≤ ↑n
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: case coe
a✝ : ℕ
h : 0 < ↑a✝
⊢ 1 ≤ ↑a✝

Tactic:
← WithBot.coe_zero,

Goal state after:
case coe
a✝ : ℕ
h : ↑0 < ↑a✝
⊢ 1 ≤ ↑a✝
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ supDegree D p + supDegree D q ∈ Set.range D

Tactic:
rw [← AddSubsemigroup.coe_set_mk (Set.range D), ← AddHom.srange_mk _ hadd, SetLike.mem_coe]
    · exact add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)
    · exact (AddHom.srange ⟨D, hadd⟩).add_mem

Goal state after:
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
hf : Function.Injective ⇑f
⊢ ∀ (a : ℕ), f (p.coeff a) ≠ 0 ↔ p.coeff a ≠ 0

Tactic:
← map_zero f,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective ⇑f
⊢ ∀ (a : ℕ), f (p.coeff a) ≠ f 0 ↔ p.coeff a ≠ 0