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

Goal state before:
pp: case inr
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 j : m' k
hij : i ≠ j
⊢ diagonal d ⟨k, i⟩ ⟨k, j⟩ = 0

Tactic:
diagonal_apply_ne _ (mt (fun h => ?_) hij)

Goal state after:
case inr
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 j : m' k
hij : i ≠ j
⊢ 0 = 0

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 j : m' k
hij : i ≠ j
h : ⟨k, i⟩ = ⟨k, j⟩
⊢ i = j
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
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
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) ∘ₗ
      lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) =
    LinearMap.id

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²³ : CommSemiring R
inst✝²² : CommSemiring A
inst✝²¹ : Semiring B
inst✝²⁰ : Algebra R A
inst✝¹⁹ : Algebra R B
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module A M
inst✝¹⁵ : Module B M
inst✝¹⁴ : IsScalarTower R A M
inst✝¹³ : IsScalarTower R B M
inst✝¹² : SMulCommClass A B M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module A P
inst✝⁷ : AddCommMonoid P'
inst✝⁶ : Module A P'
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R Q
inst✝³ : Module R P
inst✝² : IsScalarTower R A P
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ lift (uncurry R A B P Q (M ⊗[A] P ⊗[R] Q) ∘ₗ curry (mk R B (M ⊗[A] P) Q)) ∘ₗ
      lift (lift (lcurry R A B P Q (M ⊗[A] (P ⊗[R] Q)) ∘ₗ mk A B M (P ⊗[R] Q))) =
    LinearMap.id

Tactic:
ext; rfl

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

Goal state before:
pp: case tmul
R : Type uR
A : Type uA
N : Type uN
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : A
y : A ⊗[R] N
⊢ (cancelBaseChange R A A A N) (b ⊗ₜ[A] y) = (TensorProduct.lid A (A ⊗[R] N)) (b ⊗ₜ[A] y)

Tactic:
induction y using TensorProduct.induction_on with
    | zero => simp
    | tmul a m =>
      simp only [cancelBaseChange_tmul, lid_tmul, smul_tmul', smul_eq_mul, mul_comm]
    | add x y hx hy =>
      simp only [tmul_add, map_add, lid_tmul, hx, hy]

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: case inr
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
⊢ False

Tactic:
obtain ⟨m, -, hm⟩ := Submonoid.mem_closure_finset (x := a).mp (by rw [hSgen]; exact mem_top _)

Goal state after:
case inr
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 : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
⊢ False
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 * ↑sc * sb) • r₁ + (↑sd * (↑sc * rb)) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂

Tactic:
hd,

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 * ↑sc * sb) • r₁ + (↑sd * (rc * ra)) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂
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₁' : ↥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
⊢ ↑sd * rb * ↑s₁' = rd * rc * ↑s₂

Tactic:
hd,

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₁' : ↥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
⊢ rd * ↑sc * ↑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₁' : ↥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₂
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = ((↑sd * rb) • r₁' + (rd * rc) • r₂) /ₒ ⟨↑sd * ↑sb * ↑s₁, ⋯⟩

Tactic:
hd,

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₁' : ↥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₂
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = ((rd * ↑sc) • r₁' + (rd * rc) • r₂) /ₒ ⟨↑sd * ↑sb * ↑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
⊢ rd * (rb * ↑s₁) = ↑sd * ↑sc * ↑s₃

Tactic:
← hb',

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
⊢ rd * (↑sb * ↑s₂) = ↑sd * ↑sc * ↑s₃
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ ⨆ i, Submodule.map M.vecMulLinear (Submodule.map (LinearMap.single R (fun i ↦ R) i) (R ∙ 1)) =
    span R (Set.range M.row)

Tactic:
Submodule.map_span,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ ⨆ i, span R (⇑M.vecMulLinear '' ⇑(LinearMap.single R (fun i ↦ R) i) '' {1}) = span R (Set.range M.row)
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' M) ((toLin' M') x) = x

Tactic:
by rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]

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

Goal state before:
pp: case e_6.e_6
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
⊢ v₁.equivFun.symm ⇑(v₁.repr x) = x

Tactic:
exact v₁.equivFun.symm_apply_apply x

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

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
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module R N₂
inst✝³ : Module S N₁
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ f (mk' S r m • s') = mk' S r m • f s'

Tactic:
rw [← (map_units S m).smul_left_cancel]

Goal state after:
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
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module R N₂
inst✝³ : Module S N₁
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ (algebraMap R S) ↑m • f (mk' S r m • s') = (algebraMap R S) ↑m • mk' S r m • f s'
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
⊢ AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f) = algEquivOfAlgEquiv f

Tactic:
ext; rfl

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 ϕ ϕ
this✝ : Nontrivial (R ⧸ I)
this : Surjective ⇑ψ
⊢ Nontrivial (M ⊗[R] M)

Tactic:
exact this.nontrivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : CommRing β
⊢ CommRing α

Tactic:
by
  let mul := e.mul
  let add_group_with_one := e.addGroupWithOne
  let npow := e.pow ℕ
  apply e.injective.commRing _ <;> intros <;> exact e.apply_symm_apply _

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : (PreQuasiregular A)ˣ
⊢ ↑((fun x ↦
          { val := PreQuasiregular.equiv (↑↑x).toProd.2, inv := PreQuasiregular.equiv (↑↑x⁻¹).toProd.2, val_inv := ⋯,
            inv_val := ⋯ })
        ((fun x ↦
            ⟨{ val := 1 + ↑(PreQuasiregular.equiv.symm ↑x), inv := 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹), val_inv := ⋯,
                inv_val := ⋯ },
              ⋯⟩)
          x)) =
    ↑x

