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

Goal state before:
pp: case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = diagonal (d ∘ e) j j

Tactic:
diagonal_apply_eq,

Goal state after:
case pos
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : i = j
⊢ d (e j) = (d ∘ e) j
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : ¬ℵ₀ ≤ Module.rank R M
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
simp [Module.finrank, this, Module.rank_zero_iff_of_free]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : ↑I ⊆ ⋃ i ∈ ↑s, ↑(f i)
has : a ∉ s
hbs : b ∈ s
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
⊢ ∃ i ∈ insert b t, I ≤ f i
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
⊢ single i j 0 = 0

Tactic:
unfold single
  ext
  simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R
h✝ : Nontrivial R
⊢ span {r} ∈ (Ideal R)⁰ ↔ r ∈ R⁰

Tactic:
· rw [mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero, ne_eq, zero_eq_bot,
      span_singleton_eq_bot]

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 α
x : Matrix n n α
hx : ∀ (g : Matrix n n α), g * x = x * g
x✝ : Nonempty n
i : n
⊢ ∃ x_1, (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n) x_1 = x

Tactic:
obtain ⟨x, rfl⟩ := mem_range_scalar_iff_commute_single'.mpr fun _ _ ↦ hx _

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
x✝ : Nonempty n
i : n
x : α
hx : ∀ (g : Matrix n n α), g * (scalar n) x = (scalar n) x * g
⊢ ∃ x_1, (∀ (g : α), g * x_1 = x_1 * g) ∧ (scalar n) x_1 = (scalar n) x
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (DirectSum.id M ι) x = x default

Tactic:
rw [← AddEquiv.eq_symm_apply, id_symm_apply, eq_comm]

Goal state after:
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (of (fun i ↦ M) default) (x default) = x
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
ι : Type u_1
inst✝¹ : Fintype ι
G : ι → Type u_2
inst✝ : (i : ι) → AddCommMonoid (G i)
g h : DirectSum ι G
x✝ : ι
⊢ DFinsupp.equivFunOnFintype.toFun (g + h) x✝ =
    (DFinsupp.equivFunOnFintype.toFun g + DFinsupp.equivFunOnFintype.toFun h) x✝

Tactic:
by
    simp only [DFinsupp.equivFunOnFintype, Equiv.toFun_as_coe, Equiv.coe_fn_mk,
      ← DFinsupp.add_apply, Pi.add_apply]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra 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)
r : R
⊢ ∀ (x : ↥(iSup K)),
    Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ (r • x) =
      r • Set.iUnionLift (fun i ↦ ↑(K i)) (fun i x ↦ (f i) x) ⋯ ↑(iSup K) ⋯ x

Tactic:
apply Set.iUnionLift_unary (coe_iSup_of_directed dir) _ (fun _ x => r • x)
            (fun _ _ => rfl)

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra 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)
r : R
⊢ ∀ (i : ι) (x : ↑↑(K i)), (f i) (r • x) = r • (f i) x
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₁ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)

Tactic:
diagonal_apply_eq,

Goal state after:
case inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ d i₁ j₁ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: case refine_2
R : Type u_3
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : IsSelfAdjoint (x * y)
⊢ Commute x y

Tactic:
simpa only [star_mul, hx.star_eq, hy.star_eq] using! h.symm

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

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
α : Type v
β : Type w
γ : Type u_9
inst✝⁷ : Fintype n
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TrivialStar R
inst✝³ : Semiring α
inst✝² : StarRing α
inst✝¹ : Algebra R α
inst✝ : StarModule R α
r : R
M : Matrix n n α
⊢ (conjTransposeRingEquiv n α).toFun (r • M) = r • (conjTransposeRingEquiv n α).toFun M

Tactic:
by
    change conjTransposeRingEquiv n α (r • M) = r • conjTransposeRingEquiv n α M
    simp

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

Goal state before:
pp: case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ diagonal v j j = Function.update v i x j

Tactic:
diagonal_apply_eq,

Goal state after:
case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ v j = Function.update v i x j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ diagonal d (i, k) (i, k) = diagonal (fun i ↦ d (i, k)) i i

Tactic:
diagonal_apply_eq,

Goal state after:
case inl
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i : m
⊢ d (i, k) = diagonal (fun i ↦ d (i, k)) i i
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ diagonal d ⟨k, i⟩ ⟨k, i⟩ = diagonal (fun i ↦ d ⟨k, i⟩) i i

Tactic:
diagonal_apply_eq,

Goal state after:
case inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ d ⟨k, i⟩ = diagonal (fun i ↦ d ⟨k, i⟩) i i
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₃
⊢ (sc • sa • r₁ + (sc • ra • r₂ + rc • r₃)) /ₒ (sc * (sa * s₁)) = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)

Tactic:
← add_oreDiv,

Goal state after:
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₃
⊢ sc • sa • r₁ /ₒ (sc * (sa * s₁)) + (sc • ra • r₂ /ₒ (sc * (sa * s₁)) + rc • r₃ /ₒ (sc * (sa * s₁))) =
    r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype 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 → R
⊢ (toLin' 1) x = x

Tactic:
Matrix.toLin'_one,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype 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 → R
⊢ LinearMap.id x = x
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (toLin' 1) x = x

Tactic:
Matrix.toLin'_one,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ LinearMap.id x = x
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: case c
R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1

Tactic:
OreLocalization.one_def

Goal state after:
case c
R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: case c
R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if h : False then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Tactic:
apply OreLocalization.mul_inv ⟨r, _⟩

Goal state after:
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
m : Matrix ι ι (End A M)
i✝ j✝ : ι
x✝ : M
⊢ ((fun f i j ↦ { toFun := fun x ↦ f (Pi.single j x) i, map_add' := ⋯, map_smul' := ⋯ })
        ((fun m ↦ { toFun := fun x i ↦ ∑ j, (m i j) (x j), map_add' := ⋯, map_smul' := ⋯ }) m) i✝ j✝)
      x✝ =
    (m i✝ j✝) x✝

Tactic:
simp [Pi.single_apply, apply_ite]

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

Goal state before:
pp: case refine_1
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1
n : ℕ
f : End A (Fin n → A)
surj : Surjective ⇑f
⊢ Injective ⇑f

pp: case refine_2
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
⊢ g * f = 1

Tactic:
· have ⟨g, eq⟩ := Module.projective_lifting_property _ .id surj
    exact injective_of_comp_eq_id _ _ (h _ eq)

Goal state after:
case refine_2
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
⊢ g * f = 1
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
⊢ star (star x) = x

Tactic:
by
    simp_rw [star]
    rw [congr_congr]
    convert! congr($congr_refl_refl x) <;> ext <;> simp

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

Goal state before:
pp: 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₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ l a • r ^ n₁ a • ↑a ∈ B'

Tactic:
refine Subalgebra.smul_mem _ ?_ _

Goal state after:
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₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ n₁ a • ↑a ∈ B'
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_4
inst✝⁴ : CommSemiring S
K : Type u_5
inst✝³ : CommSemiring K
inst✝² : Algebra R K
e : R ≃+* S
inst✝¹ : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h : ∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)
inst✝ : IsLocalization M₁ K
⊢ IsLocalization M₂ K

Tactic:
IsLocalization.isLocalization_iff_of_base_ringEquiv _ _ e,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_4
inst✝⁴ : CommSemiring S
K : Type u_5
inst✝³ : CommSemiring K
inst✝² : Algebra R K
e : R ≃+* S
inst✝¹ : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h : ∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)
inst✝ : IsLocalization M₁ K
⊢ IsLocalization (Submonoid.map e M₂) K
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
x✝ : R × ↥M
⊢ mk x✝.1 x✝.2 = mk 1 1

Tactic:
by
      congr <;> apply Subsingleton.elim

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

Goal state before:
pp: case zero
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
⊢ ∃ J, ∃ (_ : J.FG), ∃ y, 0 = (rTensor M J.subtype) y

Tactic:
exact ⟨⊥, fg_bot, 0, rfl⟩

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

Goal state before:
pp: R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hM : 0 ∉ M
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
⊢ Bijective ⇑(algebraMap R Rₘ)

Tactic:
let := hR.toField

Goal state after:
R : Type u_4
Rₘ : Type u_5
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
hM : 0 ∉ M
hR : IsField R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
this : Field R := hR.toField
⊢ Bijective ⇑(algebraMap R Rₘ)
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case refine_1
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) * (1 + y * h.unit.inv * x) = 1

Tactic:
calc
        (1 - y * x) * (1 + y * (IsUnit.unit h).inv * x) =
            1 - y * x + y * ((1 - x * y) * h.unit.inv) * x := by noncomm_ring
        _ = 1 := by simp only [Units.inv_eq_val_inv, IsUnit.mul_val_inv, mul_one, sub_add_cancel]

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
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩ <;>
    simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul,
      star_star, star_one] using IsUnit.star h

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

Goal state before:
pp: case refine_3
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y x₁ x₂ : A ⊗[R] B
h₁ : x₁ * y = y * x₁
⊢ x₂ * y = y * x₂ → (x₁ + x₂) * y = y * (x₁ + x₂)

Tactic:
h₂

Goal state after:
case refine_3
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
x y x₁ x₂ : A ⊗[R] B
h₁ : x₁ * y = y * x₁
h₂ : x₂ * y = y * x₂
⊢ (x₁ + x₂) * y = y * (x₁ + x₂)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x : A) (y : B) (x_1 : A) (y_1 : B), (x_1 ⊗ₜ[R] y_1 * x ⊗ₜ[R] y) • m = x_1 ⊗ₜ[R] y_1 • x ⊗ₜ[R] y • m

Tactic:
intro a₁ b₁ a₂ b₂
      -- Porting note: was one `simp only`, not two
      simp only [(· • ·), Algebra.TensorProduct.tmul_mul_tmul]
      simp only [moduleAux_apply, mul_smul, smul_comm a₁ b₂]

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

Goal state before:
pp: R✝¹ : Type uR
R' : Type u_1
S✝ : Type uS
T✝ : Type u_2
A✝ : Type uA
B✝ : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴⁴ : CommSemiring R✝¹
inst✝⁴³ : 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✝
inst✝³⁵ : Semiring C
inst✝³⁴ : Algebra R✝¹ C
inst✝³³ : Algebra S✝ C
inst✝³² : IsScalarTower R✝¹ S✝ C
inst✝³¹ : Semiring D
inst✝³⁰ : Algebra R✝¹ D
inst✝²⁹ : Semiring E
inst✝²⁸ : Algebra R✝¹ E
inst✝²⁷ : Algebra S✝ E
inst✝²⁶ : IsScalarTower R✝¹ S✝ E
inst✝²⁵ : Semiring F
inst✝²⁴ : Algebra R✝¹ F
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
⊢ (q • m) ⊗ₜ[R] n = m ⊗ₜ[R] (q • n)

Tactic:
have : IsAddTorsionFree (M ⊗[R] N) := .of_module_rat _

Goal state after:
R✝¹ : Type uR
R' : Type u_1
S✝ : Type uS
T✝ : Type u_2
A✝ : Type uA
B✝ : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝⁴⁴ : CommSemiring R✝¹
inst✝⁴³ : 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✝
inst✝³⁵ : Semiring C
inst✝³⁴ : Algebra R✝¹ C
inst✝³³ : Algebra S✝ C
inst✝³² : IsScalarTower R✝¹ S✝ C
inst✝³¹ : Semiring D
inst✝³⁰ : Algebra R✝¹ D
inst✝²⁹ : Semiring E
inst✝²⁸ : Algebra R✝¹ E
inst✝²⁷ : Algebra S✝ E
inst✝²⁶ : IsScalarTower R✝¹ S✝ E
inst✝²⁵ : Semiring F
inst✝²⁴ : Algebra R✝¹ F
R✝ : Type u_3
S : Type u_4
T : Type u_5
A : Type u_6
B : Type u_7
inst✝²³ : CommSemiring R✝
inst✝²² : CommSemiring S
inst✝²¹ : CommSemiring T
inst✝²⁰ : Semiring A
inst✝¹⁹ : Semiring B
inst✝¹⁸ : Algebra R✝ A
inst✝¹⁷ : Algebra R✝ B
inst✝¹⁶ : Algebra S A
inst✝¹⁵ : Algebra S B
inst✝¹⁴ : Algebra T A
inst✝¹³ : SMulCommClass R✝ T A
inst✝¹² : SMulCommClass S T A
inst✝¹¹ : SMulCommClass R✝ S A
inst✝¹⁰ : CompatibleSMul R✝ S A B
inst✝⁹ : Algebra R✝ S
inst✝⁸ : CompatibleSMul R✝ S S A
inst✝⁷ : CompatibleSMul S R✝ S A
R : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module ℚ M
inst✝ : Module ℚ N
q : ℚ
m : M
n : N
this : IsAddTorsionFree (M ⊗[R] N)
⊢ (q • m) ⊗ₜ[R] n = m ⊗ₜ[R] (q • n)
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

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

Tactic:
by
  rw [← Set.inter_union_compl (quasispectrum R (a * b)) {r | IsUnit r},
    ← Set.inter_union_compl (quasispectrum R (b * a)) {r | IsUnit r}]
  congr! 1
  · simpa [Set.inter_comm _ {r | IsUnit r}, Unitization.quasispectrum_eq_spectrum_inr,
      Unitization.inr_mul] using spectrum.setOfPred_isUnit_inter_mul_comm _ _
  · rw [Set.inter_eq_right.mpr, Set.inter_eq_right.mpr]
    all_goals exact fun _ ↦ quasispectrum.not_isUnit_mem _

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

Goal state before:
pp: 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
⊢ quasispectrum R (a, b) = quasispectrum R a ∪ quasispectrum R b

Tactic:
by
  apply compl_injective
  ext r
  simp only [quasispectrum, Set.mem_compl_iff, Set.mem_ofPred_eq, not_forall, not_not,
    Set.mem_union]
  by_cases hr : IsUnit r
  · lift r to Rˣ using hr with r' hr'
    simp [isQuasiregular_prod_iff]
  · simp [hr]

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
a : A
b : B
⊢ (f a * 1) ⊗ₜ[R] (1 * g b) ∈ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)

Tactic:
← tmul_mul_tmul

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
a : A
b : B
⊢ f a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] g b ∈ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)