-- Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean
theorem discr_eq_discr_of_algEquiv {L : Type*} [Field L] [NumberField L] (f : K ≃ₐ[ℚ] L) :
    discr K = discr L

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = (algebraMap ℤ ℚ) (Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))

Tactic:
rw [← Algebra.discr_localizationLocalization ℤ (nonZeroDivisors ℤ) L]

Result:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) =
    Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀))

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
⊢ discr K = discr L

Tactic:
let f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (f.restrictScalars ℤ).mapIntegralClosure.toLinearEquiv

Result:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ discr K = discr L

Proof state:
case e_b
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ ⇑f ∘ ⇑(integralBasis K) = ⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀))

Tactic:
ext

Result:
case e_b.h
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
x✝ : Module.Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (⇑f ∘ ⇑(integralBasis K)) x✝ =
    (Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀)) x✝

Proof state:
case e_b.h
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
x✝ : Module.Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ f ((algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) x✝)) = (algebraMap (𝓞 L) L) (f₀ ((RingOfIntegers.basis K) x✝))

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) =
    Algebra.discr ℚ ⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀))

Tactic:
congr

Result:
case e_b
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ ⇑f ∘ ⇑(integralBasis K) = ⇑(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀))

Proof state:
case e_b.h
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
x✝ : Module.Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (⇑f ∘ ⇑(integralBasis K)) x✝ =
    (Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) L ((RingOfIntegers.basis K).map f₀)) x✝

Tactic:
simp only [Function.comp_apply, integralBasis_apply, Basis.localizationLocalization_apply,
  Basis.map_apply]

Result:
case e_b.h
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
x✝ : Module.Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ f ((algebraMap (𝓞 K) K) ((RingOfIntegers.basis K) x✝)) = (algebraMap (𝓞 L) L) (f₀ ((RingOfIntegers.basis K) x✝))

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = ↑(Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))

Tactic:
change _ = algebraMap ℤ ℚ _

Result:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = (algebraMap ℤ ℚ) (Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ discr K = discr L

Tactic:
rw [← Rat.intCast_inj, coe_discr, Algebra.discr_eq_discr_of_algEquiv (integralBasis K) f,
  ← discr_eq_discr L ((RingOfIntegers.basis K).map f₀)]

Result:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
L : Type u_2
inst✝¹ : Field L
inst✝ : NumberField L
f : K ≃ₐ[ℚ] L
f₀ : 𝓞 K ≃ₗ[ℤ] 𝓞 L := (AlgEquiv.restrictScalars ℤ f).mapIntegralClosure.toLinearEquiv
⊢ Algebra.discr ℚ (⇑f ∘ ⇑(integralBasis K)) = ↑(Algebra.discr ℤ ⇑((RingOfIntegers.basis K).map f₀))