awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 ((Algebra.trace K L : (a : L) → K) (x * c • a) : K)

Tactic:
exact hx _ (Submodule.smul_mem _ c ha)

Premises used: Submodule.smul_mem
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
x : L
⊢ x ∈ Iᵛ ↔
    ∀ a ∈ I,
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) a : K)

Tactic:
forall₂_congr fun _ _ ↦ mem_one

Premises used: Set.Mem, setOf, forall₂_congr, Submodule.mem_one
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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ᵛ ↔
    ∀ (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)
⊢ 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

Tactic:
rw [Submodule.map_le_iff_le_comap, Submodule.restrictScalars_mul, Submodule.mul_le]

Premises used: Submodule.restrictScalars_mul, Submodule.mul_le, Submodule.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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ᵛ ↔
    ∀ (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:
simp [SetLike.le_def, mem_traceDual]

Premises used: SetLike.le_def, Submodule.mem_traceDual
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
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
⊢ I ≤ (J * J')ᵛ ↔ I * J ≤ J'ᵛ

Tactic:
simp_rw [le_traceDual_iff_map_le_one, mul_assoc]

Premises used: mul_assoc, Submodule.le_traceDual_iff_map_le_one
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)ᵛ
rw₁ rw₂ : I ≤ Jᵛ ↔ I ≤ Jᵛ
⊢ I ≤ Jᵛ ↔ I * J ≤ 1ᵛ

Tactic:
rw [← le_traceDual_mul_iff, mul_one]

Premises used: Submodule.le_traceDual_mul_iff, mul_one
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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ᵛ
rw₂ rw₃ : J ≤ Iᵛ ↔ J ≤ Iᵛ
⊢ I ≤ Jᵛ ↔ J ≤ Iᵛ

Tactic:
rw [le_traceDual, mul_comm, ← le_traceDual]

Premises used: Submodule.le_traceDual, mul_comm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ I ≤ Iᵛᵛ

Tactic:
le_traceDual_comm.mpr le_rfl

Premises used: Iff.mpr, le_rfl, Submodule.le_traceDual_comm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ Eq (α := Submodule A L) (restrictScalars A Iᵛ)
    (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (S := K) (traceForm K L) (restrictScalars A I))

Tactic:
rfl

Premises used: Submodule.restrictScalars, setOf, LinearMap.BilinForm.dualSubmodule, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)))
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)
⊢ Eq (α := Submodule A L) (restrictScalars A Iᵛ) (span A (Set.range.{u, u_3 + 1} (ι := ι) (⇑b.traceDual : (a : ι) → L)))

Tactic:
rw [restrictScalars_traceDual, hb]

Premises used: Submodule.restrictScalars_traceDual
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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.{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:
(traceForm K L).dualSubmodule_span_of_basis (traceForm_nondegenerate K L) b

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, traceForm_nondegenerate, Algebra.traceForm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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.{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:
exact (traceForm K L).dualSubmodule_span_of_basis (traceForm_nondegenerate K L) b

Premises used: LinearMap.BilinForm.dualSubmodule_span_of_basis, traceForm_nondegenerate, Algebra.traceForm
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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), Membership.mem (γ := Submodule B L) ⊥ᵛ x ↔ Membership.mem (γ := Submodule B L) ⊤ x
⊢ Eq.{u + 1} (α := Submodule B L) ⊥ᵛ ⊤

Tactic:
ext
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
x : L
⊢ Membership.mem (γ := Submodule B L) ⊥ᵛ x ↔ Membership.mem (γ := Submodule B L) ⊤ x

Tactic:
simp [mem_traceDual, -RingHom.mem_range]

Premises used: RingHom.mem_range, Submodule.mem_traceDual
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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) ⊤ᵛ ⊤
neg :
  ∀ (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 ⊥)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
pos : LE.le.{u} (α := Submodule B L) ⊤ ⊤ᵛ
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊤

Tactic:
rw [_root_.eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ LE.le.{u} (α := Submodule B L) ⊤ ⊤ᵛ

Tactic:
fun _ _ _ _ ↦ h ⟨_, rfl⟩

Premises used: AlgHom.toLinearMap, Algebra.lmul, Set.Mem, setOf, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ LE.le.{u} (α := Submodule B L) ⊤ ⊤ᵛ

Tactic:
exact fun _ _ _ _ ↦ h ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
⊢ ∃ (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

Premises used: SetLike.le_def, forall_exists_index, not_exists, LinearMap.mem_range, Submodule.mem_one, Submodule.restrictScalars_mem, forall_apply_eq_imp_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
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) ⊤ᵛ ⊥
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥

Tactic:
obtain ⟨b, hb⟩ := h
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
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
⊢ Eq.{u + 1} (α := Submodule B L) ⊤ᵛ ⊥

Tactic:
simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies,
      traceForm_apply, RingHom.mem_range]

Premises used: RingHom.mem_range, Algebra.traceForm_apply, Submodule.mem_bot, SetLike.le_def, true_implies, Submodule.mem_traceDual, eq_bot_iff, Submodule.mem_top
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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)
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)
⊢ ∀ ⦃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:
contrapose! hb with hx'
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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
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)
⊢ ∃ (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'
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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 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:
simpa [hc0] using hc (c⁻¹ * b)

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.RingTheory.DedekindDomain.Different
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) ⊤ᵛ ⊤
neg neg₁ :
  ∀ (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 ⊥)

Tactic:
classical
  split_ifs with h
  · rw [_root_.eq_top_iff]
    exact fun _ _ _ _ ↦ h ⟨_, rfl⟩
  · 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
    obtain ⟨b, hb⟩ := h
    simp_rw [eq_bot_iff, SetLike.le_def, mem_bot, mem_traceDual, mem_top, true_implies,
      traceForm_apply, RingHom.mem_range]
    contrapose! hb with hx'
    obtain ⟨c, hc, hc0⟩ := hx'
    simpa [hc0] using hc (c⁻¹ * b)

Premises used: eq_top_iff, RingHom.mem_range, Algebra.traceForm_apply, Submodule.mem_bot, SetLike.le_def, forall_exists_index, not_exists, LinearMap.mem_range, Submodule.mem_one, true_implies, Submodule.restrictScalars_mem, Submodule.mem_traceDual, eq_bot_iff, forall_apply_eq_imp_iff, Classical.not_forall, Submodule.mem_top