-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma traceDual_top' :
    (⊤ : Submodule B L)ᵛ =
      if ((LinearMap.range (Algebra.trace K L)).restrictScalars A ≤ 1) then ⊤ else ⊥

Proof state:
case neg.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ∀ ⦃x : L⦄, (∀ (a : L), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (x * a)) → x = 0

Tactic:
contrapose! hb with hx'

Result:
case neg.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hx' : ∃ x, (∀ (a : L), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (x * a)) ∧ x ≠ 0
⊢ ∃ x, (algebraMap A K) x = (Algebra.trace K L) b

Proof state:
case neg.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hx' : ∃ x, (∀ (a : L), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (x * a)) ∧ x ≠ 0
⊢ ∃ x, (algebraMap A K) x = (Algebra.trace K L) b

Tactic:
obtain ⟨c, hc, hc0⟩ := hx'

Result:
case neg.intro.intro.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b c : L
hc : ∀ (a : L), ∃ x, (algebraMap A K) x = (Algebra.trace K L) (c * a)
hc0 : c ≠ 0
⊢ ∃ x, (algebraMap A K) x = (Algebra.trace K L) b

Proof state:
case pos
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1
⊢ ⊤ ≤ ⊤ᵛ

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

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
⊢ ⊤ᵛ = if restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1 then ⊤ else ⊥

Tactic:
split_ifs with h

Result:
case pos
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1
⊢ ⊤ᵛ = ⊤

case neg
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : ¬restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1
⊢ ⊤ᵛ = ⊥

Proof state:
case neg
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : ¬restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1
⊢ ⊤ᵛ = ⊥

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

Result:
case neg
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : ∃ x, ∀ (x_1 : A), ¬(algebraMap A K) x_1 = (Algebra.trace K L) x
⊢ ⊤ᵛ = ⊥

Proof state:
case neg.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ⊤ᵛ = ⊥

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

Result:
case neg.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ∀ ⦃x : L⦄, (∀ (a : L), ∃ x_1, (algebraMap A K) x_1 = (Algebra.trace K L) (x * a)) → x = 0

Proof state:
case pos
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1
⊢ ⊤ᵛ = ⊤

Tactic:
rw [_root_.eq_top_iff]

Result:
case pos
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : restrictScalars A (LinearMap.range (Algebra.trace K L)) ≤ 1
⊢ ⊤ ≤ ⊤ᵛ

Proof state:
case neg.intro.intro.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b c : L
hc : ∀ (a : L), ∃ x, (algebraMap A K) x = (Algebra.trace K L) (c * a)
hc0 : c ≠ 0
⊢ ∃ x, (algebraMap A K) x = (Algebra.trace K L) b

Tactic:
simpa [hc0] using hc (c⁻¹ * b)

Result:
no goals

Proof state:
case neg
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
h : ∃ x, ∀ (x_1 : A), ¬(algebraMap A K) x_1 = (Algebra.trace K L) x
⊢ ⊤ᵛ = ⊥

Tactic:
obtain ⟨b, hb⟩ := h

Result:
case neg.intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
b : L
hb : ∀ (x : A), ¬(algebraMap A K) x = (Algebra.trace K L) b
⊢ ⊤ᵛ = ⊥