mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
x : R
i✝ j✝ : n
⊢ (v₁.repr ((DistribSMul.toLinearMap R M₁ x) (v₁ j✝))) i✝ = Matrix.diagonal (fun x_1 ↦ x) i✝ j✝

Tactic:
DistribSMul.toLinearMap_apply,

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₁
x : R
i✝ j✝ : n
⊢ (v₁.repr (x • v₁ j✝)) i✝ = Matrix.diagonal (fun x_1 ↦ x) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f : End A (ι → M)
i : ι
x : M
j : ι
⊢ ∑ x_1, f (Pi.single x_1 (Pi.single i x x_1)) j = f (Pi.single i x) j

Tactic:
rw [← Fintype.sum_apply, ← map_sum]

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f : End A (ι → M)
i : ι
x : M
j : ι
⊢ f (∑ x_1, Pi.single x_1 (Pi.single i x x_1)) j = f (Pi.single i x) j
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
i✝ j✝ : ι
x✝ : M
⊢ f (g (Pi.single j✝ x✝)) i✝ = ∑ x, f (Pi.single x (g (Pi.single j✝ x✝) x)) i✝

Tactic:
rw [← Fintype.sum_apply, ← map_sum]

Goal state after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : CommSemiring R
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
f g : End A (ι → M)
i✝ j✝ : ι
x✝ : M
⊢ f (g (Pi.single j✝ x✝)) i✝ = f (∑ x, Pi.single x (g (Pi.single j✝ x✝) x)) i✝
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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = (snf.a i • c.sum fun a b ↦ b • Finsupp.single a 1) i

Tactic:
Finsupp.smul_single,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.bM.repr ↑(snf.bN a)) (snf.f i) = (snf.a i • c.sum fun a b ↦ Finsupp.single a (b • 1)) i
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: ι✝ : Type u_1
inst✝¹⁰ : Fintype ι✝
inst✝⁹ : DecidableEq ι✝
R : Type u_2
inst✝⁸ : CommSemiring R
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
M : Type u_4
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
ι : Type u_5
inst✝¹ : Finite ι
inst✝ : IsStablyFiniteRing A
⊢ IsStablyFiniteRing (End A (ι → A))

Tactic:
have := Fintype.ofFinite ι
  classical rw [← MulOpposite.isStablyFiniteRing_iff,
    ← RingEquiv.isStablyFiniteRing_iff (matrixRingEquivEndVecMulOpposite (ι := ι) (A := A))]
  infer_instance

Goal state after:
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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ b • snf.a a • Finsupp.single (snf.f a) 1) (snf.f i) = snf.a i • c i

Tactic:
Finsupp.smul_single,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝² : CommRing R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ (c.sum fun a b ↦ Finsupp.single (snf.f a) (b • snf.a a • 1)) (snf.f i) = snf.a i • c i
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]

Goal state after:
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 ((algebraMap R S) r • s • x) = r • (addEquiv R S M).symm (s • x)
Module: Mathlib.RingTheory.Localization.Defs

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
inst✝ : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), ↑n * x = ↑n * y ↔ x = y
⊢ (∀ (a a_1 : R), a_1 ∈ M → ∀ (a_2 a_3 : R), a_3 ∈ M → r * (a_3 * a) = r * (a_1 * a_2) → a_3 * a = a_1 * a_2) ↔
    ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂

Tactic:
exact ⟨fun h a b ↦ by simpa using h a 1 M.one_mem b 1 M.one_mem, fun h ha s hs b t ht ↦ @h _ _⟩

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

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x✝ : A
⊢ (algebraMap P Q) (h ((algebraMap A R) x✝)) = (algebraMap A Q) x✝

Tactic:
AlgEquiv.commutes,

Goal state after:
R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x✝ : A
⊢ (algebraMap P Q) ((algebraMap A P) x✝) = (algebraMap A Q) x✝
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
⊢ Injective ⇑f

Tactic:
by
  rw [IsLocalization.injective_iff_map_algebraMap_eq M]
  refine fun x y ↦ ⟨fun hz ↦ hz ▸ rfl, fun hz ↦ ?_⟩
  rw [← sub_eq_zero, ← map_sub, ← map_sub] at hz
  apply h at hz
  rwa [map_sub, sub_eq_zero] at hz

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

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ star p = p * q ↔ p * q = p

Tactic:
hp.isSelfAdjoint,

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ p = p * q ↔ p * q = p
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ˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - b * r⁻¹ • a)
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)

Tactic:
rw [mul_smul_comm r⁻¹ b a] at this

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : Rˣ
h₁ : ∀ (x y : A), IsUnit (1 - x * y) → IsUnit (1 - y * x)
this : IsUnit (1 - r⁻¹ • a * b) ↔ IsUnit (1 - r⁻¹ • (b * a))
⊢ ↑r ∈ σ (a * b) ↔ ↑r ∈ σ (b * a)
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)
⊢ {t | ∃ m n, m ⊗ₜ[R] n = t} ⊆ ↑((mk R S M) 1).range

Tactic:
rintro _ ⟨x, y, rfl⟩

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)
x : S
y : M
⊢ x ⊗ₜ[R] y ∈ ↑((mk R S M) 1).range
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_4
κ : ι → Type u_5
inst✝³ : Nonempty ι
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → NonUnitalRing (κ i)
inst✝ : (i : ι) → Module R (κ i)
a : (i : ι) → κ i
r : R
hr : ¬IsUnit r
⊢ (∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ↔ ∃ i, ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a i))

Tactic:
simp [hr]

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

Goal state before:
pp: case neg
A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : NonUnitalRing B
inst✝¹ : Module R A
inst✝ : Module R B
a : A
b : B
r : R
hr : ¬IsUnit r
⊢ (∃ (h : IsUnit r), IsQuasiregular (-(⋯.unit⁻¹ • (a, b)))) ↔
    ¬((∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))) ∨ ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • b)))

Tactic:
simp [hr]

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective ⇑includeLeft

Tactic:
rw [← Function.Bijective.of_comp_iff _ (TensorProduct.rid R S A).bijective]

Goal state after:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : Semiring B
inst✝ : Algebra R B
h : Function.Bijective ⇑(algebraMap R B)
this : includeLeft.comp ↑(TensorProduct.rid R S A) = map (AlgHom.id S A) (ofId R B)
⊢ Function.Bijective (⇑includeLeft ∘ ⇑(TensorProduct.rid R S A))
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra 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)
T : Subalgebra R A
hT : T ≤ iSup K
compat : ∀ (i j : ι) (x : A) (hxi : x ∈ ↑(K i)) (hxj : x ∈ ↑(K j)), (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩ :=
  iSupLift._proof_2 K dir f hf
⊢ ∀ (x y : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ (x * y) =
      Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ x *
        Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) compat ↑(iSup K) ⋯ y

Tactic:
dsimp
        apply Set.iUnionLift_binary (coe_iSup_of_directed (K := K) dir) dir _ (fun _ => (· * ·))
        all_goals simp

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Directed

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra 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)
T : Subalgebra R A
hT : T ≤ iSup K
i : ι
x : ↥(K i)
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT) ((inclusion h) x) = (f i) x

Tactic:
dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_inclusion]
  exact SetLike.coe_subset_coe.mpr <| h.trans hT

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
ι : Type v
M : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : ∀ (i : ι), Free R (M i)
B : (i : ι) → Basis (ChooseBasisIndex R (M i)) R (M i) := fun i ↦ chooseBasis R (M i)
b : Basis ((i : ι) × ChooseBasisIndex R (M i)) R (⨁ (i : ι), M i) := DFinsupp.basis fun i ↦ B i
⊢ Module.rank R (⨁ (i : ι), M i) = sum fun i ↦ Module.rank R (M i)

Tactic:
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']

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

Goal state before:
pp: case intro
R : Type u
η : Type u₁'
φ : η → Type u_1
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : (i : η) → AddCommMonoid (φ i)
inst✝² : (i : η) → Module R (φ i)
inst✝¹ : ∀ (i : η), Free R (φ i)
inst✝ : Finite η
val✝ : Fintype η
B : (i : η) → Basis (ChooseBasisIndex R (φ i)) R (φ i) := fun i ↦ chooseBasis R (φ i)
b : Basis ((j : η) × ChooseBasisIndex R (φ j)) R ((i : η) → φ i) := Pi.basis fun i ↦ B i
⊢ Module.rank R ((i : η) → φ i) = sum fun i ↦ Module.rank R (φ i)

Tactic:
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_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
s : Set M
⊢ Module.rank R ↥(Finsupp.linearCombination R Subtype.val).range ≤ #↑s

Tactic:
← lift_strictMono.le_iff_le

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{?u.38, v} (Module.rank R ↥(Finsupp.linearCombination R Subtype.val).range) ≤ lift.{?u.38, v} #↑s
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : NonUnitalStarSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
by rw [h]; exact mem_top

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

Goal state before:
pp: R : Type u
A : Type v
B : 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
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
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)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
subst hT
  dsimp [iSupLift]
  apply Set.iUnionLift_of_mem

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H : ∀ (c : R), c • x = 0 → σ c • y = 0
c₁ c₂ : R
h : (c₁ - c₂) • x = 0
⊢ σ (c₁ - c₂) • y = 0

Tactic:
exact H _ h

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
⊢ Classical.choose ⋯ • x = (Classical.choose ⋯ + Classical.choose ⋯) • x

Tactic:
have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
y' z' : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose ⋯ • x = ↑w
⊢ Classical.choose ⋯ • x = (Classical.choose ⋯ + Classical.choose ⋯) • x
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
c : R
z : ↥(R ∙ x)
⊢ Classical.choose ⋯ • x = (c * Classical.choose ⋯) • x

Tactic:
have (w : R ∙ x) := Classical.choose_spec (mem_span_singleton.1 w.prop)

Goal state after:
case a
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
x : E
y : F
H✝ : ∀ (c : R), c • x = 0 → σ c • y = 0
H : ∀ (c₁ c₂ : R), c₁ • x = c₂ • x → σ c₁ • y = σ c₂ • y
c : R
z : ↥(R ∙ x)
this : ∀ (w : ↥(R ∙ x)), Classical.choose ⋯ • x = ↑w
⊢ Classical.choose ⋯ • x = (c * Classical.choose ⋯) • x
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
n : ℕ
⊢ finrank K V < n ↔ Module.rank K V < ↑n

Tactic:
simp [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0 (rank_lt_aleph0 K V), finrank]

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 : ℕ
⊢ eval₂ f x ↑n = ↑n

Tactic:
induction n with
  | zero => simp only [eval₂_zero, Nat.cast_zero]
  | succ n ih => rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]

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

Goal state before:
pp: R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ¬↑2 = 0

Tactic:
CharP.cast_eq_zero_iff R p 2

Goal state after:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : Fact (2 < p)
⊢ ¬p ∣ 2
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
⊢ f = g

Tactic:
apply dExt
  · ext
    exact mem_domain_iff_of_eq_graph h
  · apply (le_of_le_graph h.le).2

Goal state after:
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
⊢ #{m} + 1 = 2

Tactic:
card_singleton

Goal state after:
R : Type u
inst✝ : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ 1 + 1 = 2
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ #{n} + 1 + 1 = 3

Tactic:
card_singleton

Goal state after:
R : Type u
inst✝ : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ 1 + 1 + 1 = 3
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case h₀
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ ∀ b ∈ antidiagonal (d + n), b ≠ (d, n) → p.coeff b.1 * (X ^ n).coeff b.2 = 0

Tactic:
rintro ⟨i, j⟩ h1 h2
    rw [coeff_X_pow, if_neg, mul_zero]
    grind [mem_antidiagonal]

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✝⁵ : CommSemiring R
inst✝⁴ : AddMonoid M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a✝¹ : A[M]
a✝ : M
⊢ ((Additive.toMul (Additive.ofMul (domCongr R A 0))) a✝¹).coeff a✝ = ((Additive.toMul 0) a✝¹).coeff a✝

Tactic:
simp [AddAut.zero_def]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
i : ℕ
r : R
hr : r = 0
⊢ ((monomial i) r).natDegree = 0

Tactic:
simp [hr]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
by_cases h₂ : natDegree q = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : q.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
h₂ : ¬q.natDegree = 0
⊢ p.natDegree = q.natDegree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : r = 0
⊢ (single a r).coeff (Function.invFun D ⊥) = r

Tactic:
simp [hr]

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

Goal state before:
pp: case neg.refine_2
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ∈ s.erase i
⊢ supDegree D (f j) < supDegree D (f i)

Tactic:
· rw [Finset.mem_erase] at hj; exact hmax j hj.2 hj.1

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
⊢ (↑u).coeff 0 ≠ 0

Tactic:
by
  conv in 0 => rw [← natDegree_coe_units u]
  rw [← leadingCoeff, Ne, leadingCoeff_eq_zero]
  exact Units.ne_zero _

Goal state after: