-- Mathlib/RingTheory/LinearDisjoint.lean
theorem of_finrank_coprime_of_free [Module.Free R A] [Module.Free R B]
    [Module.Free A (Algebra.adjoin A (B : Set S))] [Module.Free B (Algebra.adjoin B (A : Set S))]
    (H : (Module.finrank R A).Coprime (Module.finrank R B)) : A.LinearDisjoint B

Proof state:
case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : ¬Module.finrank R ↥B = 0
this✝¹ : Module.Finite R ↥A
this✝ : Module.Finite R ↥B
this : Module.Finite R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Tactic:
have : Module.finrank R A ≤ Module.finrank R ↥(A ⊔ B) :=
  LinearMap.finrank_le_finrank_of_injective <|
    Submodule.inclusion_injective (show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp)

Result:
case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : ¬Module.finrank R ↥B = 0
this✝² : Module.Finite R ↥A
this✝¹ : Module.Finite R ↥B
this✝ : Module.Finite R ↥(A ⊔ B)
this : Module.finrank R ↥A ≤ Module.finrank R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Proof state:
case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : ¬Module.finrank R ↥B = 0
this✝ : Module.Finite R ↥A
this : Module.Finite R ↥B
⊢ A.LinearDisjoint B

Tactic:
haveI := finite_sup A B

Result:
case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : ¬Module.finrank R ↥B = 0
this✝¹ : Module.Finite R ↥A
this✝ : Module.Finite R ↥B
this : Module.Finite R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : ¬Module.finrank R ↥B = 0
this✝¹ : Module.Finite R ↥A
this✝ : Module.Finite R ↥B
this : Module.Finite R ↥(A ⊔ B)
⊢ toSubmodule A ≤ toSubmodule (A ⊔ B)

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : Module.finrank R ↥B = 0
⊢ A.LinearDisjoint B

Tactic:
rw [h2, Nat.coprime_zero_right] at H

Result:
case pos
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : Module.finrank R ↥A = 1
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : Module.finrank R ↥B = 0
⊢ A.LinearDisjoint B

Proof state:
case pos
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : Module.finrank R ↥A = 0
⊢ A.LinearDisjoint B

Tactic:
rw [h1, Nat.coprime_zero_left] at H

Result:
case pos
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : Module.finrank R ↥B = 1
a✝ : Nontrivial R
h1 : Module.finrank R ↥A = 0
⊢ A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
⊢ A.LinearDisjoint B

Tactic:
by_cases h1 : Module.finrank R A = 0

Result:
case pos
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : Module.finrank R ↥A = 0
⊢ A.LinearDisjoint B

case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
⊢ A.LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
⊢ A.LinearDisjoint B

Tactic:
nontriviality R

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
⊢ A.LinearDisjoint B

Proof state:
case neg
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Module.Free R ↥A
inst✝² : Module.Free R ↥B
inst✝¹ : Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (Module.finrank R ↥A).Coprime (Module.finrank R ↥B)
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : ¬Module.finrank R ↥B = 0
this✝² : Module.Finite R ↥A
this✝¹ : Module.Finite R ↥B
this✝ : Module.Finite R ↥(A ⊔ B)
this : Module.finrank R ↥A ≤ Module.finrank R ↥(A ⊔ B)
⊢ A.LinearDisjoint B

Tactic:
exact of_finrank_sup_of_free <| (finrank_sup_le_of_free A B).antisymm <|
  Nat.le_of_dvd (lt_of_lt_of_le (Nat.pos_of_ne_zero h1) this) <| H.mul_dvd_of_dvd_of_dvd
    (finrank_left_dvd_finrank_sup_of_free A B) (finrank_right_dvd_finrank_sup_of_free A B)

Result:
no goals