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

Goal state before:
pp: case inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ 0 k' l' = single (i, k) (j, l) r (i', k') (j', l')

Tactic:
single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi),

Goal state after:
case inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
i' : I
k' : K
j' : J
l' : L
hi : i ≠ i'
⊢ 0 k' l' = 0
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = map N.subtype (span R (Set.range ⇑b))

Tactic:
b.span_eq,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = map N.subtype ⊤
Module: Mathlib.LinearAlgebra.Basis.Fin

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = map N.subtype (span R (Set.range ⇑b))

Tactic:
b.span_eq,

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
v : ι → M
inst✝⁴ : Ring R
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module R₂ M
x y✝ : M
b✝ : Basis ι R M
n : ℕ
N : Submodule R M
b : Basis (Fin n) R ↥N
y : M
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ N = map N.subtype ⊤
Module: Mathlib.LinearAlgebra.Basis.SMul

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : j ∈ span R (range v)
⊢ j ∈ span R (range (w • v))

Tactic:
rw [Submodule.mem_span] at hj ⊢

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ ↑p → j ∈ p
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
⊢ A.updateCol i b = (replicateCol (Fin 1) b).submatrix id (Function.const n 0)

Tactic:
by
  ext x y
  simp [Subsingleton.elim i y]

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 + N i✝.2 i✝.1 j✝.1 else 0) =
    (if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0) + if i✝.2 = j✝.2 then N i✝.2 i✝.1 j✝.1 else 0

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then x • M i✝.2 i✝.1 j✝.1 else 0) = x • if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) +
      if h : i✝.fst = j✝.fst then N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0

Tactic:
split_ifs <;> simp

Goal state after:
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, M k i (cast ⋯ x) * if h : k = k' then N k x (cast ⋯ j) else 0

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then x • M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    x • if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
x✝ : Subsingleton N
c : ↥S
eq : ↑c * 0 = ↑c * 1
⊢ 0 ∈ S

Tactic:
rw [mul_zero, mul_one] at eq

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
x✝ : Subsingleton N
c : ↥S
eq : 0 = ↑c
⊢ 0 ∈ 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✝¹ : AddGroup X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ -x + x = 0

Tactic:
induction x with | _ r s =>  _ 

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) + r /ₒ s = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.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₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ ⟨↑sb * ra * ↑s₃, hs₃rasb⟩) • (r₁ /ₒ s₁)

Tactic:
← Subtype.coe_eq_of_eq_mk ha'

Goal state after:
case c.c.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₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁)
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this✝ : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this✝.choose
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
a : ι → R
ha : ∀ (i : ι), a i ≠ 0
ha' : ∀ (i : ι), a i • s i ∈ N
A : R := ∏ i, a i
hA : A ≠ 0
φ : M →ₗ[R] M := (LinearMap.lsmul R M) A
this : φ.ker = ⊥
ψ : M ≃ₗ[R] ↥φ.range := LinearEquiv.ofInjective φ ⋯
i : ι
⊢ φ (s i) ∈ N

Tactic:
calc
        (∏ j ∈ {i}ᶜ, a j) • a i • s i ∈ N := N.smul_mem _ (ha' i)
        _ = (∏ j, a j) • s i := by rw [Fintype.prod_eq_prod_compl_mul i, mul_smul]

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)
⊢ ∀ (x y : ι → M), (fun i ↦ ∑ j, (m i j) ((x + y) j)) = (fun i ↦ ∑ j, (m i j) (x j)) + fun i ↦ ∑ j, (m i j) (y j)

Tactic:
by intros; ext; simp [Finset.sum_add_distrib]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  mk' (Localization S) ((Pi.evalRingHom R i) r₁) ⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ =
    mk' (Localization S) ((Pi.evalRingHom R i) r₂) ⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂

Tactic:
rw [IsLocalization.eq] at eq ⊢

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  ∃ c,
    ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
      ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
⊢ ∃ c, ↑c * (↑s₂ * r₁) = ↑c * (↑s₁ * r₂)
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
z : K
x y : A
hy : y ∈ A⁰
h : mk' K x ⟨y, hy⟩ = z
⊢ (algebraMap A K) x / (algebraMap A K) y = z

Tactic:
mk'_eq_div

Goal state after:
A : Type u_4
inst✝³ : CommRing A
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
z : K
x y : A
hy : y ∈ A⁰
h : (algebraMap A K) x / (algebraMap A K) ↑⟨y, hy⟩ = z
⊢ (algebraMap A K) x / (algebraMap A K) y = z
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ closure (Set.range ⇑(algebraMap L E) ∪ S) = closure (Set.range ⇑(algebraMap L' E) ∪ S)

Tactic:
hi,

Goal state after:
F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ closure (Set.range (⇑(algebraMap L' E) ∘ ⇑i) ∪ S) = closure (Set.range ⇑(algebraMap L' E) ∪ S)
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 (Submonoid.map e M₂) K

Tactic:
hM

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 M₁ K
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) =
    (algebraMap A (Localization M)) m * (algebraMap R (Localization M)) ↑1

Tactic:
Submonoid.coe_one,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ (algebraMap R (Localization M)) ((algebraMap A R) m) =
    (algebraMap A (Localization M)) m * (algebraMap R (Localization M)) 1
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: case inl
R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
left✝ : Nontrivial R
right✝ : Subsingleton S
c : ↥R⁰
hc : ↑c * 1 = ↑c * 0
⊢ False

Tactic:
simp at hc

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)
x y : M
hy : ϕ y = 1
⊢ ψ (x ⊗ₜ[R] y) = ϕ x

Tactic:
by simp [ψ, hy]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e✝ e : α ≃ β
inst✝¹ : Add β
inst✝ : Mul β
add✝ : Add α := e.add
mul✝ : Mul α := e.mul
⊢ α ≃+* β

Tactic:
exact
    { e with
      map_add' := fun x y => by
        simp [add_def]
      map_mul' := fun x y => by
        simp [mul_def] }

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

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

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

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

Goal state before:
pp: R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.liftBaseChange S ↑f) (((LinearMap.mul S (S ⊗[R] A)) x) y) =
    (LinearMap.liftBaseChange S ↑f) x * (LinearMap.liftBaseChange S ↑f) y

Tactic:
← LinearMap.compr₂_apply,

Goal state after:
R✝ : Type u_1
A✝ : Type u_2
B✝ : Type u_3
inst✝¹⁷ : CommSemiring R✝
inst✝¹⁶ : NonUnitalNonAssocSemiring A✝
inst✝¹⁵ : NonUnitalNonAssocSemiring B✝
inst✝¹⁴ : Module R✝ A✝
inst✝¹³ : Module R✝ B✝
inst✝¹² : SMulCommClass R✝ A✝ A✝
inst✝¹¹ : SMulCommClass R✝ B✝ B✝
inst✝¹⁰ : IsScalarTower R✝ A✝ A✝
inst✝⁹ : IsScalarTower R✝ B✝ B✝
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (((LinearMap.mul S (S ⊗[R] A)).compr₂ (LinearMap.liftBaseChange S ↑f)) x) y =
    (LinearMap.liftBaseChange S ↑f) x * (LinearMap.liftBaseChange S ↑f) y
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
⊢ IsUnit (1 + x)

Tactic:
by
  obtain ⟨y, hy₁, hy₂⟩ := isQuasiregular_iff.mp hx
  refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩
  · convert congr(1 + $(hy₁)) <;> [noncomm_ring; simp]
  · convert congr(1 + $(hy₂)) <;> [noncomm_ring; simp]

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

Goal state before:
pp: case inl
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
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
hx : 0 ∈ quasispectrum S a
⊢ (algebraMap R S) (f 0) = 0

pp: case inr
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
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx✝ : x ∈ quasispectrum S a
hx : x ∈ spectrum S a
⊢ (algebraMap R S) (f x) = x

Tactic:
· simpa using h₁ 0

Goal state after:
case inr
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
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx✝ : x ∈ quasispectrum S a
hx : x ∈ spectrum S a
⊢ (algebraMap R S) (f x) = x
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : AddMonoid R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ (↑(star a)).toProd.1 = (star ↑a).toProd.1

Tactic:
by simp only [fst_star, star_zero, fst_inr]

Goal state after:
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 b : R
hab : a < b
c : R
hc : IsRegular c
⊢ star c * a * c < star c * b * c

Tactic:
by
  rw [(star_left_conjugate_le_conjugate hab.le _).lt_iff_ne, hc.right.ne_iff, hc.star.left.ne_iff]
  exact hab.ne

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 : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
dsimp [iSupLift, inclusion]
  rw [Set.iUnionLift_of_mem]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
rw [StarOrderedRing.le_iff] at hxy ⊢

Goal state after:
R : Type u_4
S : Type u_5
inst✝⁷ : NonUnitalSemiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : NonUnitalSemiring S
inst✝² : PartialOrder S
inst✝¹ : StarRing S
inst✝ : StarOrderedRing S
f : R →⋆ₙ+* S
x y : R
hxy : ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), y = x + p
⊢ ∃ p ∈ AddSubmonoid.closure (range fun s ↦ star s * s), f y = f x + p
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 (Sum.elim (fun i ↦ ↑(bW i)) (surjInv ⋯ ∘ ⇑bQ)))

Tactic:
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]

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 (range (⇑W.mkQ ∘ surjInv ⋯ ∘ ⇑bQ)) = span R (range ⇑bQ)
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: ι : Type w
R : Type u
M : Type v
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
inst✝² : Module.Finite R M
inst✝¹ : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
inst✝ : Fintype { i // p i ≠ ⊥ }
⊢ Fintype.card { i // p i ≠ ⊥ } ≤ finrank R M

Tactic:
by simpa using hp.subtype_ne_bot_le_finrank_aux

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Ring K
inst✝² : IsDomain K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
x : K
H : x ≠ 0
⊢ ∃ y, x * y = 1

Tactic:
have : Function.Surjective (LinearMap.mulLeft F x) :=
    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
  exact this 1

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
⊢ Quot.liftOn 1 (liftFun R X f) ⋯ = 1

Tactic:
by
    change algebraMap _ _ _ = _
    simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: 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
⊢ Quot.liftOn 0 (liftFun R X f) ⋯ = 0

Tactic:
by
    change algebraMap _ _ _ = _
    simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Algebra

Goal state before:
pp: case add
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q r s : R[X]
hr : eval₂ (algebraMap R S) x (r.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) r
hs : eval₂ (algebraMap R S) x (s.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) s
⊢ eval₂ (algebraMap R S) x ((r + s).comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) (r + s)

Tactic:
| add r s hr hs =>

Goal state after: