mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ Commute ((scalar n) r) (single i j 1)

Tactic:
scalar_commute_iff

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
x✝ : M ∈ Set.range ⇑(scalar n)
i j : n
r : α
hr : (scalar n) r = M
⊢ r • single i j 1 = MulOpposite.op r • single i j 1
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : ¬Module.Finite R M
⊢ toNat (Module.rank R M) = 0

Tactic:
toNat_eq_zero,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ℵ₀ ≤ Module.rank R M
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : IsSimpleRing R
⊢ Nontrivial R

Tactic:
by
  obtain ⟨x, _, hx⟩ := SetLike.exists_of_lt (bot_lt_top : (⊥ : TwoSidedIdeal R) < ⊤)
  use x, 0, hx

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * (m * a) + m * n * b ∈ s

Tactic:
mul_assoc

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
n : S
hn : n ∈ M
hb : n * b ∈ s
⊢ n * (m * a) + m * (n * b) ∈ s
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p s : Submodule R A
h1 : 1 ∈ s
hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s
r : R
⊢ r • 1 ∈ { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯ }.carrier

Tactic:
apply s.smul_mem _ h1

Goal state after:
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
⊢ S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

Tactic:
by simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
List.forall_mem_cons

Goal state after:
case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : (∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s) ∧ ∀ x ∈ tl, ∀ y ∈ x, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : ∀ y ∈ hd :: tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = (hd :: tl).prod

Tactic:
List.forall_mem_cons

Goal state after:
case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = (hd :: tl).prod
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
hb : b ∈ adjoin R s
h : ∀ b ∈ s, Commute a b
⊢ Commute a b

Tactic:
by
  induction hb using adjoin_induction with
  | mem x hx => exact h x hx
  | algebraMap r => exact commutes r a |>.symm
  | add y z _ _ hy hz => exact hy.add_right hz
  | mul y z _ _ hy hz => exact hy.mul_right hz

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ M.map star = 0 ↔ M = 0

Tactic:
simp [← ext_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ ↑((selfAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)

Tactic:
by simp [hx]

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

Goal state before:
pp: n : ℕ
m' : Type uₘ
α : Type u_1
inst✝ : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
⊢ of A *ᵥ vecCons x v = x • vecHead ∘ A + of (vecTail ∘ A) *ᵥ v

Tactic:
by
  ext i
  simp [mulVec, mul_comm]

Goal state after:
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
D : Type u_6
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Star A
inst✝⁸ : Semiring B
inst✝⁷ : Algebra R B
inst✝⁶ : Star B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Star C
inst✝² : Semiring D
inst✝¹ : Algebra R D
inst✝ : Star D
f : B →⋆ₐ[R] C
g : A →⋆ₐ[R] B
⊢ ∀ (x : A), (↑↑((↑f).comp ↑g).toRingHom).toFun (star x) = star ((↑↑((↑f).comp ↑g).toRingHom).toFun x)

Tactic:
simp only [map_star, AlgHom.toFun_eq_coe, AlgHom.coe_comp, coe_toAlgHom,
        Function.comp_apply, forall_const]

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

Goal state before:
pp: case pred
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
n : ℕ
h : LinearEquiv.baseChange R A M M (f ^ (-↑n)) = LinearEquiv.baseChange R A M M f ^ (-↑n)
⊢ LinearEquiv.baseChange R A M M (f ^ (-↑n - 1)) = LinearEquiv.baseChange R A M M f ^ (-↑n - 1)

Tactic:
| pred n h =>

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

Goal state before:
pp: case h.left
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ (↑sd * (rc * ↑sa)) • r₁ + (↑sd * (rc * ra)) • r₂ = (↑sd * (rc * ↑sa)) • r₁ + (↑sd * rc * ra) • r₂

Tactic:
mul_assoc

Goal state after:
case h.left
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ (↑sd * (rc * ↑sa)) • r₁ + (↑sd * (rc * ra)) • r₂ = (↑sd * (rc * ↑sa)) • r₁ + (↑sd * (rc * ra)) • r₂
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case h.right
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * (rc * (↑sa * ↑s₁)) = ↑sd * rc * (↑sa * ↑s₁)

Tactic:
mul_assoc

Goal state after:
case h.right
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * sb = rc * ↑sa
this : ↑sc * rb * ↑s₂ = rc * ra * ↑s₂
sd : ↥S
hd : ↑sd * (↑sc * rb) = ↑sd * (rc * ra)
⊢ ↑sd * (rc * (↑sa * ↑s₁)) = ↑sd * (rc * (↑sa * ↑s₁))
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
this : ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂
⊢ rd * rc * ↑s₂ = rd * (rc * ↑s₂)

Tactic:
mul_assoc

Goal state after:
case h
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
this : ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂
⊢ rd * (rc * ↑s₂) = rd * (rc * ↑s₂)
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ ↑sd * (↑sc * ↑s₃) = ↑sd * ↑sc * ↑s₃

Tactic:
mul_assoc

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • r₂ = rb • r₁
hb' : ↑sb * ↑s₂ = rb * ↑s₁
r₃ : X
s₃ : ↥S
rc : R
sc : ↥S
hc : ↑sc * ↑s₃ = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rc = rd * ↑sb
⊢ ↑sd * (↑sc * ↑s₃) = ↑sd * (↑sc * ↑s₃)
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₂
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₂
k : m
i : n
⊢ (toMatrix v₁.reindexRange v₂.reindexRange) f ⟨v₂ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrix v₁ v₂) f k i

Tactic:
by
  simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ f.mk' (f.sec a).1 (f.sec a).2 = f.mk' (f.sec b).1 (f.sec b).2

Tactic:
f.eq

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ ∃ c, ↑c * (↑(f.sec b).2 * (f.sec a).1) = ↑c * (↑(f.sec a).2 * (f.sec b).1)
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✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : M₁
⊢ ((toLin v₂ v₁) M') (((toLin v₁ v₂) M) x) = x

Tactic:
by rw [← Matrix.toLin_mul_apply, hM'M, Matrix.toLin_one, id_apply]

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

Goal state before:
pp: case neg.intro.refine_2.refine_2.refine_2
ι : 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'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i✝ : Fin (n' + 1)
i : Fin n'
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i.succ) =
    Fin.cons a as i.succ • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ i.succ))

Tactic:
rw [Fin.castLE_succ]

Goal state after:
case neg.intro.refine_2.refine_2.refine_2
ι : 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'
as : Fin n' → R
h : ∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))
i✝ : Fin (n' + 1)
i : Fin n'
⊢ ↑(Fin.cons ⟨y, yN⟩ (⇑(inclusion N'_le_N) ∘ ⇑bN') i.succ) =
    Fin.cons a as i.succ • ↑(Fin.cons ⟨y', y'M⟩ (⇑(inclusion M'_le_M) ∘ ⇑bM') (Fin.castLE ⋯ i).succ)
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✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
obtain
      ⟨indepI : LinearIndependent R (s ∘ (fun x => x) : I → M), hI :
        ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)⟩ :=
      this.choose_spec

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
⊢ (n : ℕ) × Basis (Fin n) R M
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'

Goal state after:
ι : 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
n : ℕ
b : Basis (Fin n) R M
⊢ Free R M
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: A : Type u_3
inst✝ : Semiring A
⊢ IsStablyFiniteRing A ↔ ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f

Tactic:
simp_rw [isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd, isDedekindFiniteMonoid_iff]

Goal state after:
A : Type u_3
inst✝ : Semiring A
⊢ (∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1) ↔
    ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
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
x y : ↥M
⊢ mk' S (↑x) y * mk' S (↑y) x = 1

Tactic:
by
  rw [← mk'_mul, mul_comm]; exact mk'_self _ _

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
⊢ K⁰ = IsUnit.submonoid K

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (isUnit_le_nonZeroDivisors K)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : K
hx : x ∈ K⁰
⊢ x ∈ IsUnit.submonoid K
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x * mk' K ↑(sec A⁰ x).2 ⟨(sec A⁰ x).1, ⋯⟩ * (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩ = (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩

Tactic:
mul_assoc

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : CommRing K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
x : K
hx : x ≠ 0
⊢ x * (mk' K ↑(sec A⁰ x).2 ⟨(sec A⁰ x).1, ⋯⟩ * (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩) =
    (algebraMap A K) ↑⟨(sec A⁰ x).1, ⋯⟩
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✝ : Subsingleton R
a : Localization M
⊢ a = default

Tactic:
change a = mk 1 1

Goal state after:
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
⊢ a = mk 1 1
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddGroupWithOne β
n : ℕ
⊢ e.invFun ↑↑n = ↑n

Tactic:
simp only [Int.cast_natCast]

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : AddGroupWithOne β
n : ℕ
⊢ e.invFun ↑n = ↑n
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
⊢ a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)

Tactic:
by
  induction k with
  | zero => simp [one_def]
  | succ k ih => simp [pow_succ, ih]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
x✝ : PreQuasiregular R
⊢ equiv.symm (1 * x✝) = equiv.symm x✝

Tactic:
by simp [-EmbeddingLike.apply_eq_iff_eq]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
x✝ : PreQuasiregular R
⊢ equiv.symm (x✝ * 1) = equiv.symm x✝

Tactic:
by simp [-EmbeddingLike.apply_eq_iff_eq]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + y) * (1 + x) = 1

Tactic:
· convert congr(1 + $(hy₂)) <;> [noncomm_ring; simp]

Goal state after:
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) ∩ {r | IsUnit r} ∪ quasispectrum R (a * b) ∩ {r | IsUnit r}ᶜ = quasispectrum R (b * a)

Tactic:
← 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.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case e'_3.mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
⊢ (∃ x_1, (Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val) x_1 = x) →
    ∃ x_1, (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) x_1 = (Algebra.TensorProduct.comm R A B) x

Tactic:
rintro ⟨x, rfl⟩
      exact ⟨(Algebra.TensorProduct.comm R _ _) x,
        by rw [Algebra.TensorProduct.comm_comp_map_apply]⟩

Goal state after: