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

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ Submodule.map p.subtype (Submodule.comap p.subtype (A ↑i)) ↔ m ∈ ↑⟨A ↑i, ⋯⟩

Tactic:
Submodule.map_comap_subtype,

Goal state after:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ p ⊓ A ↑i ↔ m ∈ ↑⟨A ↑i, ⋯⟩
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
S : Subalgebra R A
⊢ S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S

Tactic:
cases S

Goal state after:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.toNonUnitalSubalgebra.toSubalgebra ⋯ =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
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
S : NonUnitalSubalgebra R A
h1 : 1 ∈ S
⊢ (S.toSubalgebra h1).toNonUnitalSubalgebra = S

Tactic:
cases S

Goal state after:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case a
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
⊢ span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule

Tactic:
apply span_le.2 _
    change Subsemigroup.closure s ≤ (adjoin R s).toSubsemigroup
    exact Subsemigroup.closure_le.2 (subset_adjoin R)

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 : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)

Tactic:
clear ih tl

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
HL : ∀ y ∈ hd, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ hd.prod ∈ span R ↑(Submonoid.closure s)
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
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ ((finsuppScalarRight R S M ι) (m ⊗ₜ[R] p)) i = p i • m

Tactic:
by
  simp [finsuppScalarRight]

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

Goal state before:
pp: case s
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ M ⊗[R₀] (N →₀ R₀) →ₗ[R] M ⊗[R₀] N

pp: case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ ?s ∘ₗ AlgebraTensorModule.map LinearMap.id sN = LinearMap.id

Tactic:
· exact (AlgebraTensorModule.map (LinearMap.id (R := R) (M := M)) (linearCombination R₀ id))

Goal state after:
case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
this : Projective R (M ⊗[R₀] (N →₀ R₀))
⊢ AlgebraTensorModule.map LinearMap.id (linearCombination R₀ id) ∘ₗ AlgebraTensorModule.map LinearMap.id sN =
    LinearMap.id
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
inst✝ : TrivialStar R
x : R
⊢ Commute (star x) x

Tactic:
star_trivial

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
inst✝ : TrivialStar R
x : R
⊢ Commute x x
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x, ∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0

Tactic:
Fintype.sum_eq_single k

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ (if h : k = k' then ∑ j_1, M k i j_1 * N k j_1 (cast ⋯ j) else 0) =
    ∑ x, (if h : k = k then M k i (cast ⋯ x) else 0) * if h : k = k' then N k x (cast ⋯ j) else 0

o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
⊢ ∀ (x : o),
    x ≠ k → (∑ x_1, (if h : k = x then M k i (cast ⋯ x_1) else 0) * if h : x = k' then N x x_1 (cast ⋯ j) else 0) = 0
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
hr' : r = (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
⊢ {r} ⊆ ↑(closure (↑S \ {r}))

Tactic:
hr',

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr✝ : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
hr' : r = (∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
⊢ {(∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s} ⊆
    ↑(closure (↑S \ {(∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s}))
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * (0 /ₒ 1) = 0 /ₒ 1

Tactic:
mul_div_one,

Goal state after:
case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r * 0 /ₒ s = 0 /ₒ 1
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f g : (m → R) →ₗ[R] n → R
i : m
j : n
⊢ (f + g) ((single R (fun x ↦ R) i) 1) j =
    ((fun i j ↦ f ((single R (fun x ↦ R) i) 1) j) + fun i j ↦ g ((single R (fun x ↦ R) i) 1) j) i j

Tactic:
simp only [Pi.add_apply, LinearMap.add_apply, Matrix.add_apply]

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

Goal state before:
pp: case c.c.c
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ r₁ /ₒ s₁ + (ra • r₂ /ₒ (sa * s₁) + rc • r₃ /ₒ (sc * (sa * s₁))) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)

Tactic:
congr 2

Goal state after:
case c.c.c.e_a.e_a
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ ra • r₂ /ₒ (sa * s₁) = r₂ /ₒ s₂

case c.c.c.e_a.e_a
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ rc • r₃ /ₒ (sc * (sa * s₁)) = r₃ /ₒ 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
x y z : OreLocalization S X
⊢ x + y + z = x + (y + z)

Tactic:
by
  induction x with | _ r₁ s₁
  induction y with | _ r₂ s₂
  induction z with | _ r₃ s₃
  rcases oreDivAddChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
  rcases oreDivAddChar' (sa • r₁ + ra • r₂) r₃ (sa * s₁) s₃ with ⟨rc, sc, hc, q⟩; rw [q]; clear q
  simp only [smul_add, add_assoc]
  simp_rw [← add_oreDiv, ← OreLocalization.expand']
  congr 2
  · rw [OreLocalization.expand r₂ s₂ ra (ha.symm ▸ (sa * s₁).2)]; congr; ext; exact ha
  · rw [OreLocalization.expand r₃ s₃ rc (hc.symm ▸ (sc * (sa * s₁)).2)]; congr; ext; exact hc

Goal state after:
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₁
i : m
⊢ ((toMatrix v₁ v₂) f *ᵥ ⇑(v₁.repr x)) i = (v₂.repr (f x)) i

Tactic:
← Matrix.toLin'_apply,

Goal state after:
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₁
i : m
⊢ (toLin' ((toMatrix v₁ v₂) f)) (⇑(v₁.repr x)) i = (v₂.repr (f x)) i
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: 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₀ : Type ?u.16
inst✝⁴ : Semiring R₀
inst✝³ : Module R₀ X
inst✝² : Module R₀ R
inst✝¹ : IsScalarTower R₀ R X
inst✝ : IsScalarTower R₀ R R
x : OreLocalization S X
⊢ 0 • x = 0

Tactic:
rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]

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

Goal state before:
pp: case 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₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (algebraMap R₀ R) r /ₒ 1 * (r₁ /ₒ s₁) = r₁ /ₒ s₁ * ((algebraMap R₀ R) r /ₒ 1)

Tactic:
mul_div_one,

Goal state after:
case 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₀ : Type ?u.16
inst✝¹ : CommSemiring R₀
inst✝ : Algebra R₀ R
r : R₀
r₁ : R
s₁ : ↥S
⊢ (algebraMap R₀ R) r /ₒ 1 * (r₁ /ₒ s₁) = r₁ * (algebraMap R₀ R) r /ₒ s₁
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case pos
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
this : DecidableEq M
val✝ : Fintype ι
N : Submodule R M
ih : ∀ N' ≤ N, ∀ x ∈ N, (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → ∃ n, Nonempty (Basis (Fin n) R ↥N')
b' : Basis (Fin (Fintype.card ι)) R ↥⊤ := (b.reindex (Fintype.equivFin ι)).map (LinearEquiv.ofTop ⊤ ⋯).symm
N_bot : N = ⊥
⊢ ∃ n, Nonempty (Basis (Fin n) R ↥N)

Tactic:
subst N_bot
    exact ⟨0, ⟨Basis.empty _⟩⟩

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

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

Tactic:
refine B'.toSubmodule.sum_mem ?_

Goal state after:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
⊢ ∀ c ∈ l.support, (fun a b ↦ r ^ n • b • ↑a) c (l c) ∈ Subalgebra.toSubmodule B'
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 ≠ ⊤
hx : ⊤ = R ∙ 0
f : (R ⧸ (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker = ⊤
⊢ Nontrivial (M ⧸ N)

Tactic:
rwa [Submodule.Quotient.nontrivial_iff]

Goal state after:
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
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective ⇑ϕ
ψ : M ⊗[R] M →ₗ[R] R ⧸ I := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
⊢ Nontrivial (R ⧸ I)

Tactic:
rwa [Submodule.Quotient.nontrivial_iff]

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
semiring✝ : Semiring α := ⋯
algebra✝ : Algebra R α := ⋯
r : R
⊢ e.symm (e.ringEquiv.toFun ((algebraMap R α) r)) = e.symm ((algebraMap R β) r)

Tactic:
simp only [RingEquiv.toEquiv_eq_coe, toFun_as_coe, EquivLike.coe_coe, ringEquiv_apply,
          symm_apply_apply, algebraMap_def]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
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:
by rw [smul_mul_assoc, ← mul_smul_comm, smul_sub, smul_inv_smul, h.val_inv_mul]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ (↑ₐ r + -a) = σ (↑ₐ r - a)

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ σ (↑ₐ r + -a) = σ (↑ₐ r + -a)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ (algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a

Tactic:
simp_rw [Unitization.quasispectrum_eq_spectrum_inr' _ S a, spectrum.algebraMap_mem_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Units

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
x : (i : ι) → M i
inst✝ : ∀ (i : ι), Subsingleton (M i)ˣ
⊢ ∀ (a : (i : ι) → M i), IsUnit a → a = 1

Tactic:
simp [Pi.isUnit_iff, funext_iff]

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
⊢ Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ ⟨↑x, ⋯⟩ = (f i) x

Tactic:
Set.iUnionLift_inclusion

Goal state after:
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
⊢ (f i) x = (f i) x

case h
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
⊢ ↑(K i) ⊆ ↑(iSup K)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R (⨁ (i : ι), M i) = ∑ i, finrank R (M i)

Tactic:
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_directSum, ← mk_sigma,
    mk_toNat_eq_card, card_sigma]

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

Goal state before:
pp: case hsp
R✝ : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst✝⁸ : Semiring R✝
inst✝⁷ : CommSemiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R✝ M
R : Type u_2
V : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
W : Submodule R V
m : Type u_4
n : Type u_5
bW : Basis m R ↥W
bQ : Basis n R (V ⧸ W)
b : m ⊕ n → V := Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)
br : ⇑W.mkQ ∘ b ∘ Sum.inr = ⇑bQ
⊢ span R (range (⇑W.mkQ ∘ surjInv ⋯ ∘ ⇑bQ)) = span R (range ⇑bQ)

Tactic:
congr 2

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∃ f, ∑ e ∈ t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
refine ⟨Subtype.val.extend g 0, ?_, z, z.2, by rwa [Subtype.val_injective.extend_apply]⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : ∑ i, g i • ↑i = 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∑ e ∈ t, extend Subtype.val g 0 e • e = 0
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: case h
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 κ
i : κ
h' : K ∙ b i = ⊤
v : V
hv : v ∈ K ∙ b i
⊢ ∃ r, r • b i = v

Tactic:
mem_span_singleton

Goal state after:
case h
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 κ
i : κ
h' : K ∙ b i = ⊤
v : V
hv : ∃ a, a • b i = v
⊢ ∃ r, r • b i = v
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
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank K ↥(K ∙ v)

Tactic:
rw [Nat.succ_le_iff, finrank_pos_iff]
    use ⟨v, mem_span_singleton_self v⟩, 0
    apply Subtype.coe_ne_coe.mp
    simp [hv]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a b c : FreeAlgebra R X), a + b + c = a + (b + c)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩
    exact Quot.sound Rel.add_assoc

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
n : ℕ
⊢ ∀ (x : FreeAlgebra R X), (n + 1) • x = n • x + x

Tactic:
rintro ⟨a⟩
    dsimp only [HSMul.hSMul, SMul.smul, NSMul.nsmul, Quot.map]
    rw [map_add, map_one, mk_mul, mk_mul, ← add_one_mul (_ : FreeAlgebra R X)]
    congr 1
    exact Quot.sound Rel.add_scalar

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mul_assoc
R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f (a✝ * b✝ * c✝) = liftFun R X f (a✝ * (b✝ * c✝))

Tactic:
change _ * _ * _ = _ * (_ * _)
        rw [mul_assoc]

Goal state after: