awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis.{u_1, u, v} ι R ↥B
x : ↥B
a :
  ∀ (i j : ι),
    Eq.{v + 1} (α := S)
      (↑((Algebra.leftMulMatrix (H.basisOfBasisRight H' b) : (a : S) → Matrix ι ι ↥A)
            ((algebraMap (↥B) S : (a : ↥B) → S) x) i j) :
        S)
      (↑((RingHom.mapMatrix (algebraMap R ↥A) : (a : Matrix ι ι R) → Matrix ι ι ↥A)
            ((Algebra.leftMulMatrix b : (a : ↥B) → Matrix ι ι R) x) i j) :
        S)
⊢ Eq (α := Matrix.{u_1, u_1, v} ι ι ↥A)
    ((Algebra.leftMulMatrix (H.basisOfBasisRight H' b) : (a : S) → Matrix ι ι ↥A)
        ((algebraMap (↥B) S : (a : ↥B) → S) x) :
      Matrix.{u_1, u_1, v} ι ι ↥A)
    ((RingHom.mapMatrix (algebraMap R ↥A) : (a : Matrix ι ι R) → Matrix ι ι ↥A)
        ((Algebra.leftMulMatrix b : (a : ↥B) → Matrix ι ι R) x) :
      Matrix.{u_1, u_1, v} ι ι ↥A)

Tactic:
ext
-- 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
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis.{u_1, u, v} ι R ↥B
x : ↥B
i j : ι
⊢ Eq.{v + 1} (α := S)
    (↑((Algebra.leftMulMatrix (H.basisOfBasisRight H' b) : (a : S) → Matrix ι ι ↥A)
          ((algebraMap (↥B) S : (a : ↥B) → S) x) i j) :
      S)
    (↑((RingHom.mapMatrix (algebraMap R ↥A) : (a : Matrix ι ι R) → Matrix ι ι ↥A)
          ((Algebra.leftMulMatrix b : (a : ↥B) → Matrix ι ι R) x) i j) :
      S)

Tactic:
simp [Algebra.leftMulMatrix_eq_repr_mul, ← H.algebraMap_basisOfBasisRight_repr_apply H']

Premises used: Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, Algebra.leftMulMatrix_eq_repr_mul
-- 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 ↥A
rwa rwa₁ rwa₂ rwa₃ : A ⊔ B = ⊤
⊢ B ⊔ A = ⊤

Tactic:
rwa [sup_comm]

Premises used: sup_comm
-- 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 ↥A
i : ι
rwa rwa₁ rwa₂ rwa₃ : A ⊔ B = ⊤
⊢ B ⊔ A = ⊤

Tactic:
rwa [sup_comm]

Premises used: sup_comm
-- 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 ↥A
x : ↥A
i : ι
rwa rwa₁ rwa₂ rwa₃ : A ⊔ B = ⊤
⊢ B ⊔ A = ⊤

Tactic:
rwa [sup_comm]

Premises used: sup_comm
-- 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
inst_3 : Free.{u, v} R ↥A
inst_4 : Free.{u, v} R ↥B
⊢ Free.{u, v} R ↥(A ⊔ B)

Tactic:
Module.Free.of_equiv H.mulMap.toLinearEquiv

Premises used: Module.Free.of_equiv, AlgEquiv.toLinearEquiv, Subalgebra.LinearDisjoint.mulMap
-- 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
inst_3 : IsDomain S
⊢ IsDomain.{v} (↥A ⊗[R] ↥B)

Tactic:
H.injective.isDomain (A.mulMap B).toRingHom

Premises used: Function.Injective.isDomain, Submodule.LinearDisjoint.injective, Subalgebra.mulMap, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsDomain S
A : Type u_1
B : Type u_2
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra R B
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective.{u_1 + 1, v + 1} (α := A) (β := S) (⇑fa : (a : A) → S)
hfb : Function.Injective.{u_2 + 1, v + 1} (α := B) (β := S) (⇑fb : (a : B) → S)
H : fa.range.LinearDisjoint fb.range
⊢ IsDomain (A ⊗[R] B)

Tactic:
have := H.isDomain
  (Algebra.TensorProduct.congr
    (AlgEquiv.ofInjective fa hfa) (AlgEquiv.ofInjective fb hfb)).toMulEquiv.isDomain

Premises used: Membership.mem, Subtype, AlgEquiv.toMulEquiv, AlgEquiv.ofInjective, MulEquiv.isDomain, TensorProduct, Algebra.TensorProduct.congr, Subalgebra.LinearDisjoint.isDomain, AlgHom.range
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
⊢ Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulLeftMap (M := (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
        ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) a))
    ⊥

Tactic:
have h := Submodule.LinearDisjoint.linearIndependent_left_of_flat H ha
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
h :
  Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulLeftMap (M := (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
        ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) a))
    ⊥
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : LinearIndependent ↥B.op (M := Sᵐᵒᵖ) (MulOpposite.op ∘ (⇑A.val : (a : ↥A) → S) ∘ a)),
    LinearIndependent ↥B.op (M := Sᵐᵒᵖ) (MulOpposite.op ∘ (⇑A.val : (a : ↥A) → S) ∘ a)
⊢ LinearIndependent ↥B.op (M := Sᵐᵒᵖ) (MulOpposite.op ∘ (⇑A.val : (a : ↥A) → S) ∘ a)

Tactic:
rwa [mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at h

Premises used: Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis.{u_1, u, v} ι R ↥A
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥B.op (M := Sᵐᵒᵖ)
    (MulOpposite.op ∘ Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S) (⇑a : (a : ι) → ↥A))
⊢ Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulLeftMap (M := (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
        ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) (⇑a : (a : ι) → ↥A)))
    ⊥

Tactic:
rw [← mulLeftMap_ker_eq_bot_iff_linearIndependent_op] at H

Premises used: Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis.{u_1, u, v} ι R ↥A
H :
  Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulLeftMap (M := (toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
        ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) (⇑a : (a : ι) → ↥A)))
    ⊥
⊢ A.LinearDisjoint B

Tactic:
Submodule.LinearDisjoint.of_basis_left _ _ a H

Premises used: Submodule.LinearDisjoint.of_basis_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
⊢ Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulRightMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) (N :=
        (toSubmodule : (a : Subalgebra R S) → Submodule R S) B) b))
    ⊥

Tactic:
have h := Submodule.LinearDisjoint.linearIndependent_right_of_flat H hb
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥A
ι : Type u_1
b : ι → ↥B
hb : LinearIndependent R b
h :
  Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulRightMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) (N :=
        (toSubmodule : (a : Subalgebra R S) → Submodule R S) B) b))
    ⊥
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : LinearIndependent ↥A (M := S) ((⇑B.val : (a : ↥B) → S) ∘ b)),
    LinearIndependent ↥A (M := S) ((⇑B.val : (a : ↥B) → S) ∘ b)
⊢ LinearIndependent ↥A (M := S) ((⇑B.val : (a : ↥B) → S) ∘ b)

Tactic:
rwa [mulRightMap_ker_eq_bot_iff_linearIndependent] at h

Premises used: Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis.{u_1, u, v} ι R ↥B
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥A (M := S)
    (Function.comp (β := ↥B) (⇑B.val : (a : ↥B) → S) (⇑b : (a : ι) → ↥B))
⊢ Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulRightMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) (N :=
        (toSubmodule : (a : Subalgebra R S) → Submodule R S) B) (⇑b : (a : ι) → ↥B)))
    ⊥

Tactic:
rw [← mulRightMap_ker_eq_bot_iff_linearIndependent] at H

Premises used: Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
b : Basis.{u_1, u, v} ι R ↥B
H :
  Eq (α := Submodule R (Finsupp.{u_1, v} ι ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)))
    (LinearMap.ker
      (Submodule.mulRightMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) (N :=
        (toSubmodule : (a : Subalgebra R S) → Submodule R S) B) (⇑b : (a : ι) → ↥B)))
    ⊥
⊢ A.LinearDisjoint B

Tactic:
Submodule.LinearDisjoint.of_basis_right _ _ b H

Premises used: Submodule.LinearDisjoint.of_basis_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥B
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent R a
hc : ∀ (a : ↥A) (b : ↥B), Commute (↑a : S) (↑b : S)
⊢ LinearIndependent ↥B (M := S) ((⇑A.val : (a : ↥A) → S) ∘ a)

Tactic:
(H.symm_of_commute hc).linearIndependent_right_of_flat ha

Premises used: Subalgebra.LinearDisjoint.linearIndependent_right_of_flat, Subalgebra.LinearDisjoint.symm_of_commute
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : Basis.{u_1, u, v} ι R ↥A
H :
  LinearIndependent.{u_1, v, v} (ι := ι) ↥B (M := S)
    (Function.comp (β := ↥A) (⇑A.val : (a : ↥A) → S) (⇑a : (a : ι) → ↥A))
hc : ∀ (a : ↥A) (b : ↥B), Commute (↑a : S) (↑b : S)
⊢ A.LinearDisjoint B

Tactic:
(of_basis_right B A a H).symm_of_commute fun _ _ ↦ (hc _ _).symm

Premises used: Commute.symm, Subalgebra.LinearDisjoint.symm_of_commute, Subalgebra.LinearDisjoint.of_basis_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥A
κ : Type u_1
ι : Type u_2
a : κ → ↥A
b : ι → ↥B
ha : LinearIndependent R a
hb : LinearIndependent R b
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(a i.1) : S) * (↑(b i.2) : S)

Tactic:
Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left H ha hb

Premises used: Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥B
κ : Type u_1
ι : Type u_2
a : κ → ↥A
b : ι → ↥B
ha : LinearIndependent R a
hb : LinearIndependent R b
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(a i.1) : S) * (↑(b i.2) : S)

Tactic:
Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right H ha hb

Premises used: Submodule.LinearDisjoint.linearIndependent_mul_of_flat_right
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
κ : Type u_1
ι : Type u_2
a : κ → ↥A
b : ι → ↥B
ha : LinearIndependent R a
hb : LinearIndependent R b
⊢ LinearIndependent R (M := S) fun (i : κ × ι) ↦ (↑(a i.1) : S) * (↑(b i.2) : S)

Tactic:
Submodule.LinearDisjoint.linearIndependent_mul_of_flat H hf ha hb

Premises used: Submodule.LinearDisjoint.linearIndependent_mul_of_flat
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
κ : Type u_1
ι : Type u_2
a : Basis.{u_1, u, v} κ R ↥A
b : Basis.{u_2, u, v} ι R ↥B
H :
  LinearIndependent R (M := S) fun (i : κ × ι) ↦
    HMul.hMul (α := S) (↑((a : (a : κ) → ↥A) i.1) : S) (↑((b : (a : ι) → ↥B) i.2) : S)
⊢ A.LinearDisjoint B

Tactic:
Submodule.LinearDisjoint.of_basis_mul _ _ a b H

Premises used: Submodule.LinearDisjoint.of_basis_mul
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
A' : Subalgebra R S
h : A' ≤ A
inst_3 : Flat.{u, v} R ↥B
⊢ A'.LinearDisjoint B

Tactic:
Submodule.LinearDisjoint.of_le_left_of_flat H h

Premises used: Submodule.LinearDisjoint.of_le_left_of_flat
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
B' : Subalgebra R S
h : B' ≤ B
inst_3 : Flat.{u, v} R ↥A
⊢ A.LinearDisjoint B'

Tactic:
Submodule.LinearDisjoint.of_le_right_of_flat H h

Premises used: Submodule.LinearDisjoint.of_le_right_of_flat
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
A' B' : Subalgebra R S
ha : A' ≤ A
hb : B' ≤ B
inst_3 : Flat.{u, v} R ↥B
inst_4 : Flat.{u, v} R ↥A'
⊢ A'.LinearDisjoint B'

Tactic:
(H.of_le_left_of_flat ha).of_le_right_of_flat hb

Premises used: Subalgebra.LinearDisjoint.of_le_left_of_flat, Subalgebra.LinearDisjoint.of_le_right_of_flat
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
A' B' : Subalgebra R S
ha : A' ≤ A
hb : B' ≤ B
inst_3 : Flat.{u, v} R ↥A
inst_4 : Flat.{u, v} R ↥B'
⊢ A'.LinearDisjoint B'

Tactic:
(H.of_le_right_of_flat hb).of_le_left_of_flat ha

Premises used: Subalgebra.LinearDisjoint.of_le_left_of_flat, Subalgebra.LinearDisjoint.of_le_right_of_flat
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
le_antisymm (Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat H hf hc) ?_

Premises used: Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, le_antisymm
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
refine : 1 ≤ Module.rank R ↥(A ⊓ B)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
refine le_antisymm (Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat H hf hc) ?_

Premises used: Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, le_antisymm
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
⊢ Cardinal.lift.{u, v} (Module.rank R ↥⊥) = Cardinal.lift.{v, u} (Module.rank R R)

Tactic:
have : Cardinal.lift.{u} (Module.rank R (⊥ : Subalgebra R S)) =
      Cardinal.lift.{v} (Module.rank R R) :=
    lift_rank_range_of_injective (Algebra.linearMap R S) hinj
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Cardinal.lift.{u, v} (Module.rank R ↥⊥) = Cardinal.lift.{v, u} (Module.rank R R)
⊢ Module.rank R ↥⊥ = 1

Tactic:
rw [Module.rank_self, Cardinal.lift_one, Cardinal.lift_eq_one] at this

Premises used: Module.rank_self, Cardinal.lift_one, Cardinal.lift_eq_one
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Module.rank R ↥⊥ = 1
rw : Module.rank R ↥⊥ ≤ Module.rank R ↥(A ⊓ B)
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Module.rank R ↥⊥ = 1
change :
  Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ≤
    Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊓ B) : Submodule R S)
⊢ Module.rank R ↥⊥ ≤ Module.rank R ↥(A ⊓ B)

Tactic:
change Module.rank R (toSubmodule (⊥ : Subalgebra R S)) ≤
    Module.rank R (toSubmodule (A ⊓ B))

Premises used: Membership.mem, Subtype, Bot.bot, Subalgebra.toSubmodule, Module.rank, DFunLike.coe, Min.min
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ≤
    Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊓ B) : Submodule R S)

Tactic:
Submodule.rank_mono (bot_le : (⊥ : Subalgebra R S) ≤ A ⊓ B)

Premises used: Submodule.rank_mono, bot_le
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat.{u, v} R ↥A ∨ Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) ⊥ : Submodule R S) ≤
    Module.rank R ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) (A ⊓ B) : Submodule R S)

Tactic:
exact Submodule.rank_mono (bot_le : (⊥ : Subalgebra R S) ≤ A ⊓ B)

Premises used: Submodule.rank_mono
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥A
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
H.rank_inf_eq_one_of_commute_of_flat_of_inj (Or.inl ‹_›) hc hinj

Premises used: Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj, Or.inl
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst_3 : Flat.{u, v} R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥(A ⊓ B) = 1

Tactic:
H.rank_inf_eq_one_of_commute_of_flat_of_inj (Or.inr ‹_›) hc hinj

Premises used: Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj, Or.inr
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst_3 : Flat.{u, v} R ↥A
hc : ∀ (a b : ↥A), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw :
  ∀ (hc : ∀ (a b : ↥(A ⊓ A)), Commute (↑a : S) (↑b : S))
    (hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)),
    Module.rank R ↥(A ⊓ A) = 1
⊢ Module.rank R ↥A = 1

Tactic:
rw [← inf_of_le_left (le_refl A)] at hc ⊢

Premises used: le_refl, inf_of_le_left
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst_3 : Flat.{u, v} R ↥A
hc : ∀ (a b : ↥(A ⊓ A)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥(A ⊓ A) = 1

Tactic:
H.rank_inf_eq_one_of_commute_of_flat_left_of_inj hc hinj

Premises used: Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj
-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst_3 : Flat.{u, v} R ↥A
hc : ∀ (a b : ↥(A ⊓ A)), Commute (↑a : S) (↑b : S)
hinj : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Module.rank R ↥(A ⊓ A) = 1

Tactic:
exact H.rank_inf_eq_one_of_commute_of_flat_left_of_inj hc hinj

Premises used: Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj