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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₐ[R] A₂'
x✝ : A₁'
⊢ ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom)
        ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom) f))
      x✝ =
    f x✝

Tactic:
simp

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

Goal state before:
pp: R : Type uR
A : Type uA
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A
inst✝¹² : Algebra R A
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : Module A M
inst✝⁸ : IsScalarTower R A M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module A P
inst✝² : IsScalarTower R A P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂

Tactic:
ext
  simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul,
    add_apply, tmul_add]

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
e₃ : A₃ ≃⋆ₐ[R] A₃'
f : A₁ →⋆ₐ[R] A₂
g : A₂ →⋆ₐ[R] A₃
x✝ : A₁'
⊢ ((e₁.arrowCongr e₃) (g.comp f)) x✝ = (((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
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 Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
f : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry ((curry ((lTensor B M) f ∘ₗ ↑(cancelBaseChange R A B M N))) x✝¹)) 1) x✝ =
    ((curry ((curry (↑(cancelBaseChange R A B M Q) ∘ₗ (lTensor B M) ((lTensor A A) f))) x✝¹)) 1) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q) ((b * a) ⊗ₜ[R] (n ⊗ₜ[R] q)) = (b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q)

Tactic:
simp

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

Goal state before:
pp: case tmul.zero
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
⊢ (cancelBaseChange R A A A N) (b ⊗ₜ[A] 0) = (TensorProduct.lid A (A ⊗[R] N)) (b ⊗ₜ[A] 0)

Tactic:
simp

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✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : Q
x✝ : P
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
simp

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✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ (((curry
            (curry
              (lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))))))
          x✝²)
        x✝¹)
      x✝ =
    (((curry (curry LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A 0)) 1) x✝ = ((AlgebraTensorModule.curry 0) 1) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (r • f))) 1) x✝ = ((AlgebraTensorModule.curry (r • baseChange A f)) 1) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A id)) 1) x✝ = ((AlgebraTensorModule.curry id) 1) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (g ∘ₗ f))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A g ∘ₗ baseChange A f)) 1) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Add α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_7
B : Type u_8
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
f : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry (baseChange B (baseChange A f))) 1)) 1) x✝ =
    ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry
              (↑(cancelBaseChange R A B B N).symm ∘ₗ baseChange B f ∘ₗ ↑(cancelBaseChange R A B B M)))
            1))
        1)
      x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ : α
⊢ x • ![a₀, a₁] = ![x • a₀, x • a₁]

Tactic:
simp

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

Goal state before:
pp: α : Type u
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ a₂ : α
⊢ x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : Module.End R M
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f * g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f * baseChange A g)) 1) x✝

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M ≃ₗ[R] M
⊢ LinearEquiv.baseChange R A M M (f ^ 0) = LinearEquiv.baseChange R A M M f ^ 0

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Mˣ
S : Set M
x : M
hx : x ∈ {p | p ∈ Submonoid.closure S ∧ Irreducible p}
⊢ Irreducible 1 → 1 ∈ S

Tactic:
simp

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

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

Tactic:
← mul_assoc (r ^ n r),

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : A ⊗[R] M →ₗ[A] N
x : M
⊢ ((curry (LinearMap.baseChange A f ∘ₗ ↑(TensorProduct.lid A (A ⊗[R] M)).symm)) 1) x =
    ((curry (↑(TensorProduct.lid A N).symm ∘ₗ f)) 1) x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ ↑1 * 0 = 0 * ↑s

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
⊢ (∃ u v, u • 1 = v • 0 ∧ ↑u * ↑1 = v * ↑1) ↔ 0 ∈ S

Tactic:
simp

Goal state after:
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:
mul_assoc _ _ rb,

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 * (↑sc * rb)) • r₂ = (↑sd * rc * ↑sa) • r₁ + (↑sd * rc * ra) • r₂
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
x✝ : L
⊢ x✝ ∈ f.fieldRange ↔ x✝ ∈ Subfield.map f ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
⊢ ↑(sInf (toSubring '' S)) = ⋂ s ∈ S, ↑s