Tactic:
simp [-PreQuasiregular.equiv_symm_apply]

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

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
⊢ (TensorProduct.comm R A B).symm = TensorProduct.comm R B A

Tactic:
ext; rfl

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

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁶ : Semifield R
inst✝⁵ : Semifield S
inst✝⁴ : Ring A
inst✝³ : Algebra R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
a : A
f : S → R
inst✝ : IsScalarTower R S A
h : SpectrumRestricts a f
⊢ ⇑(algebraMap R S) '' spectrum R a ⊆ spectrum S a

Tactic:
simpa only [spectrum.preimage_algebraMap] using
      (spectrum S a).image_preimage_subset (algebraMap R S)

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
C : Type uC
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ↑↑(leftComm R A B C) = ↑(_root_.TensorProduct.leftComm R A B C)

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ lmul'' R = (↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul S R S S S)

Tactic:
ext; rfl

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

Goal state before:
pp: R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
⊢ ↑(lmulEquiv R S) = ↑(lidOfCompatibleSMul R S S)

Tactic:
ext; rfl

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

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
u : Aˣ
⊢ 0 ≤ a ∧ IsUnit (↑u * a * star ↑u) ↔ 0 ≤ a ∧ IsUnit a

Tactic:
rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]

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

Goal state before:
pp: case 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 A
inst✝ : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : ∑ i ∈ b.support, (x * b i) ⊗ₜ[R] ℬ i = ∑ i ∈ b.support, (b i * x) ⊗ₜ[R] ℬ i
⊢ ∑ x_1 ∈ b.support, ((TensorProduct.mk R A B).flip (ℬ x_1)) ((x • b) x_1) =
    ∑ x_1 ∈ b.support, ((TensorProduct.mk R A B).flip (ℬ x_1)) ((mapRange (fun x_2 ↦ x_2 * x) ⋯ b) x_1)

Tactic:
simpa only [Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, LinearMap.flip_apply,
      TensorProduct.mk_apply, Finsupp.mapRange_apply] using hw

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R (id '' s)).mkQ ∘ id) t

Tactic:
rw [image_id]

Goal state after:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R (⇑M'.mkQ) t
⊢ LinearIndepOn R (⇑(span R s).mkQ ∘ id) t
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case e'_3.mpr
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
y : ↥(centralizer R S) ⊗[R] A
hy : (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y = (Algebra.TensorProduct.comm R A B) x
⊢ (Algebra.TensorProduct.comm R A B)
      ((Algebra.TensorProduct.map (AlgHom.id R A) (centralizer R S).val)
        ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A) y)) =
    (Algebra.TensorProduct.comm R A B) x

Tactic:
rw [← hy, comm_comp_map_apply, ← Algebra.TensorProduct.comm_symm, AlgEquiv.symm_apply_apply]

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

Goal state before:
pp: F : Type u_2
E : Type u_3
inst✝⁶ : CommRing F
inst✝⁵ : IsDomain F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : IsTorsionFree F E
inst✝ : Nontrivial E
⊢ Module.rank F ↥(F ∙ 1) = 1

Tactic:
rank_span_set,

Goal state after:
F : Type u_2
E : Type u_3
inst✝⁶ : CommRing F
inst✝⁵ : IsDomain F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : IsTorsionFree F E
inst✝ : Nontrivial E
⊢ #↑{1} = 1

F : Type u_2
E : Type u_3
inst✝⁶ : CommRing F
inst✝⁵ : IsDomain F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : IsTorsionFree F E
inst✝ : Nontrivial E
⊢ LinearIndepOn F id {1}
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
⊢ Submodule.map W.mkQ (span R (range (surjInv ⋯ ∘ ⇑bQ))) = ⊤

Tactic:
Submodule.map_span,

Goal state after:
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 (⇑W.mkQ '' range (surjInv ⋯ ∘ ⇑bQ)) = ⊤
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
hs : LinearIndepOn K id s
⊢ ↑⊤ ⊆ ↑(span K (range ((hs.extend ⋯).domRestrict id)))

Tactic:
by simpa using hs.subset_span_extend (subset_univ s)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ (adjoin R s).toNonUnitalSubalgebra ≤ S.toNonUnitalSubalgebra ↔ s ⊆ ↑S

Tactic:
adjoin_toNonUnitalSubalgebra,

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ NonUnitalAlgebra.adjoin R (s ∪ star s) ≤ S.toNonUnitalSubalgebra ↔ s ⊆ ↑S
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ (adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))

Tactic:
adjoin_toNonUnitalSubalgebra,

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ (NonUnitalAlgebra.adjoin R (s ∪ star s)).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : NonUnitalSemiring A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module R A
inst✝¹³ : NonUnitalSemiring B
inst✝¹² : StarRing B
inst✝¹¹ : Module R B
inst✝¹⁰ : FunLike F A B
inst✝⁹ : NonUnitalAlgHomClass F R A B
inst✝⁸ : StarHomClass F A B
S : NonUnitalStarSubalgebra R A
ι : Type u_1
inst✝⁷ : StarRing R
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : IsScalarTower R B B
inst✝² : SMulCommClass R B B
inst✝¹ : StarModule R B
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
⊢ (f i) ⟨x, hxi⟩ = (f j) ⟨x, hxj⟩

Tactic:
let ⟨k, hik, hjk⟩ := dir i j
            rw [hf i k hik, hf j k hjk]
            rfl

Goal state after: