-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem Ideal.rank_eq {R S : Type*} [CommRing R] [StrongRankCondition R] [Ring S] [IsDomain S]
    [Algebra R S] {n m : Type*} [Fintype n] [Fintype m] (b : Basis n R S) {I : Ideal S}
    (hI : I ≠ ⊥) (c : Basis m R I) : Fintype.card m = Fintype.card n

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
⊢ LinearIndependent R fun i => b i • a

Tactic:
have hb := b.linearIndependent

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : LinearIndependent R ⇑b
⊢ LinearIndependent R fun i => b i • a

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i : n, g i • b i • a = 0
⊢ ∑ i : n, g i • b i = 0

Tactic:
simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i : n, g i • b i = 0 ∨ a = 0
⊢ ∑ i : n, g i • b i = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
⊢ ∀ (g : n → R), ∑ i : n, g i • b i • a = 0 → ∀ (i : n), g i = 0

Tactic:
intro g hg

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i : n, g i • b i • a = 0
⊢ ∀ (i : n), g i = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : LinearIndependent R ⇑b
⊢ LinearIndependent R fun i => b i • a

Tactic:
rw [Fintype.linearIndependent_iff] at hb ⊢

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
⊢ ∀ (g : n → R), ∑ i : n, g i • b i • a = 0 → ∀ (i : n), g i = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
⊢ Fintype.card m = Fintype.card n

Tactic:
obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr hI)

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
⊢ Fintype.card m = Fintype.card n

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
⊢ Fintype.card m = Fintype.card n

Tactic:
have : LinearIndependent R fun i => b i • a := by
  have hb := b.linearIndependent
  rw [Fintype.linearIndependent_iff] at hb ⊢
  intro g hg
  apply hb g
  simp only [← smul_assoc, ← Finset.sum_smul, smul_eq_zero] at hg
  exact hg.resolve_right ha

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
this : LinearIndependent R fun i => b i • a
⊢ Fintype.card m = Fintype.card n

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
this : LinearIndependent R fun i => b i • a
⊢ Fintype.card m = Fintype.card n

Tactic:
exact le_antisymm
  (b.card_le_card_of_linearIndependent (c.linearIndependent.map' (Submodule.subtype I)
    ((LinearMap.ker_eq_bot (f := (Submodule.subtype I : I →ₗ[R] S))).mpr Subtype.coe_injective)))
  (c.card_le_card_of_linearIndependent this)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i : n, g i • b i = 0 ∨ a = 0
⊢ ∑ i : n, g i • b i = 0

Tactic:
exact hg.resolve_right ha

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i : n, g i • b i • a = 0
⊢ ∀ (i : n), g i = 0

Tactic:
apply hb g

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_3
m : Type u_4
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i : n, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i : n, g i • b i • a = 0
⊢ ∑ i : n, g i • b i = 0