awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : length R R = ⊤
⊢ (ENat.card.{u_2} (Free.ChooseBasisIndex R M) = 0) =
    Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (0 : ℕ∞)

Tactic:
simp [ENat.card_eq_zero_iff_empty, rank_pos_of_free.ne']

Premises used: ENat.card_eq_zero_iff_empty, Module.rank_pos_of_free, LT.lt.ne'
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : ¬length R R = ⊤
⊢ IsNoetherian R R ∧ IsArtinian R R

Tactic:
rw [← ne_eq, Module.length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian] at H

Premises used: Module.length_ne_top_iff, ne_eq, isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : IsNoetherian R R ∧ IsArtinian R R
⊢ IsNoetherian R R

Tactic:
cases H
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : IsNoetherian R R ∧ IsArtinian R R
left : IsNoetherian R R
⊢ IsArtinian R R

Tactic:
cases H
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b_1 : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
left : IsNoetherian R R
right : IsArtinian R R
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
neg :
  length R (Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
neg₁ :
  ENat.card.{u_2} (Free.ChooseBasisIndex R M) * length R R =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
neg₂ :
  ENat.card.{u_2} (Free.ChooseBasisIndex R M) * length R R =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (Free.ChooseBasisIndex R M)) : ℕ∞)
      (length R R)
neg₃ neg₄ :
  HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (Free.ChooseBasisIndex R M)) : ℕ∞)
      (length R R) =
    HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Cardinal.mk (Free.ChooseBasisIndex R M)) : ℕ∞)
      (length R R)
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)

Tactic:
rw [b.repr.length_eq, Module.length_finsupp, Free.rank_eq_card_chooseBasisIndex, ENat.card]

Premises used: LinearEquiv.length_eq, Module.Basis.repr, Module.length_finsupp, ENat.card, Module.Free.rank_eq_card_chooseBasisIndex
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
inst_5 : Module.Finite R M
rw :
  HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R) =
    (↑(finrank R M) : ℕ∞) * length R R
rw₁ rw₂ : (↑(finrank R M) : ℕ∞) * length R R = (↑(finrank R M) : ℕ∞) * length R R
⊢ length R M = (↑(finrank R M) : ℕ∞) * length R R

Tactic:
rw [length_of_free, Cardinal.toENat_eq_natCast.mpr (finrank_eq_rank _ _).symm]

Premises used: Iff.mpr, Module.length_of_free, Module.finrank_eq_rank, Cardinal.toENat_eq_natCast, Eq.symm
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑1 : WithBot ℕ∞) ↔ IsSimpleModule R M
rw₂ : Order.krullDim.{u_2} (Submodule R M) = 1 ↔ IsSimpleModule R M
rw₃ : IsSimpleOrder.{u_2} (Submodule R M) ↔ IsSimpleModule R M
rw₄ rw₅ : IsSimpleOrder.{u_2} (Submodule R M) ↔ IsSimpleOrder.{u_2} (Submodule R M)
⊢ length R M = 1 ↔ IsSimpleModule R M

Tactic:
rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_one,
    Order.krullDim_eq_one_iff_of_boundedOrder, isSimpleModule_iff]

Premises used: Module.coe_length, isSimpleModule_iff, WithBot.coe_one, WithBot.coe_inj, Order.krullDim_eq_one_iff_of_boundedOrder
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSimpleModule R M
⊢ length R M = 1

Tactic:
Module.length_eq_one_iff.mpr ‹_›

Premises used: Iff.mpr, Module.length_eq_one_iff
-- Module: Mathlib.RingTheory.Length
Goal:
K : Type u_5
M : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
⊢ length K M = (Cardinal.toENat : (a : Cardinal.{u_6}) → ℕ∞) (Module.rank K M)

Tactic:
simp [Module.length_of_free]

Premises used: Module.length_of_free
-- Module: Mathlib.RingTheory.Length
Goal:
K : Type u_5
M : Type u_6
inst : DivisionRing K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
⊢ length K M = (↑(finrank K M) : ℕ∞)

Tactic:
simp [Module.length_of_free]

Premises used: Module.length_of_free
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_5
inst_3 : Ring A
inst_4 : SMul A R
inst_5 : Module A M
inst_6 : IsScalarTower A R M
p : Submodule R M
rw : Order.krullDim.{u_2} (Submodule R ↥p) ≤ Order.krullDim.{u_2} (Submodule A ↥(restrictScalars A p))
⊢ Module.length.{u_1, u_2} R ↥p ≤ Module.length.{u_5, u_2} A ↥(restrictScalars A p)

Tactic:
rw [← WithBot.coe_le_coe, Module.coe_length, Module.coe_length]

Premises used: Module.coe_length, WithBot.coe_le_coe
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_5
inst_3 : Ring A
inst_4 : SMul A R
inst_5 : Module A M
inst_6 : IsScalarTower A R M
p : Submodule R M
⊢ Order.krullDim.{u_2} (Submodule R ↥p) ≤ Order.krullDim.{u_2} (Submodule A ↥(restrictScalars A p))

Tactic:
Order.krullDim_le_of_orderEmbedding (restrictScalarsEmbedding A R p)

Premises used: Order.krullDim_le_of_orderEmbedding, Membership.mem, Subtype, Submodule.restrictScalarsEmbedding
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_5
inst_3 : Ring A
inst_4 : SMul A R
inst_5 : Module A M
inst_6 : IsScalarTower A R M
p : Submodule R M
⊢ Order.krullDim.{u_2} (Submodule R ↥p) ≤ Order.krullDim.{u_2} (Submodule A ↥(restrictScalars A p))

Tactic:
exact Order.krullDim_le_of_orderEmbedding (restrictScalarsEmbedding A R p)

Premises used: Order.krullDim_le_of_orderEmbedding, Membership.mem, Subtype, Submodule.restrictScalarsEmbedding
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
rw : Order.coheight p < Order.coheight.{u_2} (α := Submodule R M) ⊥
⊢ Module.length.{u_1, u_2} R (M ⧸ p) < Module.length R M

Tactic:
rw [Module.length_quotient, Module.length, WithBot.lt_unbot_iff, ← Order.coheight_bot_eq_krullDim,
    WithBot.coe_lt_coe]

Premises used: WithBot.lt_unbot_iff, Module.length, WithBot.coe_lt_coe, Order.coheight_bot_eq_krullDim, Module.length_quotient
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
⊢ Order.coheight p < Order.coheight.{u_2} (α := Submodule R M) ⊥

Tactic:
Order.coheight_strictAnti (bot_lt_iff_ne_bot.mpr h) (Order.coheight_lt_top p)

Premises used: Iff.mpr, bot_lt_iff_ne_bot, Order.coheight_lt_top, Order.coheight_strictAnti
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
p : Submodule R M
h : p ≠ ⊥
⊢ Order.coheight p < Order.coheight.{u_2} (α := Submodule R M) ⊥

Tactic:
exact Order.coheight_strictAnti (bot_lt_iff_ne_bot.mpr h) (Order.coheight_lt_top p)

Premises used: Iff.mpr, bot_lt_iff_ne_bot, Order.coheight_lt_top, Order.coheight_strictAnti
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A B : Subalgebra R S
⊢ A.LinearDisjoint B ↔
    Submodule.LinearDisjoint.{u, v} (R := R) (S := S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
      ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Subsingleton R
⊢ A.LinearDisjoint B

Tactic:
Submodule.LinearDisjoint.of_subsingleton

Premises used: Submodule.LinearDisjoint.of_subsingleton
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Subsingleton S
⊢ A.LinearDisjoint B

Tactic:
Submodule.LinearDisjoint.of_subsingleton_top

Premises used: Submodule.LinearDisjoint.of_subsingleton_top
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hc : ∀ (a : ↥A) (b : ↥B), Commute (↑a : S) (↑b : S)
⊢ B.LinearDisjoint A

Tactic:
Submodule.LinearDisjoint.symm_of_commute H hc

Premises used: Submodule.LinearDisjoint.symm_of_commute
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A B : Subalgebra R S
hc : ∀ (a : ↥A) (b : ↥B), Commute (↑a : S) (↑b : S)
⊢ A.LinearDisjoint B ↔ B.LinearDisjoint A

Tactic:
⟨fun H ↦ H.symm_of_commute hc, fun H ↦ H.symm_of_commute fun _ _ ↦ (hc _ _).symm⟩

Premises used: Commute.symm, Subalgebra.LinearDisjoint.symm_of_commute, Iff.intro
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective.{v + 1, w + 1} (α := S) (β := T) (⇑f : (a : S) → T)
⊢ (Subalgebra.map f A).LinearDisjoint (Subalgebra.map f B)

Tactic:
Submodule.LinearDisjoint.map H f hf

Premises used: Set.Mem, setOf, Submodule.LinearDisjoint.map, Set.image, Submodule.map
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
B : Subalgebra R S
rw : Submodule.LinearDisjoint.{u, v} (R := R) (S := S) 1 ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)
⊢ Subalgebra.LinearDisjoint ⊥ B

Tactic:
rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]

Premises used: Algebra.toSubmodule_bot, Subalgebra.LinearDisjoint
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
B : Subalgebra R S
⊢ Submodule.LinearDisjoint.{u, v} (R := R) (S := S) 1 ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)

Tactic:
Submodule.LinearDisjoint.one_left _

Premises used: Submodule.LinearDisjoint.one_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
B : Subalgebra R S
⊢ Submodule.LinearDisjoint.{u, v} (R := R) (S := S) 1 ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)

Tactic:
exact Submodule.LinearDisjoint.one_left _

Premises used: Submodule.LinearDisjoint.one_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
rw : Submodule.LinearDisjoint.{u, v} (R := R) (S := S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) 1
⊢ A.LinearDisjoint ⊥

Tactic:
rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]

Premises used: Algebra.toSubmodule_bot, Subalgebra.LinearDisjoint
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
⊢ Submodule.LinearDisjoint.{u, v} (R := R) (S := S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) 1

Tactic:
Submodule.LinearDisjoint.one_right _

Premises used: Submodule.LinearDisjoint.one_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
A : Subalgebra R S
⊢ Submodule.LinearDisjoint.{u, v} (R := R) (S := S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) 1

Tactic:
exact Submodule.LinearDisjoint.one_right _

Premises used: Submodule.LinearDisjoint.one_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
B : Type w
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
rw :
  Function.Injective (α :=
    ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
            (AlgHom.range Algebra.TensorProduct.includeLeft) :
          Submodule R (A ⊗[R] B)) ⊗[R]
      ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
            (AlgHom.range Algebra.TensorProduct.includeRight) :
          Submodule R (A ⊗[R] B)))
    (β := A ⊗[R] B)
    (⇑(Submodule.mulMap
          ((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
            (AlgHom.range Algebra.TensorProduct.includeLeft))
          ((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
            (AlgHom.range Algebra.TensorProduct.includeRight))) :
      (a :
          ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
                Algebra.TensorProduct.includeLeft.range) ⊗[R]
            ↥((toSubmodule : (a : Subalgebra R (A ⊗[R] B)) → Submodule R (A ⊗[R] B))
                Algebra.TensorProduct.includeRight.range)) →
        A ⊗[R] B)
⊢ Subalgebra.LinearDisjoint (R := R) (S := A ⊗[R] B) (AlgHom.range Algebra.TensorProduct.includeLeft)
    (AlgHom.range Algebra.TensorProduct.includeRight)

Tactic:
rw [Subalgebra.LinearDisjoint, Submodule.linearDisjoint_iff]

Premises used: Submodule.linearDisjoint_iff, Subalgebra.LinearDisjoint
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
B : Type w
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Injective (α :=
    ↥(LinearMap.range (AlgHom.toLinearMap Algebra.TensorProduct.includeLeft)) ⊗[R]
      ↥(LinearMap.range (AlgHom.toLinearMap Algebra.TensorProduct.includeRight)))
    (β := A ⊗[R] B)
    (⇑(↑(LinearEquiv.symm (Algebra.TensorProduct.linearEquivIncludeRange R A B)) :
          ↥Algebra.TensorProduct.includeLeft.range ⊗[R] ↥Algebra.TensorProduct.includeRight.range →ₗ[R] A ⊗[R] B) :
      (a :
          ↥Algebra.TensorProduct.includeLeft.toLinearMap.range ⊗[R]
            ↥Algebra.TensorProduct.includeRight.toLinearMap.range) →
        A ⊗[R] B)

Tactic:
LinearEquiv.injective _

Premises used: LinearEquiv.injective
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
inst : CommSemiring R
A : Type v
inst_1 : Semiring A
B : Type w
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Function.Injective (α :=
    ↥(LinearMap.range (AlgHom.toLinearMap Algebra.TensorProduct.includeLeft)) ⊗[R]
      ↥(LinearMap.range (AlgHom.toLinearMap Algebra.TensorProduct.includeRight)))
    (β := A ⊗[R] B)
    (⇑(↑(LinearEquiv.symm (Algebra.TensorProduct.linearEquivIncludeRange R A B)) :
          ↥Algebra.TensorProduct.includeLeft.range ⊗[R] ↥Algebra.TensorProduct.includeRight.range →ₗ[R] A ⊗[R] B) :
      (a :
          ↥Algebra.TensorProduct.includeLeft.toLinearMap.range ⊗[R]
            ↥Algebra.TensorProduct.includeRight.toLinearMap.range) →
        A ⊗[R] B)

Tactic:
exact LinearEquiv.injective _

Premises used: LinearEquiv.injective
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
⊢ B.LinearDisjoint A

Tactic:
H.symm_of_commute fun _ _ ↦ mul_comm _ _

Premises used: Subalgebra.LinearDisjoint.symm_of_commute, mul_comm, Subtype.val
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
⊢ A.LinearDisjoint B ↔ B.LinearDisjoint A

Tactic:
⟨LinearDisjoint.symm, LinearDisjoint.symm⟩

Premises used: Subalgebra.LinearDisjoint.symm, Iff.intro
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
rw :
  Function.Injective.{v + 1, v + 1} (α :=
      ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
        ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
      (β := S)
      (⇑(Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) :
        (a :
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
          S) ↔
    Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)
⊢ A.LinearDisjoint B ↔ Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)

Tactic:
rw [linearDisjoint_iff, Submodule.linearDisjoint_iff]

Premises used: Submodule.linearDisjoint_iff, Subalgebra.linearDisjoint_iff
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
⊢ Function.Injective.{v + 1, v + 1} (α :=
      ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
        ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
      (β := S)
      (⇑(Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) :
        (a :
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
          S) ↔
    Function.Injective (α := ↥A ⊗[R] ↥B) (β := S) (⇑(A.mulMap B) : (a : ↥A ⊗[R] ↥B) → S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
a : ↥A
b : ↥B
⊢ (↑((H.mulMap : (a : ↥A ⊗[R] ↥B) → ↥(A ⊔ B)) (a ⊗ₜ[R] b)) : S) = (↑a : S) * (↑b : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
a :
  Eq (α := Subalgebra R S)
    (restrictScalars R (S := ↥A)
      (AlgHom.range (A := ↥A ⊗[R] ↥B)
        (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)))
    (restrictScalars R (S := ↥A) ⊤)
⊢ Eq (α := Subalgebra (↥A) S)
    (AlgHom.range (A := ↥A ⊗[R] ↥B)
      (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S))
    ⊤

Tactic:
apply Subalgebra.restrictScalars_injective R

Premises used: Subalgebra.restrictScalars_injective
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
a :
  restrictScalars R (S := ↥A)
      (AlgHom.range (A := ↥A ⊗[R] ↥B)
        (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)) =
    A ⊔ B
⊢ Eq (α := Subalgebra R S)
    (restrictScalars R (S := ↥A)
      (AlgHom.range (A := ↥A ⊗[R] ↥B)
        (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)))
    (restrictScalars R (S := ↥A) ⊤)

Tactic:
rw [restrictScalars_top, ← H']

Premises used: Subalgebra.restrictScalars_top
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ restrictScalars R (S := ↥A)
      (AlgHom.range (A := ↥A ⊗[R] ↥B)
        (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)) =
    A ⊔ B

Tactic:
mulMap_range A B

Premises used: Set.Mem, Subalgebra.mulMap_range, Subsemiring.copy, Subalgebra.restrictScalars, AlgHom.range, RingHom.rangeS
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ restrictScalars R (S := ↥A)
      (AlgHom.range (A := ↥A ⊗[R] ↥B)
        (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val : ↥A ⊗[R] ↥B →ₐ[↥A] S)) =
    A ⊔ B

Tactic:
exact mulMap_range A B

Premises used: Subalgebra.mulMap_range
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
a : ↥A
b : ↥B
⊢ (H.mulMapLeftOfSupEqTop H' : (a : ↥A ⊗[R] ↥B) → S) (a ⊗ₜ[R] b) = (↑a : S) * (↑b : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis.{u_1, u, v} ι R ↥B
i : ι
⊢ Eq.{v + 1} (α := S) ((H.basisOfBasisRight H' b : (a : ι) → S) i : S)
    ((algebraMap (↥B) S : (a : ↥B) → S) ((b : (a : ι) → ↥B) i : ↥B) : S)

Tactic:
simp [basisOfBasisRight]

Premises used: Subalgebra.LinearDisjoint.basisOfBasisRight
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
x : ↥B
⊢ (↑x : S) = (H.mulMapLeftOfSupEqTop H' : (a : ↥A ⊗[R] ↥B) → S) (1 ⊗ₜ[R] x)

Tactic:
simp
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
ι : Type u_1
b : Basis.{u_1, u, v} ι R ↥B
x : ↥B
i : ι
⊢ Eq (α := S)
    ((algebraMap (↥A) S : (a : ↥A) → S)
        (((((H.basisOfBasisRight H' b).repr : (a : S) → ι →₀ ↥A) (↑x : S) : Finsupp.{u_1, v} ι ↥A) : (a : ι) → ↥A) i :
          ↥A) :
      S)
    ((algebraMap R S : (a : R) → S) ((((b.repr : (a : ↥B) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) : S)

Tactic:
simp [basisOfBasisRight, Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, Subalgebra.LinearDisjoint.basisOfBasisRight