Tactic:
simp

Goal state after:
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 r' : X
s : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

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

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

Tactic:
intro j

Goal state after:
R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
f : (m → R) →ₗ[R] n → R
j : m
⊢ (vecMulLinear ((fun f i j ↦ f ((single R (fun x ↦ R) i) 1) j) f)) ((Pi.basisFun R m) j) = f ((Pi.basisFun R m) j)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
i : m
j : n
⊢ (fun f i j ↦ f ((single R (fun x ↦ R) i) 1) j) M.vecMulLinear i j = M i j

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (l → R) →ₗ[R] m → R
g : (m → R) →ₗ[R] n → R
⊢ toLinearMapRight' (toMatrixRight' (g ∘ₗ f)) = toLinearMapRight' (toMatrixRight' f * toMatrixRight' g)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
i✝ x✝ : m
⊢ (toLinearMapRight' 1 ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝ =
    (LinearMap.id ∘ₗ LinearMap.single R (fun i ↦ R) i✝) 1 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
⊢ toLinearMapRight' (toMatrixRight' id) = toLinearMapRight' 1

Tactic:
simp

Goal state after:
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
f : (n → R) →ₗ[R] m → R
⊢ ∀ (i : n), ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin ((Pi.basisFun R n) i) = f ((Pi.basisFun R n) i)

Tactic:
intro j

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
f : (n → R) →ₗ[R] m → R
j : n
⊢ ((fun f ↦ of fun i j ↦ f (Pi.single j 1) i) f).mulVecLin ((Pi.basisFun R n) j) = f ((Pi.basisFun R n) j)
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
s : ↥S
⊢ s • 0 = 1 • 0 ∧ ↑s * ↑1 = 1 * ↑s

Tactic:
simp

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

Goal state before:
pp: case 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
⊢ (0 + r✝) /ₒ s✝ = r✝ /ₒ s✝

Tactic:
simp

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

Goal state before:
pp: case 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✝ + 0) /ₒ s✝ = r✝ /ₒ s✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: case pos
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
hy0 : dy = 0
⊢ nx / dx + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

pp: case neg
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
hy0 : ¬dy = 0
⊢ nx / dx + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

Tactic:
· rwa [hy0, div_zero, add_zero]

Goal state after:
case neg
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : ¬dx = 0
hy0 : ¬dy = 0
⊢ nx / dx + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ ra * ↑s₂ ∈ S

Tactic:
rw [← ha]

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₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑(sa * s₁) = ra * ↑s₂
⊢ ↑(sa * s₁) ∈ 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
h : 0 ∈ S
a b : N
⊢ a = b

Tactic:
← f.mk'_sec a,

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
h : 0 ∈ S
a b : N
⊢ f.mk' (f.sec a).1 (f.sec a).2 = b
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
s : ↥S
⊢ f m = 0 ↔ ∃ s, ↑s * m = 0

Tactic:
map_eq_zero_iff

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
s : ↥S
⊢ (∃ s, ↑s * m = 0) ↔ ∃ s, ↑s * m = 0
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
h0 : f (ms.1 * m) = 0
eq : n * f ↑ms.2 = f ms.1
⊢ n = 0

Tactic:
map_eq_zero_iff

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
h0 : ∃ s, ↑s * (ms.1 * m) = 0
eq : n * f ↑ms.2 = f ms.1
⊢ n = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case zero
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f : M₁ →ₗ[R] M₁
⊢ (toMatrix v₁ v₁) f ^ 0 = (toMatrix v₁ v₁) (f ^ 0)

Tactic:
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
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
⊢ f ms.1 = 0

Tactic:
map_eq_zero_iff

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
⊢ ∃ s, ↑s * ms.1 = 0
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: 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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ ↑1 * 0 = 0 * ↑s

Tactic:
simp

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

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r : X
s : ↥S
⊢ 0 • r /ₒ (1 * 1) = 0

Tactic:
simp

Goal state after: