-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma Submodule.one_le_traceDual_one :
    (1 : Submodule B L) ≤ 1ᵛ

Proof state:
case 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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ ∃ y, (algebraMap A K) y = (↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x)

Tactic:
apply IsIntegrallyClosed.isIntegral_iff.mp

Result:
case 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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ IsIntegral A ((↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x))

Proof state:
case 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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ (↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x) ∈ 1

Tactic:
rw [mem_one]

Result:
case 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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ ∃ y, (algebraMap A K) y = (↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x)

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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ map (↑A (Algebra.trace K L)) (restrictScalars A (LinearMap.range (Algebra.linearMap B L))) ≤ 1

Tactic:
rintro _ ⟨x, ⟨x, rfl⟩, rfl⟩

Result:
case 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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ (↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x) ∈ 1

Proof state:
case intro.intro.intro.hx
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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ IsIntegral A ((Algebra.linearMap B L) x)

Tactic:
rw [IsIntegralClosure.isIntegral_iff (A := B)]

Result:
case intro.intro.intro.hx
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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ ∃ y, (algebraMap B L) y = (Algebra.linearMap B L) x

Proof state:
case intro.intro.intro.hx
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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ ∃ y, (algebraMap B L) y = (Algebra.linearMap B L) x

Tactic:
exact ⟨_, 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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ 1 ≤ 1ᵛ

Tactic:
rw [le_traceDual_iff_map_le_one, mul_one, one_eq_range]

Result:
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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
⊢ map (↑A (Algebra.trace K L)) (restrictScalars A (LinearMap.range (Algebra.linearMap B L))) ≤ 1

Proof state:
case 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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ IsIntegral A ((↑A (Algebra.trace K L)) ((Algebra.linearMap B L) x))

Tactic:
apply isIntegral_trace

Result:
case intro.intro.intro.hx
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
inst✝³ : IsFractionRing A K
inst✝² : IsIntegrallyClosed A
inst✝¹ : FiniteDimensional K L
inst✝ : IsIntegralClosure B A L
x : B
⊢ IsIntegral A ((Algebra.linearMap B L) x)