mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype m
v : m → α
M : Matrix m n α
N : Matrix n o α
x✝ : o
⊢ (v ᵥ* M ᵥ* N) x✝ = (v ᵥ* (M * N)) x✝

Tactic:
apply dotProduct_assoc

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
x✝ : m
⊢ ((M * N) *ᵥ v) x✝ = (M *ᵥ N *ᵥ v) x✝

Tactic:
apply dotProduct_assoc

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
⊢ M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), Commute (single i j 1) M

Tactic:
refine ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
    fun hM => mem_range_scalar_iff_commute_single.mpr <| fun i j _ => hM i j⟩
  rw [scalar_commute_iff]
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset

Tactic:
· rw [h, zero_add, one_nsmul]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ ((n + 1) • s).toFinset = s.toFinset
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Algebra R α
r : R
⊢ (transposeRingEquiv m α).toFun ((algebraMap R (Matrix m m α)) r) = (algebraMap R (Matrix m m α)ᵐᵒᵖ) r

Tactic:
simp [algebraMap_eq_diagonal]

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

Goal state before:
pp: case neg
R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : ¬Module.Finite S M
⊢ finrank S M ≤ finrank R M

Tactic:
rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]

Goal state after:
case neg
R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : ¬Module.Finite S M
⊢ 0 ≤ finrank R M

R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
H : ¬Module.Finite S M
⊢ ℵ₀ ≤ Module.rank S M
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: case neg
R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ finrank R S ≤ finrank R T

Tactic:
rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]

Goal state after:
case neg
R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ 0 ≤ finrank R T

R : Type u
inst✝¹¹ : Semiring R
inst✝¹⁰ : StrongRankCondition R
S : Type u_2
T : Type u_3
inst✝⁹ : Semiring S
inst✝⁸ : Semiring T
inst✝⁷ : Module R T
inst✝⁶ : Module S T
inst✝⁵ : Module R S
inst✝⁴ : IsScalarTower R S T
inst✝³ : IsScalarTower S T T
inst✝² : FaithfulSMul S T
inst✝¹ : Module.Finite S T
inst✝ : Free R S
H : ¬Module.Finite R S
⊢ ℵ₀ ≤ Module.rank R S
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
⊢ ∃! c, u = c • LinearMap.id

Tactic:
use c
    simp only [this, true_and]
    intro d hcd
    rw [LinearMap.ext_iff] at hcd
    simpa using (LinearEquiv.congr_arg (e := e.symm) (hcd (e 1))).symm

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ (component R ι M x✝) f = (component R ι M x✝) g

Tactic:
rw [h]

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

Goal state before:
pp: case Hsmul_l
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → r • x * y ∈ span R ↑(Subsemigroup.closure s)

pp: case Hsmul_r
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → x * r • y ∈ span R ↑(Subsemigroup.closure s)

Tactic:
case Hsmul_l => exact fun r x y _ _ hxy ↦ by simpa [smul_mul_assoc] using smul_mem _ _ hxy

Goal state after:
case Hsmul_r
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝ x y : A
hx✝ : x ∈ adjoin R s
hy✝ : y ∈ adjoin R s
hpx : x ∈ span R ↑(Subsemigroup.closure s)
hpy : y ∈ span R ↑(Subsemigroup.closure s)
⊢ ∀ (r : R) (x y : A),
    x ∈ span R ↑(Subsemigroup.closure s) →
      y ∈ span R ↑(Subsemigroup.closure s) →
        x * y ∈ span R ↑(Subsemigroup.closure s) → x * r • y ∈ span R ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ M
n : N
i : ι
⊢ ((finsuppLeft R S M N ι) (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n

Tactic:
by
  rw [finsuppLeft_apply_tmul, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsRightRegular x ∧ IsLeftRegular x ↔ IsLeftRegular x ∧ IsRightRegular x

Tactic:
and_comm

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsLeftRegular x ∧ IsRightRegular x ↔ IsLeftRegular x ∧ IsRightRegular x
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M i✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1

Tactic:
rw [h]

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

Goal state before:
pp: case e_c
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (k = k' ∧ i = j) = (i = j ∧ k = k')

Tactic:
and_comm

Goal state after:
case e_c
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : DecidableEq m
d : o → m → α
i : m
k : o
j : m
k' : o
⊢ (i = j ∧ k = k') = (i = j ∧ k = k')
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}

Tactic:
simp_rw [le_antisymm_iff, I.span_singleton_le_iff_mem.2 hx, and_true, ← Ideal.mem_span_singleton]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ generator I ∈ Ideal.span {x} ↔ I ≤ Ideal.span {x}
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
⊢ Basis (Fin (m' + 1)) R ↥M

Tactic:
refine Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ?_

Goal state after:
case neg.intro.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
⊢ ∀ z ∈ M, ∃ c, z + c • y' ∈ M'
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
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₂
f : M₁ →ₗ[R] M₂
x : M₁
⊢ (toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x) = ⇑(v₂.repr (f x))

Tactic:
ext i
  rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
    LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]
  congr
  exact v₁.equivFun.symm_apply_apply x

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
⊢ n • x = n • x

Tactic:
let inst := OreLocalization.instModuleOfIsScalarTower (R₀ := ℤ) (R := R) (X := X) (S := S)

Goal state after:
R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
inst : Module ℤ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x
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))

pp: case neg
ι : 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:
case neg
ι : 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))
Module: Mathlib.Algebra.Star.TensorProduct

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
⊢ (congr ((starLinearEquiv R).trans (starLinearEquiv R)) ((starLinearEquiv R).trans (starLinearEquiv R))) x = x

