mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ[R] n₁ + m₂ ⊗ₜ[R] n₂ = m ⊗ₜ[R] n
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass R R ↥x
c : R →₀ ↥x
hc1 : ↑c.support ⊆ t
hm : ↑(c.sum fun r m ↦ r • m) ∈ t • x
⊢ r • ∑ i ∈ c.support, ↑(i • c i) ∈ (s * t) • x

Tactic:
]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass R R ↥x
c : R →₀ ↥x
hc1 : ↑c.support ⊆ t
hm : ↑(c.sum fun r m ↦ r • m) ∈ t • x
⊢ r • ∑ i ∈ c.support, ↑(i • c i) ∈ (s * t) • x
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
x : Submodule R M
w✝ : M
h : w✝ ∈ x
⊢ w✝ ∈ x

Tactic:
]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
x : Submodule R M
w✝ : M
h : w✝ ∈ x
⊢ w✝ ∈ x
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
m : M
hr : r ∈ s
hm : ∃ y_1 ∈ x, ∃ z ∈ y, y_1 + z = m
⊢ r • m ∈ s • x + s • y

Tactic:
]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
m : M
hr : r ∈ s
hm : ∃ y_1 ∈ x, ∃ z ∈ y, y_1 + z = m
⊢ r • m ∈ s • x + s • y
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n + l

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n + l
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n✝ m : ℕ
hnm : (fun n ↦ r ^ n) n✝ = (fun n ↦ r ^ n) m
n l : ℕ
h₁ : n ≤ n + l
h₂ : l = 0
⊢ n = n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : Finite R
h : IsLeftRegular r
⊢ Function.Injective fun x ↦ r * x

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : Finite R
h : IsLeftRegular r
⊢ Function.Injective fun x ↦ r * x
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : Finite R
h : IsRightRegular r
⊢ Function.Injective fun x ↦ x * r

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : Finite R
h : IsRightRegular r
⊢ Function.Injective fun x ↦ x * r
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
hr : r ∈ s
a : M
ha : a ∈ x
b : M
hb : b ∈ y
⊢ ∃ y_1 ∈ s • x, ∃ z ∈ s • y, y_1 + z = r • a + r • b

Tactic:
]

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s : Set R
x y : Submodule R M
r : R
hr : r ∈ s
a : M
ha : a ∈ x
b : M
hb : b ∈ y
⊢ ∃ y_1 ∈ s • x, ∃ z ∈ s • y, y_1 + z = r • a + r • b
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
a : R
inst✝ : Finite R
⊢ IsUnit a ↔ IsUnit a

Tactic:
]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
M₂ : Type u_12
N₂ : Type u_14
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R₂ M₂
inst✝ : Module R₂ N₂
r : R₂
f : M →ₛₗ[σ₁₂] M₂
g : N →ₛₗ[σ₁₂] N₂
⊢ map (r • f) g = r • map f g

Tactic:
by
  ext
  simp only [smul_tmul, compr₂ₛₗ_apply, mk_apply, map_tmul, smul_apply, tmul_smul]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange ((multiplesHom R) 1)

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange ((multiplesHom R) 1)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n = 0
⊢ m • n = 0

Tactic:
]

Goal state after:
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n = 0
⊢ m • n = 0
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + b = b
hbc : b + c = c
⊢ b + c = b + c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
hab : a + b = b
hba : b + a = a
⊢ a + b = b

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
hab : a + b = b
hba : b + a = a
⊢ a + b = b
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
⊢ a + b = a + b

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
⊢ (⇑(lTensor M g) ∘ ⇑(lTensor M f)) x = (lTensor M g) ((lTensor M f) x)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
⊢ (⇑(lTensor M g) ∘ ⇑(lTensor M f)) x = (lTensor M g) ((lTensor M f) x)
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + c = c
hbc : b + c = c
⊢ a + c = c

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b c : α
hab : a + c = c
hbc : b + c = c
⊢ a + c = c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : 1 ≤ n
⊢ ↑n = 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : 1 ≤ n
⊢ ↑n = 1
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: case succ
α : Type u_1
inst✝ : IdemSemiring α
n x : ℕ
hmn✝ : 1 ≤ x
hx : ↑x = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
x✝ : n + 2 ≠ 0
a : α
⊢ a = a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b : α
hbc : a ≤ b
c : α
⊢ b ⊔ c ≤ b ⊔ c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ b + a = b + a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ b + a + a = b + a

Tactic:
rw [add_assoc, add_idem]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c a b : α
⊢ a + b = a + b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ a * c = (fun x1 x2 ↦ x1 * x2) a c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ c * a = swap (fun x1 x2 ↦ x1 * x2) a c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : c * a ≤ c
⊢ c ≤ c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
⊢ c ≤ c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a ≤ 1
⊢ a ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a ≤ 1
⊢ a ≤ 1
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ (⇑(rTensor M g) ∘ ⇑(rTensor M f)) x = (rTensor M g) ((rTensor M f) x)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : N ⊗[R] M
⊢ (⇑(rTensor M g) ∘ ⇑(rTensor M f)) x = (rTensor M g) ((rTensor M f) x)
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a∗ = a
⊢ a∗ = a∗

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
n : ℕ
⊢ a∗ ≤ a∗

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a * a∗ ≤ a∗

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a * a∗ ≤ a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ * 1 ≤ 1 + a * a∗

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ * 1 ≤ 1 + a * a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a∗ * a ≤ a∗

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a∗ * a ≤ a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ 1 * a∗ ≤ 1 + a∗ * a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ 1 * a∗ ≤ 1 + a∗ * a
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ x = x

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : N ⊗[R] M
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹¹ : IdemSemiring α
inst✝¹⁰ : LE β
inst✝⁹ : LT β
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Max β
inst✝ : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f a ⊔ f b = f a ⊔ f b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • x✝ + m • y✝ ∈ M • N ⊔ M • P

Tactic:
]

Goal state after:
case refine_3
R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
M : AddSubmonoid R
N P : AddSubmonoid A
m : R
hm : m ∈ M
np : A
hnp : np ∈ N ⊔ P
x✝ y✝ : A
hx✝ : x✝ ∈ closure (↑N ∪ ↑P)
hy✝ : y✝ ∈ closure (↑N ∪ ↑P)
h1 : m • x✝ ∈ M • N ⊔ M • P
h2 : m • y✝ ∈ M • N ⊔ M • P
⊢ m • x✝ + m • y✝ ∈ M • N ⊔ M • P
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : AddMonoid R
inst✝¹ : AddMonoid A
inst✝ : DistribSMul R A
ι : Sort u_4
T : AddSubmonoid R
S : ι → AddSubmonoid A
t : R
ht : t ∈ T
s : A
hs : s ∈ ⨆ i, S i
x y : A
⊢ t • x ∈ ⨆ i, T • S i → t • y ∈ ⨆ i, T • S i → t • (x + y) ∈ ⨆ i, T • S i

Tactic:
simp_rw [smul_add]; apply add_mem

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a ∈ comap (AddMonoidHom.mulRight b) (closure (S * T))

Tactic:
]

Goal state after:
case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
a : R
ha : a ∈ closure S
b : R
hb : b ∈ closure T
⊢ a ∈ comap (AddMonoidHom.mulRight b) (closure (S * T))
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
n : ℕ
h : map f id ^ n = map (f ^ n) id
⊢ rTensor N f ^ n = rTensor N (f ^ n)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] M
n : ℕ
h : map f id ^ n = map (f ^ n) id
⊢ rTensor N f ^ n = rTensor N (f ^ n)
Module: Mathlib.Data.Set.Semiring

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)

Tactic:
]

Goal state after:
case a
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S T : Set R
⊢ S * T ⊆ ↑(closure S * closure T)
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map id (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map id (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = M * N

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ m * n = 0

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ m * n = 0
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ m * n = 0

Tactic:
hm,

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ 0 * n = 0
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ 1 ≤ (f a)∗

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ 1 ≤ (f a)∗
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P

Tactic:
]

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ m * p + n * p ∈ M * P ⊔ N * P
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
y : N ⊗[R] M
⊢ y = y

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N ≃ₗ[R] N
n : ℕ
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
by
  simpa only [one_pow] using! TensorProduct.congr_pow (1 : M ≃ₗ[R] M) f n

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ f a * (f a)∗ ≤ (f a)∗

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a : β
⊢ f a * (f a)∗ ≤ (f a)∗