mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
⊢ ∀ {x y : R}, c x y → d x y

Tactic:
_

Goal state after:
case mp
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
x✝ : R
⊢ ∀ {y : R}, c x✝ y → d x✝ y
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
x✝ : R
⊢ ∀ {y : R}, c x✝ y → d x✝ y

Tactic:
_

Goal state after:
case mp
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
x✝ y✝ : R
⊢ c x✝ y✝ → d x✝ y✝
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h : ∀ {x y : R}, c x y → d x y
⊢ ∀ {x y : Rᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y

Tactic:
_

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h : ∀ {x y : R}, c x y → d x y
x✝ : Rᵐᵒᵖ
⊢ ∀ {y : Rᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x✝ y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x✝ y
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h : ∀ {x y : R}, c x y → d x y
x✝ : Rᵐᵒᵖ
⊢ ∀ {y : Rᵐᵒᵖ},
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x✝ y →
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x✝ y

Tactic:
_

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h : ∀ {x y : R}, c x y → d x y
x✝ y✝ : Rᵐᵒᵖ
⊢ ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x✝ y✝ →
    ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x✝ y✝
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Free R M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Free R M'
inst✝² : StrongRankCondition R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R M'
⊢ finrank R M ≤ finrank R M' ↔ ∃ f, Injective ⇑f

Tactic:
by
  simp [← lift_rank_le_iff_exists_linearMap, ← finrank_eq_rank]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : x ∈ ↑I
⊢ x ∈ ↑J

Tactic:
rw [SetLike.mem_coe, mem_iff] at hx ⊢; exact h hx

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

Goal state before:
pp: R : Type u
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
H : ∀ {S : Type u} [inst : NonAssocSemiring S] (f : R →+* S), Function.Injective ⇑f ∨ Subsingleton S
x✝² : Type u
x✝¹ : NonAssocSemiring x✝²
x✝ : Nontrivial x✝²
f : R →+* x✝²
⊢ ¬Subsingleton x✝²

Tactic:
simpa [not_subsingleton_iff_nontrivial]

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ : Subalgebra R A
S : Subalgebra R R
x✝ : R
⊢ x✝ ∈ S → x✝ ∈ default

Tactic:
_

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ : Subalgebra R A
S : Subalgebra R R
x✝ : R
a✝ : x✝ ∈ S
⊢ x✝ ∈ default
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
S : Subalgebra R A
inst✝³ : CommSemiring R'
inst✝² : SMul R' R
inst✝¹ : Algebra R' A
inst✝ : IsScalarTower R' R A
x : R'
⊢ (algebraMap R' A) x ∈ S

Tactic:
rw [Algebra.algebraMap_eq_smul_one, ← smul_one_smul R x (1 : A), ←
      Algebra.algebraMap_eq_smul_one]
    exact algebraMap_mem S _

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

Goal state before:
pp: case e'_2
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑x = ↑(x • 1)

Tactic:
exact (mul_one _).symm

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

Goal state before:
pp: case e'_3
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑y = ↑(y • 1)

Tactic:
exact (mul_one _).symm

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

Goal state before:
pp: case tmul
R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)) =
    (rTensor M₂' (lof R ι₁ M₁ i)) (x ⊗ₜ[R] y)

Tactic:
| tmul x y =>

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₂ : Type v₂
inst✝⁶ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
this :
  ↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m =
    (mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i
⊢ ((directSumRight R S M₁' M₂) (m ⊗ₜ[R] n)) i = m ⊗ₜ[R] n i

Tactic:
simpa using! LinearMap.congr_fun this n

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
this : b * a = 0
⊢ Commute a b

Tactic:
grind [commute_iff_eq]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
⊢ (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c)

Tactic:
ext
  rw [updateCol_apply, map_apply, map_apply, updateCol_apply]
  exact apply_ite f _ _ _

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ Mᵀ.updateRow j c i✝ j✝ = (M.updateCol j c)ᵀ i✝ j✝

Tactic:
transpose_apply,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ Mᵀ.updateRow j c i✝ j✝ = M.updateCol j c j✝ i✝
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ Mᵀ.updateCol i b i✝ j✝ = (M.updateRow i b)ᵀ i✝ j✝

Tactic:
transpose_apply,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ Mᵀ.updateCol i b i✝ j✝ = M.updateRow i b j✝ i✝
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
ι : Sort u_1
inst✝ : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
by
  apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
i' : n
⊢ i' ∈ Finset.univ → i' ≠ i → M j i' * (Finsupp.single i 1) i' = 0

Tactic:
_

Goal state after:
case h₀
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : Fintype m
M : Matrix m n R
i : n
j : m
_hj : j ∈ Finset.univ
i' : n
a✝ : i' ∈ Finset.univ
⊢ i' ≠ i → M j i' * (Finsupp.single i 1) i' = 0
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
inst : Module ℤ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Tactic:
exact congr($(AddCommGroup.uniqueIntModule.2 inst).smul n x)

Goal state after:
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
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Finite ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
i : ι
⊢ smithNormalFormCoeffs b h i ≠ 0

Tactic:
intro hi

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
N : Submodule R M
inst✝ : Finite ι
b : Basis ι R M
h : finrank R ↥N = finrank R M
i : ι
hi : smithNormalFormCoeffs b h i = 0
⊢ False
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
⊢ smithCoeffs b I hI i ≠ 0

Tactic:
intro hi

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
inst✝⁴ : IsPrincipalIdealRing R
S : Type u_4
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Finite ι
b : Basis ι R S
I : Ideal S
hI : I ≠ ⊥
i : ι
hi : smithCoeffs b I hI i = 0
⊢ False
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
s : Set A
t : Set B
hS : adjoin R s = ⊤
⊢ Subalgebra.restrictScalars R (adjoin A t) = adjoin R (⇑(algebraMap A B) '' s ∪ t)

Tactic:
by
  have := congr_arg (Subalgebra.map (IsScalarTower.toAlgHom R A B)) hS
  rw [Algebra.map_top, AlgHom.map_adjoin, IsScalarTower.coe_toAlgHom'] at this
  rw [adjoin_union_eq_adjoin_adjoin, this, ← IsScalarTower.adjoin_range_toAlgHom]

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

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
x : A
y : M
⊢ x ⊗ₜ[R] y ∈ Submodule.span A ↑(Finset.image (⇑((TensorProduct.mk R A M) 1)) s)

Tactic:
| tmul x y =>

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

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Module.Finite R A
h : Algebra.IsEpi R A
R' : Submodule R A := (Algebra.linearMap R A).range
h✝ : Nontrivial (A ⧸ R')
x y : A ⧸ R'
⊢ x ⊗ₜ[R] y = 0

Tactic:
| tmul x y =>

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

Goal state before:
pp: case tmul.tmul
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : Module R B
inst✝⁵ : SMulCommClass R B B
inst✝⁴ : IsScalarTower R B B
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : IsScalarTower S A A
inst✝ : SMulCommClass R S A
r : S
a : A
b : B
a' : A
b' : B
⊢ r • a' ⊗ₜ[R] b' * a ⊗ₜ[R] b = r • (a' * a) ⊗ₜ[R] (b' * b)

Tactic:
rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]

Goal state after:
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
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑(IsUnit.unit hb) - ↑(IsUnit.unit ha) = a - b

Tactic:
hb.unit_spec,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
ha : r ∈ resolventSet R a
hb : r ∈ resolventSet R b
⊢ ↑ₐ r - b - ↑(IsUnit.unit ha) = a - b
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 : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (1 - r⁻¹⁻¹ • ↑a⁻¹)

Tactic:
inv_inv,

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (1 - r • ↑a⁻¹)
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case tmul
R : Type uR
A : Type uA
B : Type uB
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
C : Type u_3
inst✝ : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom
x : A
y : B
⊢ f (x ⊗ₜ[R] y) = g (x ⊗ₜ[R] y)

Tactic:
| tmul x y =>

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

Goal state before:
pp: case tmul
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
⊢ x ⊗ₜ[R] y ∈ Subring.closure (Set.range ⇑includeLeft ∪ Set.range ⇑includeRight)

Tactic:
| tmul x y =>

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

Goal state before:
pp: case refine_1.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
⊢ (0 * z) • m = 0 • z • m → (0 * w) • m = 0 • w • m → (0 * (z + w)) • m = 0 • (z + w) • m

Tactic:
_

Goal state after:
case refine_1.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
a✝ : (0 * z) • m = 0 • z • m
⊢ (0 * w) • m = 0 • w • m → (0 * (z + w)) • m = 0 • (z + w) • m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_1.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
a✝ : (0 * z) • m = 0 • z • m
⊢ (0 * w) • m = 0 • w • m → (0 * (z + w)) • m = 0 • (z + w) • m

Tactic:
_

Goal state after:
case refine_1.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
a✝¹ : (0 * z) • m = 0 • z • m
a✝ : (0 * w) • m = 0 • w • m
⊢ (0 * (z + w)) • m = 0 • (z + w) • m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
⊢ (z * 0) • m = z • 0 • m → (w * 0) • m = w • 0 • m → ((z + w) * 0) • m = (z + w) • 0 • m

Tactic:
_

Goal state after:
case refine_3.refine_1
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
a✝ : (z * 0) • m = z • 0 • m
⊢ (w * 0) • m = w • 0 • m → ((z + w) * 0) • m = (z + w) • 0 • m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
a✝ : (z * 0) • m = z • 0 • m
⊢ (w * 0) • m = w • 0 • m → ((z + w) * 0) • m = (z + w) • 0 • m

Tactic:
_

Goal state after:
case refine_3.refine_1
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
z w : A ⊗[R] B
a✝¹ : (z * 0) • m = z • 0 • m
a✝ : (w * 0) • m = w • 0 • m
⊢ ((z + w) * 0) • m = (z + w) • 0 • m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
⊢ (∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m) →
    (∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m) →
      ∀ (x y : A ⊗[R] B),
        (x * (u + v)) • m = x • (u + v) • m →
          (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m

Tactic:
_

Goal state after:
case refine_3.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
a✝ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
⊢ (∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m) →
    ∀ (x y : A ⊗[R] B),
      (x * (u + v)) • m = x • (u + v) • m →
        (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_3.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
a✝ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
⊢ (∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m) →
    ∀ (x y : A ⊗[R] B),
      (x * (u + v)) • m = x • (u + v) • m →
        (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m

Tactic:
_

Goal state after:
case refine_3.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
a✝¹ : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
a✝ : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
⊢ ∀ (x y : A ⊗[R] B),
    (x * (u + v)) • m = x • (u + v) • m →
      (y * (u + v)) • m = y • (u + v) • m → ((x + y) * (u + v)) • m = (x + y) • (u + v) • m
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
⊢ (includeLeft.comp f).range ⊔ (includeRight.comp g).range ≤ (map f g).range

Tactic:
rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]
    exact sup_le (AlgHom.range_comp_le_range _ _) (AlgHom.range_comp_le_range _ _)

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ (lmul' R).comp (map f g) = lift f g ⋯

Tactic:
by ext <;> rfl

Goal state after: