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

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (of fun i j ↦ diagonal v (Sum.inl i) (Sum.inl j)) = diagonal fun i ↦ v (Sum.inl i)

Tactic:
funext i j

Goal state after:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
i j : l
⊢ of (fun i j ↦ diagonal v (Sum.inl i) (Sum.inl j)) i j = diagonal (fun i ↦ v (Sum.inl i)) i j
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (of fun i j ↦ diagonal v (Sum.inr i) (Sum.inr j)) = diagonal fun i ↦ v (Sum.inr i)

Tactic:
funext i j

Goal state after:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
i j : m
⊢ of (fun i j ↦ diagonal v (Sum.inr i) (Sum.inr j)) i j = diagonal (fun i ↦ v (Sum.inr i)) i j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
⊢ (A.submatrix ⇑e ⇑f).updateRow i r = (A.updateRow (e i) fun j ↦ r (f.symm j)).submatrix ⇑e ⇑f

Tactic:
by
  ext i' j
  simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]

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

Goal state before:
pp: ι : 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
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))

Tactic:
let a := generator (ϕ.submoduleImage N)

Goal state after:
ι : 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)
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : 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
i : ι
x✝ : i ∈ Finset.univ
⊢ (a * c i) • b'M i = (b'M.repr ⟨y, ⋯⟩) i • b'M i

Tactic:
← hc

Goal state after:
ι : 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
i : ι
x✝ : i ∈ Finset.univ
⊢ (b'M.coord i) ⟨y, ⋯⟩ • b'M i = (b'M.repr ⟨y, ⋯⟩) i • b'M i
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : 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
⊢ ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0

Tactic:
intro c x xM' hc

Goal state after:
ι : 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
c : R
x : O
xM' : x ∈ M'
hc : c • y' + x = 0
⊢ c = 0
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
⊢ rd * (rc * ↑s₂) = rd * rc * ↑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₁' : ↥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 * rc * ↑s₂ = rd * rc * ↑s₂
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
m : M
hm : m ∈ nonZeroDivisors M
n : N
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
h0 : ∃ s, ↑s * ms.1 * m = 0
⊢ n = 0

Tactic:
mul_right_mem_nonZeroDivisorsRight_eq_zero_iff hm.2

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
hm : m ∈ nonZeroDivisors M
n : N
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
h0 : ∃ s, ↑s * ms.1 = 0
⊢ n = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * (f r₃ * f r₂) = ↑(fS s₂)⁻¹ * f r₂

Tactic:
← mul_assoc

Goal state after:
case c.c.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑s₁ = r₃ * ↑s₂
⊢ ↑(fS s₁)⁻¹ * ↑(fS s₃)⁻¹ * f r₃ * f r₂ = ↑(fS s₂)⁻¹ * f r₂
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case right
ι : 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 : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
i : ι
hi : i ∈ I
⊢ s i ∈ N

Tactic:
exact subset_span (mem_range_self (⟨i, hi⟩ : I))

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g ((toLocalizationMap M S).sec y).1 *
        (g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2) +
      g ↑((toLocalizationMap M S).sec y).2 *
        (g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2) =
    g ↑((toLocalizationMap M S).sec y).2 *
      (g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1)

Tactic:
← mul_assoc

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✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g ((toLocalizationMap M S).sec y).1 * g ↑((toLocalizationMap M S).sec x).2 *
        ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ↑((toLocalizationMap M S).sec y).2 * g ((toLocalizationMap M S).sec x).1 *
        ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec y).2 * g ↑((toLocalizationMap M S).sec x).2 *
      ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).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
inst✝¹ : IsLocalization M S
inst✝ : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : x ∈ nonZeroDivisors R
⊢ (algebraMap R S) x ≠ 0

Tactic:
by
  rw [Ne, to_map_eq_zero_iff S hM]
  exact nonZeroDivisors.ne_zero hx

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommRing P
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : IsDomain A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ Function.Injective ⇑((algebraMap A (FractionRing A)).comp (algebraMap R A))

Tactic:
exact (FaithfulSMul.algebraMap_injective A (FractionRing A)).comp
    (FaithfulSMul.algebraMap_injective R A)

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
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst✝¹⁹ : CommSemiring Rₘ
inst✝¹⁸ : CommSemiring Sₙ
inst✝¹⁷ : CommSemiring Rₘ'
inst✝¹⁶ : CommSemiring Sₙ'
inst✝¹⁵ : Algebra R Rₘ
inst✝¹⁴ : Algebra S Sₙ
inst✝¹³ : Algebra R Rₘ'
inst✝¹² : Algebra S Sₙ'
inst✝¹¹ : Algebra R Sₙ
inst✝¹⁰ : Algebra Rₘ Sₙ
inst✝⁹ : Algebra Rₘ' Sₙ'
inst✝⁸ : Algebra R Sₙ'
N : Submonoid S
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization N Sₙ
inst✝⁵ : IsLocalization M Rₘ'
inst✝⁴ : IsLocalization N Sₙ'
inst✝³ : IsScalarTower R Rₘ Sₙ
inst✝² : IsScalarTower R S Sₙ
inst✝¹ : IsScalarTower R Rₘ' Sₙ'
inst✝ : IsScalarTower R S Sₙ'
⊢ (↑(algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ) = (algebraMap Rₘ' Sₙ').comp ↑(algEquiv M Rₘ Rₘ')

Tactic:
refine IsLocalization.ringHom_ext M (RingHom.ext fun x => ?_)
  simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes]
  rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
    ← AlgEquiv.restrictScalars_apply R, AlgEquiv.commutes]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
y : A ⊗[R] A
h' : ∀ (x : A ⊗[R] A), ∃ a, x = a ⊗ₜ[R] 1
a : A
hxy : (lift (LinearMap.mul R A)) (a ⊗ₜ[R] 1) = (lift (LinearMap.mul R A)) y
⊢ a ⊗ₜ[R] 1 = y

Tactic:
obtain ⟨b, rfl⟩ := h' y

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
h : ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
h' : ∀ (x : A ⊗[R] A), ∃ a, x = a ⊗ₜ[R] 1
a b : A
hxy : (lift (LinearMap.mul R A)) (a ⊗ₜ[R] 1) = (lift (LinearMap.mul R A)) (b ⊗ₜ[R] 1)
⊢ a ⊗ₜ[R] 1 = b ⊗ₜ[R] 1
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).Finite

Tactic:
convert_to (((Algebra.TensorProduct.comm _ _ _).trans
      (Algebra.TensorProduct.cancelBaseChange R S S S' T)).toAlgHom.comp
    Algebra.TensorProduct.includeLeft).Finite

Goal state after:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) =
    (↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
            (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
      Algebra.TensorProduct.includeLeft

R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this✝¹ : Algebra S S' := f.toAlgebra
this✝ : IsScalarTower R S S'
this : Module.Finite S S'
⊢ ((↑((Algebra.TensorProduct.comm S (TensorProduct R S T) S').trans
            (Algebra.TensorProduct.cancelBaseChange R S S S' T))).comp
      Algebra.TensorProduct.includeLeft).Finite
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 α := e.semiring
algebra✝ : Algebra R α := Equiv.algebra R e
r : R
⊢ e.ringEquiv.toFun ((algebraMap R α) r) = (algebraMap R β) r

Tactic:
apply e.symm.injective

Goal state after:
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)
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
a b c : A
h₁ : (↑ₐ r - a) * b = 1
h₂ : c * (↑ₐ r - a) = 1
⊢ b * (↑ₐ r - a) = 1

Tactic:
rwa [← left_inv_eq_right_inv h₂ h₁]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
h : adjoin A ↑(Subalgebra.map includeRight ⊤) = ⊤
⊢ adjoin A ((fun x ↦ 1 ⊗ₜ[R] x) '' s) = ⊤

Tactic:
by
    simp [← h, ← hs, AlgHom.map_adjoin, adjoin_adjoin_of_tower]

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set B
hs : adjoin R s = ⊤
⊢ adjoin A ((fun x ↦ 1 ⊗ₜ[R] x) '' s) = ⊤

Tactic:
by
  suffices h : adjoin A ((⊤ : Subalgebra R B).map (includeRight (A := A)) : Set (A ⊗[R] B)) = ⊤ by
    simp [← h, ← hs, AlgHom.map_adjoin, adjoin_adjoin_of_tower]
  rw [← Algebra.toSubmodule_eq_top, ← top_le_iff, Algebra.map_top, ← Submodule.baseChange_top,
    Submodule.baseChange_eq_span, Submodule.map_top]
  exact span_le_adjoin _ _

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

Goal state before:
pp: R : Type u_3
S : 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
⊢ quasispectrum R ↑a = quasispectrum R a

Tactic:
rw [quasispectrum_eq_spectrum_union_zero, quasispectrum_eq_spectrum_inr' R S]

Goal state after:
R : Type u_3
S : 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
⊢ spectrum R ↑a ∪ {0} = spectrum R ↑a
Module: Mathlib.Algebra.Algebra.StrictPositivity

Goal state before:
pp: A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
⊢ 0 < x

Tactic:
have h₁ : 0 ≤ x := by grind

Goal state after:
A : Type u_1
𝕜 : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : PartialOrder A
inst✝³ : CommSemiring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : Algebra 𝕜 A
inst✝ : NonnegSpectrumClass 𝕜 A
a : A
ha : IsStrictlyPositive a
x : 𝕜
hx : x ∈ spectrum 𝕜 a
h₁ : 0 ≤ x
⊢ 0 < x
Module: Mathlib.Algebra.Order.Star.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * c

Tactic:
← hc

Goal state after:
R : Type u_1
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : 0 ≤ a
c : R
hc : IsSelfAdjoint c
⊢ 0 ≤ c * a * star c
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
b : Finset M
h : LinearIndependent R fun x ↦ ↑x
⊢ Fintype.card ↥b ≤ finrank R M

Tactic:
exact h.fintype_card_le_finrank

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

Goal state before:
pp: 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)
⊢ Basis (m ⊕ n) R V

Tactic:
let b : m ⊕ n → V := Sum.elim (fun i ↦ bW i) ((Function.surjInv W.mkQ_surjective) ∘ bQ)
  have br : W.mkQ ∘ b ∘ Sum.inr = bQ := by
    ext j
    apply Function.rightInverse_surjInv W.mkQ_surjective
  apply Basis.mk (v := b)
  · apply LinearIndependent.sumElim_of_quotient
    · exact bW.linearIndependent
    · convert! bQ.linearIndependent
  · unfold b
    rw [Set.Sum.elim_range, Submodule.span_union,
      show Set.range (fun i ↦ (bW i : V)) = W.subtype '' (Set.range (fun i ↦ bW i)) by aesop,
      ← Submodule.map_span, bW.span_eq, Submodule.map_top, Submodule.range_subtype, top_le_iff,
      ← Submodule.map_mkQ_eq_top, Submodule.map_span, ← Set.range_comp, ← bQ.span_eq]
    congr 2

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: 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'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : ⇑f '' B ⊆ this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
⊢ ∃ g, g ∘ₗ f = id

Tactic:
refine ⟨(hC.constr ℕ : _ → _) (C.domRestrict (invFun f)), hB.ext fun b => ?_⟩

Goal state after:
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'
f : V →ₗ[K] V'
hf_inj : f.ker = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndepOn K _root_.id (Set.range ⇑hB)
this : LinearIndepOn K _root_.id (⇑f '' B)
C : Set V' := this.extend ⋯
BC : ⇑f '' B ⊆ this.extend ⋯
hC : Basis (↑(this.extend ⋯)) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ((hC.constr ℕ) (C.domRestrict (invFun ⇑f)) ∘ₗ f) (hB b) = id (hB b)
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 + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun x ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
⊢ finrank R M < #t - 1

Tactic:
exact Nat.lt_pred_iff.mpr h

Goal state after: