-- 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
⊢ A.LinearDisjoint B

Tactic:
haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h2)

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
⊢ 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
⊢ A.LinearDisjoint B

Tactic:
by_cases h2 : Module.finrank R B = 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
h2 : Module.finrank R ↥B = 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
h2 : ¬Module.finrank R ↥B = 0
⊢ 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
⊢ A.LinearDisjoint B

Tactic:
haveI := Module.finite_of_finrank_pos (Nat.pos_of_ne_zero h1)

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
⊢ 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 ↥B = 1
a✝ : Nontrivial R
h1 : Module.finrank R ↥A = 0
⊢ A.LinearDisjoint ⊥

Tactic:
exact bot_right _

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 = 1
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : Module.finrank R ↥B = 0
⊢ ⊥.LinearDisjoint B

Tactic:
exact bot_left _

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 = 1
a✝ : Nontrivial R
h1 : ¬Module.finrank R ↥A = 0
h2 : Module.finrank R ↥B = 0
⊢ A.LinearDisjoint B

Tactic:
rw [eq_bot_of_finrank_one 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
⊢ ⊥.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 ↥B = 1
a✝ : Nontrivial R
h1 : Module.finrank R ↥A = 0
⊢ A.LinearDisjoint B

Tactic:
rw [eq_bot_of_finrank_one 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 ⊥