awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Valuation (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X⁻¹ :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := F⟮X⟯) 1 RatFunc.X) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₁ : Eq (α := WithZero (Multiplicative ℤ))
  (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
      (HPow.hPow (α := F⟮X⟯) (β := ℤ) RatFunc.X (-1)) :
    WithZero (Multiplicative ℤ))
  (exp (-1) : WithZero (Multiplicative ℤ))
Tactic: rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Valuation (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        RatFunc.X⁻¹ :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := F⟮X⟯) (β := ℤ) RatFunc.X (-1)) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((inftyValuation F : Valuation F⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : F⟮X⟯) → WithZero (Multiplicative ℤ))
        (HDiv.hDiv (α := F⟮X⟯) 1 RatFunc.X) :
      WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))
have rw₂ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-1)) (exp (-1))
Tactic: rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Valuation (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
⊢ inftyValuationDef F ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p) = exp (↑p.natDegree : ℤ)
have rw : (if Eq (α := F⟮X⟯) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p : F⟮X⟯) (0 : F⟮X⟯) then 0
  else exp (intDegree.{u_1} (K := F) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p))) =
  exp (↑p.natDegree : ℤ)
Tactic: rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Valuation (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
rw :
  (if Eq (α := F⟮X⟯) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p : F⟮X⟯) (0 : F⟮X⟯) then 0
    else exp (intDegree.{u_1} (K := F) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p))) =
    exp (↑p.natDegree : ℤ)
⊢ inftyValuationDef F ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p) = exp (↑p.natDegree : ℤ)
have rw₁ : exp (intDegree.{u_1} (K := F) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p)) = exp (↑p.natDegree : ℤ)
Tactic: rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]
-- Lean 4 proof step from Mathlib.FieldTheory.RatFunc.Valuation (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F⟮X⟯
p : F[X]
hp : p ≠ 0
rw :
  (if Eq (α := F⟮X⟯) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p : F⟮X⟯) (0 : F⟮X⟯) then 0
    else exp (intDegree.{u_1} (K := F) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p))) =
    exp (↑p.natDegree : ℤ)
rw₁ : exp (intDegree.{u_1} (K := F) ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p)) = exp (↑p.natDegree : ℤ)
⊢ inftyValuationDef F ((algebraMap F[X] F⟮X⟯ : (a : F[X]) → F⟮X⟯) p) = exp (↑p.natDegree : ℤ)
have rw₂ : Eq (α := WithZero (Multiplicative ℤ)) (exp (↑p.natDegree : ℤ)) (exp (↑p.natDegree : ℤ))
Tactic: rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (hypothesis)
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
⊢ Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = Module.rank ↥A ↥(extendScalars h)
have this : A ⊓ B = A
Tactic: have := inf_of_le_left h
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
⊢ (A ⊓ B).relrank A = B.relrank A
have rw : (B ⊓ A).relrank A = B.relrank A
Tactic: rw [inf_comm, inf_relrank_right]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : (B ⊓ A).relrank A = B.relrank A
⊢ (A ⊓ B).relrank A = B.relrank A
have rw₁ : B.relrank A = B.relrank A
Tactic: rw [inf_comm, inf_relrank_right]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A : Subfield E
⊢ A.relrank A = 1
have rw : Module.rank ↥A ↥(extendScalars sorry) = 1
Tactic: rw [relrank_eq_rank_of_le (le_refl A), extendScalars_self, IntermediateField.rank_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A : Subfield E
rw : Module.rank ↥A ↥(extendScalars ⋯) = 1
⊢ A.relrank A = 1
have rw₁ : Module.rank ↥A ↥⊥ = 1
Tactic: rw [relrank_eq_rank_of_le (le_refl A), extendScalars_self, IntermediateField.rank_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A : Subfield E
rw : Module.rank ↥A ↥(extendScalars ⋯) = 1
rw₁ : Module.rank ↥A ↥⊥ = 1
⊢ A.relrank A = 1
have rw₂ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
Tactic: rw [relrank_eq_rank_of_le (le_refl A), extendScalars_self, IntermediateField.rank_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
⊢ A.relrank B = 1 ↔ B ≤ A
have rw : Module.rank ↥(A ⊓ B) ↥(extendScalars sorry) = 1 ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A
have rw₁ : extendScalars sorry = ⊥ ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
rw₁ : extendScalars ⋯ = ⊥ ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A
have rw₂ : (extendScalars sorry).toSubfield = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
rw₁ : extendScalars ⋯ = ⊥ ↔ B ≤ A
rw₂ : (extendScalars ⋯).toSubfield = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A
have rw₃ : B = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
rw₁ : extendScalars ⋯ = ⊥ ↔ B ≤ A
rw₂ : (extendScalars ⋯).toSubfield = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₃ : B = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A
have rw₄ : B = RingHom.fieldRange (K := ↥(A ⊓ B)) (algebraMap (↥(A ⊓ B)) E) ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
rw₁ : extendScalars ⋯ = ⊥ ↔ B ≤ A
rw₂ : (extendScalars ⋯).toSubfield = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₃ : B = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₄ : B = RingHom.fieldRange (K := ↥(A ⊓ B)) (algebraMap (↥(A ⊓ B)) E) ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A
have rw₅ : B = (A ⊓ B).subtype.fieldRange ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
rw₁ : extendScalars ⋯ = ⊥ ↔ B ≤ A
rw₂ : (extendScalars ⋯).toSubfield = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₃ : B = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₄ : B = RingHom.fieldRange (K := ↥(A ⊓ B)) (algebraMap (↥(A ⊓ B)) E) ↔ B ≤ A
rw₅ : B = (A ⊓ B).subtype.fieldRange ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A
have rw₆ : B = A ⊓ B ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = 1 ↔ B ≤ A
rw₁ : extendScalars ⋯ = ⊥ ↔ B ≤ A
rw₂ : (extendScalars ⋯).toSubfield = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₃ : B = IntermediateField.toSubfield (K := ↥(A ⊓ B)) ⊥ ↔ B ≤ A
rw₄ : B = RingHom.fieldRange (K := ↥(A ⊓ B)) (algebraMap (↥(A ⊓ B)) E) ↔ B ≤ A
rw₅ : B = (A ⊓ B).subtype.fieldRange ↔ B ≤ A
rw₆ : B = A ⊓ B ↔ B ≤ A
⊢ A.relrank B = 1 ↔ B ≤ A
have rw₇ : B ≤ A ↔ B ≤ A
Tactic: rw [relrank, IntermediateField.rank_eq_one_iff, ← IntermediateField.toSubfield_inj,
    extendScalars_toSubfield, IntermediateField.bot_toSubfield, algebraMap_ofSubfield,
    fieldRange_subtype, right_eq_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
⊢ A.relfinrank B = 1 ↔ B ≤ A
have rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (A.relrank B) : ℕ) (1 : ℕ) ↔ B ≤ A
Tactic: rw [relfinrank_eq_toNat_relrank, toNat_eq_one, relrank_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (A.relrank B) : ℕ) (1 : ℕ) ↔ B ≤ A
⊢ A.relfinrank B = 1 ↔ B ≤ A
have rw₁ : A.relrank B = 1 ↔ B ≤ A
Tactic: rw [relfinrank_eq_toNat_relrank, toNat_eq_one, relrank_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (A.relrank B) : ℕ) (1 : ℕ) ↔ B ≤ A
rw₁ : A.relrank B = 1 ↔ B ≤ A
⊢ A.relfinrank B = 1 ↔ B ≤ A
have rw₂ : B ≤ A ↔ B ≤ A
Tactic: rw [relfinrank_eq_toNat_relrank, toNat_eq_one, relrank_eq_one_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E
have rw : Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E
Tactic: rw [relrank_eq_rank_of_le h]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (hypothesis)
Goal:
E : Type v
inst : Field E
A B : Subfield E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank ↥A ↥(extendScalars h) * Module.rank (↥B) E = Module.rank (↥A) E
have this₁ : IsScalarTower (↥A) (↥B) E
Tactic: haveI : IsScalarTower A B E := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A : Subfield E
x : AddCommMonoid ↥⊤ := inferInstance
⊢ A.relrank ⊤ = Module.rank (↥A) E
have rw : Module.rank ↥A ↥(extendScalars (E := ⊤) sorry) = Module.rank (↥A) E
Tactic: rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,
    IntermediateField.topEquiv.toLinearEquiv.rank_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A : Subfield E
x : AddCommMonoid ↥⊤ := inferInstance
rw : Module.rank ↥A ↥(extendScalars (E := ⊤) ⋯) = Module.rank (↥A) E
⊢ A.relrank ⊤ = Module.rank (↥A) E
have rw₁ : Module.rank ↥A ↥⊤ = Module.rank (↥A) E
Tactic: rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,
    IntermediateField.topEquiv.toLinearEquiv.rank_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ A.relrank ⊤ = Module.rank (↥A) E
have rw₂ : Module.rank (↥A) E = Module.rank (↥A) E
Tactic: rw [relrank_eq_rank_of_le (show A ≤ ⊤ from le_top), extendScalars_top,
    IntermediateField.topEquiv.toLinearEquiv.rank_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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 ⊓ map f B) : Subring L)
have rw : Eq.{w + 1} (α := Subring L) (Subring.map f (A ⊓ B).toSubring : Subring L) (toSubring (map f (A ⊓ B)) : Subring L)
Tactic: rw [← map_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A : Subfield E
f : L →+* E
B : Subfield L
⊢ map.{w, v} (K := L) f (comap f A) ⊓ map f B = A ⊓ map f B
have rw : A ⊓ RingHom.fieldRange.{w, v} (K := L) f ⊓ map f B = A ⊓ map f B
Tactic: rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ map.{w, v} (K := L) f (comap f A) ⊓ map f B = A ⊓ map f B
have rw₁ : A ⊓ map.{w, v} (K := L) f ⊤ ⊓ map f B = A ⊓ map f B
Tactic: rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ map.{w, v} (K := L) f (comap f A) ⊓ map f B = A ⊓ map f B
have rw₂ : A ⊓ (map.{w, v} (K := L) f ⊤ ⊓ map f B) = A ⊓ map f B
Tactic: rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ map.{w, v} (K := L) f (comap f A) ⊓ map f B = A ⊓ map f B
have rw₃ : A ⊓ map f (⊤ ⊓ B) = A ⊓ map f B
Tactic: rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ map.{w, v} (K := L) f (comap f A) ⊓ map f B = A ⊓ map f B
have rw₄ : A ⊓ map f B = A ⊓ map f B
Tactic: rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
| lift.{v, w} (relrank (E := L) (comap f A) (comap f B))
have rw : lift.{w, v} ((A ⊓ RingHom.fieldRange.{w, v} (K := L) f).relrank (B ⊓ RingHom.fieldRange.{w, v} (K := L) f))
Tactic: rw [← lift_relrank_map_map _ _ f, map_comap_eq, map_comap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
⊢ 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))
have 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))
Tactic: conv_lhs => rw [← lift_relrank_map_map _ _ f, map_comap_eq, map_comap_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
⊢ 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))
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
⊢ (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)
have 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)
Tactic: apply relrank_eq_of_inf_eq
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
L : Type w
inst_1 : Field L
A B : Subfield E
f : L →+* E
⊢ 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)
have 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)
Tactic: rw [inf_assoc, inf_left_comm _ B, inf_of_le_left (le_refl _)]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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 ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f) =
    A ⊓ (B ⊓ RingHom.fieldRange.{w, v} (K := L) f)
have 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)
Tactic: rw [inf_assoc, inf_left_comm _ B, inf_of_le_left (le_refl _)]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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)
⊢ 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)
have e_c₂ : A ⊓ (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 _)]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (hypothesis)
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C
have h3 : A ≤ C
Tactic: have h3 := h1.trans h2
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B C : Subfield E
h1 : A ≤ B
h2 : B ≤ C
h3 : A ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C
have rw : Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)
Tactic: rw [relrank_eq_rank_of_le h1, relrank_eq_rank_of_le h2, relrank_eq_rank_of_le h3]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (hypothesis)
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
⊢ Module.rank ↥A ↥(extendScalars h1) * Module.rank ↥B ↥(extendScalars h2) = Module.rank ↥A ↥(extendScalars h3)
have this₁ : IsScalarTower.{v, v, v} ↥A ↥B ↥C
Tactic: haveI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
E : Type v
inst : Field E
A B C : Subfield E
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
have rw : (A ⊓ (B ⊓ C)).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]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
have rw₁ : (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * (B ⊓ C).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]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
have rw₂ : (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * (B ⊓ C).relrank C = (A ⊓ B ⊓ C).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]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
have rw₃ : (A ⊓ (B ⊓ C)).relrank (B ⊓ C) * (B ⊓ C).relrank C = (A ⊓ (B ⊓ C)).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]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
have rw₄ : (A ⊓ (B ⊓ C)).relrank C = (A ⊓ (B ⊓ C)).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]