-- Mathlib/RingTheory/Adjoin/Dimension.lean
theorem finrank_sup_le_of_free : finrank R ↥(A ⊔ B) ≤ finrank R A * finrank R B

Proof state:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
this : Module.rank R ↥(toSubmodule A) ≤ Module.rank R ↥(toSubmodule (A ⊔ B))
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
rw [show finrank R A = 0 from Cardinal.toNat_apply_of_aleph0_le hA,
  show finrank R ↥(A ⊔ B) = 0 from Cardinal.toNat_apply_of_aleph0_le (hA.trans this), zero_mul]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : ¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
rw [← rank_lt_aleph0_iff, not_lt] at hA

Result:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Proof state:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
  show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp

Result:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
this : Module.rank R ↥(toSubmodule A) ≤ Module.rank R ↥(toSubmodule (A ⊔ B))
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Proof state:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : Cardinal.aleph0 ≤ Module.rank R ↥A
⊢ toSubmodule A ≤ toSubmodule (A ⊔ B)

Tactic:
simp

Result:
no goals

Proof state:
case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this✝ :
  ∀ (A B : Subalgebra R S) [inst : Free R ↥A] [inst : Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
this : finrank R ↥(B ⊔ A) ≤ finrank R ↥B * finrank R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
rwa [sup_comm, mul_comm] at this

Result:
no goals

Proof state:
case neg
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
wlog hA : ¬ Module.Finite R A generalizing A B

Result:
case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this :
  ∀ (A B : Subalgebra R S) [inst : Free R ↥A] [inst : Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A✝ B✝ A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
hA : ¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Proof state:
case pos.intro
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
left✝ : Module.Finite R ↥A
right✝ : Module.Finite R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
simpa only [map_mul] using Cardinal.toNat_le_toNat (A.rank_sup_le_of_free B)
  (Cardinal.mul_lt_aleph0 (rank_lt_aleph0 R A) (rank_lt_aleph0 R B))

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
by_cases h : Module.Finite R A ∧ Module.Finite R B

Result:
case pos
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : Module.Finite R ↥A ∧ Module.Finite R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

case neg
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Proof state:
case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this :
  ∀ (A B : Subalgebra R S) [inst : Free R ↥A] [inst : Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
have := this B A (fun h' ↦ h h'.symm) (not_and.1 h (of_not_not hA))

Result:
case neg.inr
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B)
this✝ :
  ∀ (A B : Subalgebra R S) [inst : Free R ↥A] [inst : Free R ↥B],
    ¬(Module.Finite R ↥A ∧ Module.Finite R ↥B) → ¬Module.Finite R ↥A → finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B
hA : ¬¬Module.Finite R ↥A
this : finrank R ↥(B ⊔ A) ≤ finrank R ↥B * finrank R ↥A
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Proof state:
case pos
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
h : Module.Finite R ↥A ∧ Module.Finite R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B

Tactic:
obtain ⟨_, _⟩ := h

Result:
case pos.intro
R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : StrongRankCondition R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free R ↥B
left✝ : Module.Finite R ↥A
right✝ : Module.Finite R ↥B
⊢ finrank R ↥(A ⊔ B) ≤ finrank R ↥A * finrank R ↥B