awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : K
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (x + y)) :
      ℝ≥0)
    (max
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x))
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)
have h_mono : Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal sorry) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
Tactic: have h_mono := (toNNReal_strictMono hb).monotone
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
x y : K
h_mono :
  Monotone (α := WithZero (Multiplicative ℤ)) (β := ℝ≥0) (⇑(toNNReal ⋯) : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
⊢ LE.le (α := ℝ≥0)
    ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (x + y)) :
      ℝ≥0)
    (max
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x))
        ((toNNReal ⋯ : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
          (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y)) :
      ℝ≥0)
have rw : LE.le (α := ℝ≥0)
  ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (x + y)) :
    ℝ≥0)
  ((toNNReal sorry : (a : WithZero (Multiplicative ℤ)) → ℝ≥0)
      (max (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x)
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) y)) :
    ℝ≥0)
Tactic: rw [← h_mono.map_max]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LE.le (α := ℝ) ((v.adicAbv hb : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) r : K) : ℝ) (1 : ℝ)
have rw : LE.le (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ)
Tactic: rw [adicAbv_of_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ LT.lt (α := ℝ) ((v.adicAbv hb : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) r : K) : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal
have rw : LT.lt (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∈ v.asIdeal
Tactic: rw [adicAbv_of_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ Eq (α := ℝ) ((v.adicAbv hb : (a : K) → ℝ) ((algebraMap R K : (a : R) → K) r : K) : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal
have rw : Eq (α := ℝ) ((v.intAdicAbv hb : (a : R) → ℝ) r : ℝ) (1 : ℝ) ↔ r ∉ v.asIdeal
Tactic: rw [adicAbv_of_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((valuation ℚ 𝔭 : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    (↑x.den : R) ∉ 𝔭.asIdeal
have this : CharZero R
Tactic: have : CharZero R := ⟨.of_comp (f := algebraMap R ℚ) (by simpa using Nat.cast_injective)⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (hypothesis)
Goal:
R : Type u_4
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
𝔭 : HeightOneSpectrum R
x : ℚ
this : CharZero R
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((valuation ℚ 𝔭 : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    (↑x.den : R) ∉ 𝔭.asIdeal
have this₁ : Ne.{u_4 + 1} (α := R) (↑x.den : R) 0
Tactic: have : (x.den : R) ≠ 0 := by simp
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
⊢ P.IsMaximal
have rw : IsMaximal (comap e.symm P)
Tactic: rw [← Ideal.map_comap_eq_self_of_equiv e.symm P,
      Ideal.isMaximal_map_iff_of_bijective _ e.symm.bijective]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
hA : DimensionLEOne A
e : R ≃+* A
P : Ideal R
hP_ne : P ≠ ⊥
hP_prime : P.IsPrime
⊢ IsMaximal (comap e.symm P)
have apply : Ne (α := Ideal A) (comap e.symm P) ⊥
Tactic: apply Ring.DimensionLEOne.maximalOfPrime ?_ (P.comap_isPrime e.symm)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
⊢ Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}
have this : IsDomain R
Tactic: have : IsDomain R := .of_faithfulSMul R A
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
⊢ Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}
have refine_1 : Set.Nonempty (α := Ideal A) (p.primesOver A)
Tactic: refine Set.eq_singleton_iff_nonempty_unique_mem.mpr ⟨?_, fun P hP ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
refine_1 : Set.Nonempty (α := Ideal A) (p.primesOver A)
⊢ Eq (α := Set (Ideal A)) (p.primesOver A) {maximalIdeal A}
have refine_2 : ∀ (P : Ideal A) (hP : Membership.mem (γ := Set (Ideal A)) (p.primesOver A) P), P = maximalIdeal A
Tactic: refine Set.eq_singleton_iff_nonempty_unique_mem.mpr ⟨?_, fun P hP ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : IsLocalRing A
inst_3 : IsDedekindDomain A
inst_4 : Algebra R A
inst_5 : FaithfulSMul R A
inst_6 : Module.Finite R A
p : Ideal R
inst_7 : p.IsMaximal
hp0 : p ≠ ⊥
this : IsDomain R
⊢ Set.Nonempty (α := Ideal A) (p.primesOver A)
have refine_1 : ∀ (w' : Ideal A) (hmax : w'.IsMaximal) (hover : w'.LiesOver p), Set.Nonempty (α := Ideal A) (p.primesOver A)
Tactic: obtain ⟨w', hmax, hover⟩ := exists_maximal_ideal_liesOver_of_isIntegral (S := A) p
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I : Submodule B L
c : B
x : L
hx :
  x ∈
    (toAddSubmonoid
        (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (S := K) (traceForm K L) (restrictScalars A I))).carrier
a : L
ha : Membership.mem (γ := Submodule A L) (restrictScalars A I) a
⊢ Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
    ((((traceForm K L : (a : L) → L →ₗ[K] K) (c • x) : L →ₗ[K] K) : (a : L) → K) a : K)
have rw : Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1 ((Algebra.trace K L : (a : L) → K) (x * c • a) : K)
Tactic: rw [traceForm_apply, smul_mul_assoc, mul_comm, ← smul_mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔
    LE.le (α := Submodule A K)
      (map
        ((↑A :
            {S : Type u_2} →
              {M : Type u} →
                {M₂ : Type u_2} →
                  [inst : Semiring A] →
                    [inst_11 : Semiring S] →
                      [inst_12 : AddCommMonoid M] →
                        [inst_13 : AddCommMonoid M₂] →
                          [inst_14 : Module A M] →
                            [inst_15 : Module A M₂] →
                              [inst_16 : Module S M] →
                                [inst_17 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
          (Algebra.trace K L))
        (restrictScalars A (I * J)))
      1
have rw : I ≤ Jᵛ ↔
  ∀ (m : L),
    Membership.mem (γ := Submodule A L) (restrictScalars A I) m →
      ∀ (n : L),
        Membership.mem (γ := Submodule A L) (restrictScalars A J) n →
          Membership.mem (γ := Submodule A L)
            (comap
              ((↑A :
                  {S : Type u_2} →
                    {M : Type u} →
                      {M₂ : Type u_2} →
                        [inst : Semiring A] →
                          [inst_11 : Semiring S] →
                            [inst_12 : AddCommMonoid M] →
                              [inst_13 : AddCommMonoid M₂] →
                                [inst_14 : Module A M] →
                                  [inst_15 : Module A M₂] →
                                    [inst_16 : Module S M] →
                                      [inst_17 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
                (Algebra.trace K L))
              1)
            (m * n)
Tactic: rw [Submodule.map_le_iff_le_comap, Submodule.restrictScalars_mul, Submodule.mul_le]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I J J' : Submodule B L
⊢ I ≤ (J * J')ᵛ ↔ I * J ≤ J'ᵛ
have simp_rw : LE.le (α := Submodule A K)
    (map
      ((↑A :
          {S : Type u_2} →
            {M : Type u} →
              {M₂ : Type u_2} →
                [inst : Semiring A] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module A M] →
                          [inst_15 : Module A M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
        (Algebra.trace K L))
      (restrictScalars A (I * (J * J'))))
    1 ↔
  LE.le (α := Submodule A K)
    (map
      ((↑A :
          {S : Type u_2} →
            {M : Type u} →
              {M₂ : Type u_2} →
                [inst : Semiring A] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module A M] →
                          [inst_15 : Module A M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ A S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[A] M₂)
        (Algebra.trace K L))
      (restrictScalars A (I * J * J')))
    1
Tactic: simp_rw [le_traceDual_iff_map_le_one, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ I * J ≤ 1ᵛ
have rw : I ≤ Jᵛ ↔ I ≤ (J * 1)ᵛ
Tactic: rw [← le_traceDual_mul_iff, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I J : Submodule B L
rw : I ≤ Jᵛ ↔ I ≤ (J * 1)ᵛ
⊢ I ≤ Jᵛ ↔ I * J ≤ 1ᵛ
have rw₁ : I ≤ Jᵛ ↔ I ≤ Jᵛ
Tactic: rw [← le_traceDual_mul_iff, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ J ≤ Iᵛ
have rw : I * J ≤ 1ᵛ ↔ J ≤ Iᵛ
Tactic: rw [le_traceDual, mul_comm, ← le_traceDual]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I J : Submodule B L
rw : I * J ≤ 1ᵛ ↔ J ≤ Iᵛ
⊢ I ≤ Jᵛ ↔ J ≤ Iᵛ
have rw₁ : J * I ≤ 1ᵛ ↔ J ≤ Iᵛ
Tactic: rw [le_traceDual, mul_comm, ← le_traceDual]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
I J : Submodule B L
rw : I * J ≤ 1ᵛ ↔ J ≤ Iᵛ
rw₁ : J * I ≤ 1ᵛ ↔ J ≤ Iᵛ
⊢ I ≤ Jᵛ ↔ J ≤ Iᵛ
have rw₂ : J ≤ Iᵛ ↔ J ≤ Iᵛ
Tactic: rw [le_traceDual, mul_comm, ← le_traceDual]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_4
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : FiniteDimensional K L
inst_12 : Algebra.IsSeparable K L
I : Submodule B L
ι : Type u_3
inst_13 : Finite ι
inst_14 : DecidableEq ι
b : Basis ι K L
hb : Eq (α := Submodule A L) (restrictScalars A I) (span A (Set.range.{u, u_3 + 1} (ι := ι) (⇑b : (a : ι) → L)))
⊢ Eq (α := Submodule A L) (restrictScalars A Iᵛ) (span A (Set.range.{u, u_3 + 1} (ι := ι) (⇑b.traceDual : (a : ι) → L)))
have rw : Eq.{u + 1} (α := Submodule A L)
  (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (S := K) (M := L) (traceForm K L)
      (span A (Set.range.{u, u_3 + 1} (ι := ι) (⇑b : (a : ι) → L))) :
    Submodule A L)
  (span A (Set.range.{u, u_3 + 1} (ι := ι) (⇑b.traceDual : (a : ι) → L)) : Submodule A L)
Tactic: rw [restrictScalars_traceDual, hb]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
⊢ Eq.{u + 1} (α := Submodule B L) ⊥ᵛ ⊤
have h : ∀ (x : L), Membership.mem (γ := Submodule B L) ⊥ᵛ x ↔ Membership.mem (γ := Submodule B L) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ
    (if LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1 then ⊤ else ⊥)
have pos : ∀ (h : LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1),
  Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊤
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
pos :
  ∀ (h : LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1),
    Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊤
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ
    (if LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1 then ⊤ else ⊥)
have neg : ∀ (h : ¬LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1),
  Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
h : LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊤
have pos : LE.le.{u} (α := Submodule B L) ⊤ ⊤ᵛ
Tactic: rw [_root_.eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
h : ¬LE.le (α := Submodule A K) (restrictScalars A (LinearMap.range (Algebra.trace K L))) 1
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥
have h₁ : ∃ (x : L),
  ∀ (x_1 : A), ¬Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x_1 : K) ((Algebra.trace K L : (a : L) → K) x : K)
Tactic: simp only [SetLike.le_def, restrictScalars_mem, LinearMap.mem_range, mem_one,
      forall_exists_index, forall_apply_eq_imp_iff, not_forall, not_exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
h :
  ∃ (x : L),
    ∀ (x_1 : A),
      ¬Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x_1 : K) ((Algebra.trace K L : (a : L) → K) x : K)
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥
have neg : ∀ (b : L)
  (hb :
    ∀ (x : A), ¬Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((Algebra.trace K L : (a : L) → K) b : K)),
  Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥
Tactic: obtain ⟨b, hb⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((Algebra.trace K L : (a : L) → K) b : K)
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥
have neg : ∀ ⦃x : L⦄,
  (∀ (a : L),
      ∃ (x_1 : A),
        Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
          ((Algebra.trace K L : (a : L) → K) (x * a) : K)) →
    x = 0
Tactic: simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies,
      traceForm_apply, RingHom.mem_range]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((Algebra.trace K L : (a : L) → K) b : K)
⊢ ∀ ⦃x : L⦄,
    (∀ (a : L),
        ∃ (x_1 : A),
          Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
            ((Algebra.trace K L : (a : L) → K) (x * a) : K)) →
      x = 0
have neg : ∀
  (hx' :
    ∃ (x : L),
      (∀ (a : L),
          ∃ (x_1 : A),
            Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
              ((Algebra.trace K L : (a : L) → K) (x * a) : K)) ∧
        x ≠ 0),
  ∃ (x : A), Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((Algebra.trace K L : (a : L) → K) b : K)
Tactic: contrapose! hb with hx'
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
b : L
hx' :
  ∃ (x : L),
    (∀ (a : L),
        ∃ (x_1 : A),
          Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x_1 : K)
            ((Algebra.trace K L : (a : L) → K) (x * a) : K)) ∧
      x ≠ 0
⊢ ∃ (x : A), Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((Algebra.trace K L : (a : L) → K) b : K)
have neg : ∀ (c : L)
  (hc :
    ∀ (a : L),
      ∃ (x : A),
        Eq.{u_2 + 1} (α := K) (((algebraMap A K : A →+* K) : (a : A) → K) x : K)
          ((Algebra.trace K L : (a : L) → K) (c * a) : K))
  (hc0 : c ≠ 0),
  ∃ (x : A), Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((Algebra.trace K L : (a : L) → K) b : K)
Tactic: obtain ⟨c, hc, hc0⟩ := hx'
Cleared hypotheses: hx'