Tactic:
convert! congr($congr_refl_refl x) <;> ext

Goal state after:
case e'_2.e'_21
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
x✝ : A
⊢ ((starLinearEquiv R).trans (starLinearEquiv R)) x✝ = (LinearEquiv.refl R A) x✝

case e'_2.e'_22
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : StarAddMonoid A
inst✝⁵ : Module R A
inst✝⁴ : StarModule R A
inst✝³ : AddCommMonoid B
inst✝² : StarAddMonoid B
inst✝¹ : Module R B
inst✝ : StarModule R B
x : A ⊗[R] B
x✝ : B
⊢ ((starLinearEquiv R).trans (starLinearEquiv R)) x✝ = (LinearEquiv.refl R B) 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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy) (z • x) = g z • (map Q g hy) x

Tactic:
rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_eq]

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

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s : NonUnitalSubalgebra R A
⊢ span R ({1} ∪ ↑(Subsemigroup.closure ↑s)) = R ∙ 1 ⊔ s.toSubmodule

Tactic:
span_union,

Goal state after:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s : NonUnitalSubalgebra R A
⊢ R ∙ 1 ⊔ span R ↑(Subsemigroup.closure ↑s) = R ∙ 1 ⊔ s.toSubmodule
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
r : A
s : ↥A⁰
⊢ IsLocalization.mk' (Localization A⁰) r s = (algebraMap A (FractionRing A)) r / (algebraMap A (FractionRing A)) ↑s

Tactic:
IsFractionRing.mk'_eq_div

Goal state after:
A : Type u_4
inst✝¹ : CommRing A
inst✝ : IsDomain A
r : A
s : ↥A⁰
⊢ (algebraMap A (Localization A⁰)) r / (algebraMap A (Localization A⁰)) ↑s =
    (algebraMap A (FractionRing A)) r / (algebraMap A (FractionRing A)) ↑s
Module: Mathlib.RingTheory.Localization.FractionRing

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
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
K✝ : Type u_5
inst✝⁸ : IsDomain A
k : Type u_6
K : Type u_7
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A k
inst✝⁴ : Algebra A K
inst✝³ : Algebra k K
inst✝² : FaithfulSMul A k
inst✝¹ : FaithfulSMul A K
inst✝ : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x✝ : A × ↥A⁰
a₁ : A
a₂ : ↥A⁰
⊢ ((↑a₂ • Localization.mk a₁ a₂) • b) • c = (↑a₂ • Localization.mk a₁ a₂) • b • c

Tactic:
Localization.smul_mk,

Goal state after:
R : Type u_1
inst✝¹³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Type u_3
inst✝¹⁰ : CommRing P
A : Type u_4
inst✝⁹ : CommRing A
K✝ : Type u_5
inst✝⁸ : IsDomain A
k : Type u_6
K : Type u_7
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A k
inst✝⁴ : Algebra A K
inst✝³ : Algebra k K
inst✝² : FaithfulSMul A k
inst✝¹ : FaithfulSMul A K
inst✝ : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x✝ : A × ↥A⁰
a₁ : A
a₂ : ↥A⁰
⊢ (Localization.mk (↑a₂ • a₁) a₂ • b) • c = Localization.mk (↑a₂ • a₁) a₂ • b • c
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : s.Finite
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(rTensor M J.subtype).range

Tactic:
choose J fg y eq using exists_fg_le_eq_rTensor_subtype (R := R) (M := M) (N := N)

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (N ⊗[R] M)
hs : s.Finite
J : N ⊗[R] M → Submodule R N
fg : ∀ (x : N ⊗[R] M), (J x).FG
y : (x : N ⊗[R] M) → ↥(J x) ⊗[R] M
eq : ∀ (x : N ⊗[R] M), x = (rTensor M (J x).subtype) (y x)
⊢ ∃ J, ∃ (_ : J.FG), s ⊆ ↑(rTensor M J.subtype).range
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 : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
x y : A ⊗[R] A
hxy : (lift (LinearMap.mul R A)) x = (lift (LinearMap.mul R A)) y
u v : A
⊢ u ⊗ₜ[R] 1 * 1 ⊗ₜ[R] v = u ⊗ₜ[R] 1 * v ⊗ₜ[R] 1

Tactic:
rw [h]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ star '' s = star ⁻¹' s

Tactic:
rw [image_eq_preimage_of_inverse]

Goal state after:
case h₁
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ Function.LeftInverse star star

case h₂
α : Type u_1
s : Set α
inst✝ : InvolutiveStar α
⊢ Function.RightInverse star star
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case a.tmul
R : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
l : M →ₗ[R] N
x✝ : A
y✝ : M
⊢ x✝ • l y✝ ∈ Submodule.span A ↑l.range

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, rfl⟩)

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
r : Rˣ
s : R
a : A
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
smul_inv_smul,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : Rˣ
x : R
x_eq : x = r • r⁻¹ • x
⊢ r⁻¹ • x ∈ σ a → x ∈ r • σ a

Tactic:
exact fun h => ⟨r⁻¹ • x, ⟨h, show r • r⁻¹ • x = x by simp⟩⟩

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
a b : A
r : Rˣ
x y : A
h : IsUnit (1 - x * y)
⊢ 1 - y * x + y * ((1 - x * y) * h.unit.inv) * x = 1

Tactic:
by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalCommSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x✝¹ x✝ : Unitization R A
⊢ (x✝¹ * x✝).toProd.2 = (x✝ * x✝¹).toProd.2

Tactic:
by simp [add_comm, mul_comm]

Goal state after: