awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
⊢ relrank ⊤ A = 1

Tactic:
relrank_eq_one_of_le le_top

Premises used: Subfield.relrank_eq_one_of_le, le_top
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
⊢ relfinrank ⊤ A = 1

Tactic:
relfinrank_eq_one_of_le le_top

Premises used: Subfield.relfinrank_eq_one_of_le, le_top
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
x : AddCommMonoid ↥⊤ := inferInstance
rw : Module.rank ↥A ↥(extendScalars (E := ⊤) ⋯) = Module.rank (↥A) E
rw₁ : Module.rank ↥A ↥⊤ = Module.rank (↥A) E
rw₂ rw₃ : Module.rank (↥A) E = Module.rank (↥A) E
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,
    IntermediateField.topEquiv.toLinearEquiv.rank_eq]

Premises used: Subfield.extendScalars_top, le_top, Subfield.relrank_eq_rank_of_le, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv, IntermediateField.topEquiv
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
⊢ A.relfinrank ⊤ = finrank (↥A) E

Tactic:
simp [relfinrank_eq_toNat_relrank, finrank]

Premises used: Subfield.relfinrank_eq_toNat_relrank, Module.finrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : E →+* L
rw : Eq.{w + 1} (α := Subring L) (Subring.map f (A ⊓ B).toSubring : Subring L) (toSubring (map f (A ⊓ B)) : Subring L)
⊢ Eq.{w + 1} (α := Subring L) (Subring.map f (A ⊓ B).toSubring : Subring L) (toSubring (map f A ⊓ map f B) : Subring L)

Tactic:
rw [← map_inf]

Premises used: Subfield.map_inf
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : E →+* L
⊢ Eq.{w + 1} (α := Subring L) (Subring.map f (A ⊓ B).toSubring : Subring L) (toSubring (map f (A ⊓ B)) : Subring L)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
L : Type v
inst_1 : Field L
f : E →+* L
⊢ relrank (E := L) (map f A) (map f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_map_map A B f

Premises used: Subfield.lift_relrank_map_map, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A : Subfield E
f : L →+* E
B : Subfield L
rw : A ⊓ RingHom.fieldRange.{w, v} (K := L) f ⊓ map f B = A ⊓ map f B
rw₁ : A ⊓ map.{w, v} (K := L) f ⊤ ⊓ map f B = A ⊓ map f B
rw₂ : A ⊓ (map.{w, v} (K := L) f ⊤ ⊓ map f B) = A ⊓ map f B
rw₃ : A ⊓ map f (⊤ ⊓ B) = A ⊓ map f B
rw₄ rw₅ : A ⊓ map f B = A ⊓ map f B
⊢ map.{w, v} (K := L) f (comap f A) ⊓ map f B = A ⊓ map f B

Tactic:
rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]

Premises used: Subfield.map_inf, top_inf_eq, Subfield.map_comap_eq, RingHom.fieldRange_eq_map, inf_assoc
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
L : Type v
inst_1 : Field L
f : L →+* E
B : Subfield L
⊢ relrank (comap f A) B = A.relrank (map f B)

Tactic:
simpa only [lift_id] using A.lift_relrank_comap f B

Premises used: Subfield.lift_relrank_comap, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A : Subfield E
f : L →+* E
B : Subfield L
⊢ relfinrank (comap f A) B = A.relfinrank (map f B)

Tactic:
simpa using congr(toNat $(lift_relrank_comap A f B))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A : Subfield E
f : L →+* E
⊢ lift.{v, w} (Module.rank (↥(comap f A)) L) = lift.{w, v} (A.relrank (RingHom.fieldRange.{w, v} (K := L) f))

Tactic:
simpa only [relrank_top_right, ← RingHom.fieldRange_eq_map] using lift_relrank_comap A f ⊤

Premises used: Subfield.lift_relrank_comap, RingHom.fieldRange_eq_map, Subfield.relrank_top_right, Top.top
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A : Subfield E
L : Type v
inst_1 : Field L
f : L →+* E
⊢ Module.rank (↥(comap f A)) L = A.relrank (f.fieldRange (K := L))

Tactic:
simpa only [lift_id] using A.lift_rank_comap f

Premises used: Subfield.lift_rank_comap, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A : Subfield E
f : L →+* E
⊢ finrank (↥(comap f A)) L = A.relfinrank (RingHom.fieldRange.{w, v} (K := L) f)

Tactic:
simpa using congr(toNat $(lift_rank_comap A f))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : E →+* L
⊢ relfinrank.{w} (E := L) (map f A) (map f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_map_map A B f))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
rw : lift.{w, v} ((A ⊓ RingHom.fieldRange.{w, v} (K := L) f).relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f))
| lift.{v, w} (relrank (E := L) (comap f A) (comap f B))

Tactic:
rw [← lift_relrank_map_map _ _ f, map_comap_eq, map_comap_eq]

Premises used: Subfield.lift_relrank_map_map, Subfield.map_comap_eq
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
conv_lhs :
  lift.{w, v} ((A ⊓ RingHom.fieldRange.{w, v} (K := L) f).relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)) =
    lift.{w, v} (A.relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f))
⊢ lift.{v, w} (relrank (E := L) (comap f A) (comap f B)) =
    lift.{w, v} (A.relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f))

Tactic:
conv_lhs => rw [← lift_relrank_map_map _ _ f, map_comap_eq, map_comap_eq]

Premises used: Subfield.lift_relrank_map_map, Subfield.map_comap_eq
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
e_c :
  (A ⊓ RingHom.fieldRange.{w, v} (K := L) f).relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f) =
    A.relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)
⊢ lift.{w, v} ((A ⊓ RingHom.fieldRange.{w, v} (K := L) f).relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)) =
    lift.{w, v} (A.relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f))

Tactic:
congr 1
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
e_c :
  A ⊓ RingHom.fieldRange.{w, v} (K := L) f ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f) =
    A ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)
⊢ (A ⊓ RingHom.fieldRange.{w, v} (K := L) f).relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f) =
    A.relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)

Tactic:
apply relrank_eq_of_inf_eq

Premises used: Subfield.relrank_eq_of_inf_eq
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
e_c :
  A ⊓ (RingHom.fieldRange.{w, v} (K := L) f ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)) =
    A ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)
e_c₁ :
  A ⊓ (B ⊓ (RingHom.fieldRange.{w, v} (K := L) f ⊓ RingHom.fieldRange.{w, v} (K := L) f)) =
    A ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)
e_c₂ e_c₃ : A ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f) = A ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)
⊢ A ⊓ RingHom.fieldRange.{w, v} (K := L) f ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f) =
    A ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)

Tactic:
rw [inf_assoc, inf_left_comm _ B, inf_of_le_left (le_refl _)]

Premises used: le_refl, inf_of_le_left, inf_assoc, inf_left_comm
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
L : Type v
inst_1 : Field L
f : L →+* E
⊢ relrank (E := L) (comap f A) (comap f B) = A.relrank (B ⊓ f.fieldRange (K := L))

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Premises used: Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
⊢ relfinrank.{w} (E := L) (comap f A) (comap f B) = A.relfinrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
h : B ≤ RingHom.fieldRange.{w, v} (K := L) f
⊢ lift.{v, w} (relrank (E := L) (comap f A) (comap f B)) = lift.{w, v} (A.relrank B)

Tactic:
simpa only [inf_of_le_left h] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Premises used: inf_of_le_left, Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
L : Type v
inst_1 : Field L
f : L →+* E
h : B ≤ f.fieldRange (K := L)
⊢ relrank (E := L) (comap f A) (comap f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h

Premises used: Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_le, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
h : B ≤ RingHom.fieldRange.{w, v} (K := L) f
⊢ relfinrank.{w} (E := L) (comap f A) (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
h : Function.Surjective.{w + 1, v + 1} (α := L) (β := E) (⇑f : (a : L) → E)
⊢ lift.{v, w} (relrank (E := L) (comap f A) (comap f B)) = lift.{w, v} (A.relrank B)

Tactic:
lift_relrank_comap_comap_eq_lift_relrank_of_le A B f fun x _ ↦ h x

Premises used: Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
L : Type v
inst_1 : Field L
f : L →+* E
h : Function.Surjective (α := L) (β := E) (⇑f : (a : L) → E)
⊢ relrank (E := L) (comap f A) (comap f B) = A.relrank B

Tactic:
simpa using lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h

Premises used: Subfield.lift_relrank_comap_comap_eq_lift_relrank_of_surjective
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
h : Function.Surjective.{w + 1, v + 1} (α := L) (β := E) (⇑f : (a : L) → E)
⊢ relfinrank.{w} (E := L) (comap f A) (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relrank B ∣ Module.rank (↥A) E

Tactic:
dvd_of_mul_right_eq _ (relrank_mul_rank_top h)

Premises used: dvd_of_mul_right_eq, Subfield.relrank_mul_rank_top
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relfinrank B ∣ finrank (↥A) E

Tactic:
dvd_of_mul_right_eq _ (relfinrank_mul_finrank_top h)

Premises used: Subfield.relfinrank_mul_finrank_top, dvd_of_mul_right_eq
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A ≤ C

Tactic:
have h3 := h1.trans h2
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
rw : Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
rw [relrank_eq_rank_of_le h1, relrank_eq_rank_of_le h2, relrank_eq_rank_of_le h3]

Premises used: Subfield.relrank_eq_rank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this_1 : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this_2 : Algebra ↥B ↥C := (inclusion h2).toAlgebra
this : Algebra ↥A ↥C := (inclusion h3).toAlgebra
⊢ IsScalarTower.{v, v, v} ↥A ↥B ↥C

Tactic:
haveI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this_1 : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this_2 : Algebra ↥B ↥C := (inclusion h2).toAlgebra
this_3 : Algebra ↥A ↥C := (inclusion h3).toAlgebra
this : IsScalarTower.{v, v, v} ↥A ↥B ↥C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
rank_mul_rank A B C

Premises used: Set.Mem, rank_mul_rank, Membership.mem, Subtype, Subfield.extendScalars, Subfield.toIntermediateField
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
this_1 : Algebra ↥A ↥B := (inclusion h1).toAlgebra
this_2 : Algebra ↥B ↥C := (inclusion h2).toAlgebra
this_3 : Algebra ↥A ↥C := (inclusion h3).toAlgebra
this : IsScalarTower.{v, v, v} ↥A ↥B ↥C
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)

Tactic:
exact rank_mul_rank A B C

Premises used: rank_mul_rank, Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank h1 h2))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
rw : (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
rw₁ : (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * (B ⊓ C).relrank C = (A ⊓ B).relrank C
rw₂ : (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * (B ⊓ C).relrank C = (A ⊓ B ⊓ C).relrank C
rw₃ : (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * (B ⊓ C).relrank C = (A ⊓ (B ⊓ C)).relrank C
rw₄ rw₅ : (A ⊓ (B ⊓ C)).relrank C = (A ⊓ (B ⊓ C)).relrank C
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C

Tactic:
rw [← inf_relrank_right A (B ⊓ C), ← inf_relrank_right B C, ← inf_relrank_right (A ⊓ B) C,
    inf_assoc, relrank_mul_relrank inf_le_right inf_le_right]

Premises used: inf_le_right, Subfield.relrank_mul_relrank, inf_assoc, Subfield.inf_relrank_right, Min.min
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank A B C))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : B ≤ C
⊢ A.relrank B * B.relrank C = (A ⊓ B).relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Premises used: inf_of_le_left, Subfield.relrank_inf_mul_relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank_eq_inf_relrank A h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : A ≤ B
⊢ A.relrank (B ⊓ C) * B.relrank C = A.relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Premises used: inf_of_le_left, Subfield.relrank_inf_mul_relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : A ≤ B
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank_of_le C h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : A ≤ B
⊢ B.relrank C ∣ A.relrank C

Tactic:
dvd_of_mul_left_eq _ (relrank_inf_mul_relrank_of_le C h)

Premises used: dvd_of_mul_left_eq, Subfield.relrank_inf_mul_relrank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h : A ≤ B
⊢ B.relfinrank C ∣ A.relfinrank C

Tactic:
dvd_of_mul_left_eq _ (relfinrank_inf_mul_relfinrank_of_le C h)

Premises used: Subfield.relfinrank_inf_mul_relfinrank_of_le, dvd_of_mul_left_eq
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ A.relfinrank B = (toNat : (a : Cardinal.{v}) → ℕ) (A.relrank B)

Tactic:
rfl

Premises used: Subfield.relrank, IntermediateField.relfinrank, Subfield.relfinrank, IntermediateField.relrank, Module.finrank, rfl
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : A ⊓ C = B ⊓ C
⊢ A.relrank C = B.relrank C

Tactic:
Subfield.relrank_eq_of_inf_eq congr(toSubfield $h)

Premises used: congrArg, Subfield.relrank_eq_of_inf_eq, id, IntermediateField.toSubfield, IntermediateField.relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : A ⊓ C = B ⊓ C
⊢ A.relfinrank C = B.relfinrank C

Tactic:
congr(toNat $(relrank_eq_of_inf_eq h))

Premises used: congrArg, IntermediateField.relrank_eq_of_inf_eq, Cardinal.toNat, id, DFunLike.coe
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ A.relrank B = Module.rank ↥A ↥(extendScalars h)

Tactic:
Subfield.relrank_eq_rank_of_le h

Premises used: Subfield.subtype, Set.Mem, IntermediateField.extendScalars, Subfield.relrank_eq_rank_of_le, Subfield.extendScalars, IntermediateField.relrank, Subfield.toIntermediateField
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ A.relfinrank B = finrank.{v, v} ↥A ↥(extendScalars h)

Tactic:
congr(toNat $(relrank_eq_rank_of_le h))

Premises used: congrArg, Cardinal.toNat, id, IntermediateField.relrank_eq_rank_of_le, DFunLike.coe
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ (A ⊓ B).relrank B = A.relrank B

Tactic:
relrank_eq_rank_of_le (inf_le_right : A ⊓ B ≤ B)

Premises used: Subfield.subtype, IntermediateField.copy, Subfield.relrank, Set.Mem, inf_le_right, IntermediateField.extendScalars, Subfield.extendScalars, IntermediateField.relrank_eq_rank_of_le, IntermediateField.relrank, Subfield.toIntermediateField
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ (A ⊓ B).relfinrank B = A.relfinrank B

Tactic:
congr(toNat $(inf_relrank_right A B))

Premises used: congrArg, IntermediateField.inf_relrank_right, Cardinal.toNat, id, DFunLike.coe
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
rw : (B ⊓ A).relrank A = B.relrank A
rw₁ rw₂ : B.relrank A = B.relrank A
⊢ (A ⊓ B).relrank A = B.relrank A

Tactic:
rw [inf_comm, inf_relrank_right]

Premises used: IntermediateField.inf_relrank_right, inf_comm
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ (A ⊓ B).relfinrank A = B.relfinrank A

Tactic:
congr(toNat $(inf_relrank_left A B))

Premises used: congrArg, Cardinal.toNat, id, IntermediateField.inf_relrank_left, DFunLike.coe
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ A.relrank A = 1

Tactic:
A.toSubfield.relrank_self

Premises used: IntermediateField.toSubfield, IntermediateField.relrank, Subfield.relrank_self
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ A.relfinrank A = 1

Tactic:
A.toSubfield.relfinrank_self

Premises used: IntermediateField.relfinrank, IntermediateField.toSubfield, Subfield.relfinrank_self
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ A.relrank B = 1 ↔ B ≤ A

Tactic:
Subfield.relrank_eq_one_iff

Premises used: Set.Mem, Subfield.relrank_eq_one_iff, IntermediateField.relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ A.relfinrank B = 1 ↔ B ≤ A

Tactic:
Subfield.relfinrank_eq_one_iff

Premises used: Subfield.relfinrank_eq_one_iff, Set.Mem, IntermediateField.relfinrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A : IntermediateField F E
f : L →ₐ[F] E
⊢ Cardinal.lift.{v, w} (Module.rank (↥(comap f A)) L) = Cardinal.lift.{w, v} (A.relrank f.fieldRange)

Tactic:
A.toSubfield.lift_rank_comap f.toRingHom

Premises used: Set.Mem, Subfield.copy, Subsemiring.comap, Subfield.comap, AlgHom.toRingHom, Subring.comap, IntermediateField.toSubfield, Subfield.lift_rank_comap, RingHom.fieldRange, IntermediateField.relrank, Subsemiring.copy, IntermediateField.comap, RingHom.rangeS
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type v
inst_3 : Field L
inst_4 : Algebra F L
f : L →ₐ[F] E
⊢ Module.rank (↥(comap f A)) L = A.relrank f.fieldRange

Tactic:
simpa only [lift_id] using A.lift_rank_comap f

Premises used: IntermediateField.lift_rank_comap, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A : IntermediateField F E
f : L →ₐ[F] E
⊢ finrank (↥(comap f A)) L = A.relfinrank f.fieldRange

Tactic:
simpa using congr(toNat $(lift_rank_comap A f))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A : IntermediateField F E
f : L →ₐ[F] E
B : IntermediateField F L
⊢ Cardinal.lift.{v, w} ((comap f A).relrank B) = Cardinal.lift.{w, v} (A.relrank (map f B))

Tactic:
A.toSubfield.lift_relrank_comap f.toRingHom B.toSubfield

Premises used: Subring.map, Subsemiring.comap, Subfield.comap, Subfield.lift_relrank_comap, AlgHom.toRingHom, Subring.comap, IntermediateField.toSubfield, Subsemiring.map, IntermediateField.relrank, Subfield.map
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type v
inst_3 : Field L
inst_4 : Algebra F L
f : L →ₐ[F] E
B : IntermediateField F L
⊢ (comap f A).relrank B = A.relrank (map f B)

Tactic:
simpa only [lift_id] using A.lift_relrank_comap f B

Premises used: IntermediateField.lift_relrank_comap, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A : IntermediateField F E
f : L →ₐ[F] E
B : IntermediateField F L
⊢ (comap f A).relfinrank B = A.relfinrank (map f B)

Tactic:
simpa using congr(toNat $(lift_relrank_comap A f B))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : E →ₐ[F] L
rw : Cardinal.lift.{w, v} ((comap f (map f A)).relrank B) = Cardinal.lift.{w, v} (A.relrank B)
rw₁ rw₂ : Cardinal.lift.{w, v} (A.relrank B) = Cardinal.lift.{w, v} (A.relrank B)
⊢ Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
rw [← lift_relrank_comap, comap_map]

Premises used: IntermediateField.lift_relrank_comap, IntermediateField.comap_map
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
L : Type v
inst_3 : Field L
inst_4 : Algebra F L
f : E →ₐ[F] L
⊢ (map f A).relrank (map f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_map_map A B f

Premises used: IntermediateField.lift_relrank_map_map, Cardinal.lift_id