how to change sth to instance?

Stream: new members

[Chengyan Hu]

Hi! It seems like I have a million have in my proof, and they are all fundamental properties. Is it possible to change for example the lemma here to an automatically loaded instance or something?
As my code is too long, I only put the lemma in my first have here , the theorem part might not run, please let me know if it's better for me to ask the question in some different way:

import Mathlib
open Ideal Padic Nat
open scoped algebraMap
lemma isDomain_of_faithfulSMul (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] : IsDomain B :=
  Function.Injective.isDomain (algebraMap B L) <| by
  rwa [← faithfulSMul_iff_algebraMap_injective B L]

lemma faithfulSMul_of_isIntegralClosure (A B L : Type*) [CommRing A] [CommSemiring B] [CommRing L]
    [Algebra A L] [Algebra B L] [IsIntegralClosure B A L] : FaithfulSMul B L where
  eq_of_smul_eq_smul {b₁ b₂} h := by
    apply IsIntegralClosure.algebraMap_injective B A L
    simp [Algebra.algebraMap_eq_smul_one, h 1]

theorem cyclo_thing:
  ((cyclotomicCharacter L l (MulSemiringAction.toRingEquiv G L F)) : ℤ_[l]) =
  Nat.card (A ⧸ I.under A) := by
  set q:= ↑(Nat.card (A ⧸ under A I))
  set g:= (MulSemiringAction.toRingEquiv G L F)
  rw[← PadicInt.ext_of_toZModPow]
  intro i
  have := faithfulSMul_of_isIntegralClosure A B L
  have := isDomain_of_faithfulSMul B L
  have := enough_pow_root_L A K L B I l hlp
  simp
  obtain ⟨ζ,hζ⟩ := enough_pow_root_B A K L B I l hlp i
  have foo: (ζ:L)= algebraMap B L (ζ:B):= rfl
  have hζ': IsPrimitiveRoot (ζ:L) (l ^ i):= foo2 (ζ:B) (ζ:L) foo hζ

  have good_Andrew : g ζ = (ζ ^ q : B) := by
    have tauto: (F • ζ : B) = g ζ := algebraMap.coe_smul G B L F ζ
    rw [←tauto, ←AlgHom.IsArithFrobAt.apply_of_pow_eq_one hF hζ.pow_eq_one (pow_not_in I l hlp i)]
    simp
  have pow_eq: (ζ:L)^q = ζ^( (cyclotomicCharacter L l g).val.toZModPow i).val := by
    rw[← cyclotomicCharacter.spec l g ↑ζ hζ'.pow_eq_one,good_Andrew]
    exact Eq.symm (algebraMap.coe_pow ζ q)
  rw[pow_eq_ex_eq' (ζ:L) (l^i) hζ' (a := q)
    (b := ((cyclotomicCharacter L l g).val.toZModPow i).val)] at pow_eq
  simp at pow_eq
  exact id (Eq.symm pow_eq)

[Aaron Liu]

Make them instances? If for some reason that's not desirable you can also make them local

[Aaron Liu]

You can also just try deleting some of the haves

[Chengyan Hu]

Aaron Liu said:

Make them instances? If for some reason that's not desirable you can also make them local

I'm confusing how to write this 2 lemma into instance, simply writing istance gives an error:

cannot find synthesization order for instance isDomain_of_faithfulSMul with type
  ∀ (B : Type u_1) (L : Type u_2) [inst : CommRing B] [inst_1 : CommRing L] [IsDomain L] [inst_3 : Algebra B L]
    [FaithfulSMul B L], IsDomain B
all remaining arguments have metavariables:
  CommRing ?L
  @IsDomain ?L CommRing.toCommSemiring.toSemiring
  @Algebra B ?L CommRing.toCommSemiring CommRing.toCommSemiring.toSemiring
  @FaithfulSMul B ?L Algebra.toSMul

[Aaron Liu]

oh

[Aaron Liu]

that makes sense

[Chengyan Hu]

Aaron Liu said:

You can also just try deleting some of the haves

Ah, it helps a bit, I succeed deleted one, but only one lol

[Kenny Lau]

@Chengyan Hu those are non-decreasing instances so it would be dangerous to Lean. but a way to get around it might be to assume more instances for the lemma, and only remove those assumptions in the final theorem.

Another approach which I've considered is to bundle the K L A B into one structure so you can add more instances. but the drawback is that you won't be able to refer them as K L A B any more, but rather as something like s.K, s.L, s.A, and s.B (s is an arbitrary variable name).

[Kenny Lau]

@Chengyan Hu here is a demonstration of the first approach:

import Mathlib

lemma isDomain_of_faithfulSMul (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] : IsDomain B :=
  ((faithfulSMul_iff_algebraMap_injective B L).1 ‹_›).isDomain

-- Note the extra [IsDomain B] assumption at the end
lemma some_useful_lemma (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] [IsDomain B] :
    ∀ b : B, ∃ l : L, algebraMap B L (b + 1) = l := sorry

-- Now note that we don't need that assumption here.
theorem main_theorem (B L : Type*) [CommRing B] [CommRing L] [IsDomain L]
    [Algebra B L] [FaithfulSMul B L] : ∀ b : B, ∃ l : L, algebraMap B L b + 1 = l := by
  have := isDomain_of_faithfulSMul B L -- and we only derive it at the main theorem.
  intro b
  obtain ⟨l, hl⟩ := some_useful_lemma B L b
  exact ⟨l, by simpa using hl⟩

[Kenny Lau]

@Chengyan Hu and here is a demonstration of the second approach:

import Mathlib

structure AKLB where
  (A K L B : Type*)
  [crA : CommRing A] [fK : Field K] [fL : Field L] [crB : CommRing B]
  [aAK: Algebra A K] [aKL : Algebra K L] [aAB : Algebra A B] [aBL : Algebra B L] [aAL : Algebra A L]
  [sAKL : IsScalarTower A K L] [sABL : IsScalarTower A B L]
  [fAK : FaithfulSMul A K]
  [fBL : FaithfulSMul B L]
  [acKL : IsAlgClosure K L]
  [iAB : IsIntegralClosure B A L]

variable (s : AKLB)

namespace AKLB

attribute [instance] crA fK fL crB aAK aKL aAB aBL aAL sAKL sABL fAK fBL acKL iAB

instance : IsDomain s.B :=
  ((faithfulSMul_iff_algebraMap_injective s.B s.L).1 inferInstance).isDomain

lemma some_useful_lemma : ∀ b : s.B, ∃ l : s.L, algebraMap s.B s.L (b + 1) = l := sorry

theorem main_theorem : ∀ b : s.B, ∃ l : s.L, algebraMap s.B s.L b + 1 = l := by
  intro b
  obtain ⟨l, hl⟩ := s.some_useful_lemma b
  exact ⟨l, by simpa using hl⟩

end AKLB

[Chengyan Hu]

The second one sounds like a really good idea! I’m a bit confused about the first one though — it seems quite similar to the approach I originally had?