awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : (i : Fin n) → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R :=
  HSub.hSub (α := Matrix (Fin n) (Fin n) R) (β := Matrix (Fin n) (Fin n) R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) A' : Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), Eq.{v + 1} (α := S ⧸ M) (∑ j : Fin n, A i j • a j) 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
span_d : Submodule.restrictScalars R (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) ≤ M
x : L
hx :
  Membership.mem (γ := Submodule L L)
    (span (singleton (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) A.det : S) : L))) x
⊢ Membership.mem (γ := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) x

Tactic:
IsFractionRing.ideal_span_singleton_map_subset R hRL span_d hx

Premises used: Set.Mem, setOf, IsFractionRing.ideal_span_singleton_map_subset
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
smul_top_eq : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ (a' : Fin n → R), (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i : Fin n, a' i • a i = x
A' : (i : Fin n) → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1 : Fin n, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R :=
  HSub.hSub (α := Matrix (Fin n) (Fin n) R) (β := Matrix (Fin n) (Fin n) R)
    ((Matrix.of : (a : Fin n → Fin n → R) → Matrix (Fin n) (Fin n) R) A' : Matrix (Fin n) (Fin n) R)
    (1 : Matrix (Fin n) (Fin n) R)
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), Eq.{v + 1} (α := S ⧸ M) (∑ j : Fin n, A i j • a j) 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
span_d : Submodule.restrictScalars R (Submodule.span S (singleton (α := S) ((f : (a : R) → S) A.det : S))) ≤ M
x : L
hx :
  Membership.mem (γ := Submodule L L)
    (span (singleton (α := L) ((algebraMap S L : (a : S) → L) ((f : (a : R) → S) A.det : S) : L))) x
⊢ Membership.mem (γ := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) x

Tactic:
exact IsFractionRing.ideal_span_singleton_map_subset R hRL span_d hx

Premises used: IsFractionRing.ideal_span_singleton_map_subset
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb' : LinearIndependent.{u_6, v, u_4} S (M := V') ((⇑f' : (a : V'') → V') ∘ b)
contrapose :
  ∀ (hb : ¬LinearIndependent.{u_6, u_1, u_3} K (M := V) ((⇑F : (a : V'') → V) ∘ b)),
    ¬LinearIndependent.{u_6, v, u_4} S (M := V') ((⇑f' : (a : V'') → V') ∘ b)
⊢ LinearIndependent.{u_6, u_1, u_3} K (M := V) ((⇑F : (a : V'') → V) ∘ b)

Tactic:
contrapose hb' with hb
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb : ¬LinearIndependent.{u_6, u_1, u_3} K (M := V) ((⇑F : (a : V'') → V) ∘ b)
simp :
  ∀
    (hb :
      ∃ (x : Finset ι) (x_1 : ι → K) (_ :
        Eq.{u_3 + 1} (α := V) (∑ i ∈ x, HSMul.hSMul (β := V) (x_1 i) (((⇑F : (a : V'') → V) ∘ b) i)) 0) (x_2 : ι) (_ :
        x_2 ∈ x), ¬x_1 x_2 = 0),
    ∃ (x : Finset ι) (x_1 : ι → S) (_ :
      Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
      x_2 ∈ x), ¬x_1 x_2 = 0
⊢ ¬LinearIndependent.{u_6, v, u_4} S (M := V') ((⇑f' : (a : V'') → V') ∘ b)

Tactic:
simp only [linearIndependent_iff', not_forall] at hb ⊢

Premises used: linearIndependent_iff', Classical.not_forall
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb :
  ∃ (x : Finset ι) (x_1 : ι → K) (_ :
    Eq.{u_3 + 1} (α := V) (∑ i ∈ x, HSMul.hSMul (β := V) (x_1 i) (((⇑F : (a : V'') → V) ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0
obtain :
  ∀ (s : Finset ι) (g : ι → K)
    (eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0) (j' : ι)
    (hj's : j' ∈ s) (hj'g : ¬g j' = 0),
    ∃ (x : Finset ι) (x_1 : ι → S) (_ :
      Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
      x_2 ∈ x), ¬x_1 x_2 = 0
⊢ ∃ (x : Finset ι) (x_1 : ι → S) (_ :
    Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0

Tactic:
obtain ⟨s, g, eq, j', hj's, hj'g⟩ := hb
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
h :
  ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
⊢ ∃ (x : Finset ι) (x_1 : ι → S) (_ :
    Eq.{u_4 + 1} (α := V') (∑ i ∈ x, HSMul.hSMul (β := V') (x_1 i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0) (x_2 : ι) (_ :
    x_2 ∈ x), ¬x_1 x_2 = 0

Tactic:
use s
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
h :
  ∀ (a : K) (hag : ∀ i ∈ s, IsLocalization.IsInteger R (a * g i)) (j : ι) (hjs : j ∈ s)
    (hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)),
    ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
      (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0

Tactic:
obtain ⟨a, hag, j, hjs, hgI⟩ := Ideal.exist_integer_multiples_notMem hRS s g hj's hj'g

Premises used: Ideal.exist_integer_multiples_notMem
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
hag : ∀ i ∈ s, IsLocalization.IsInteger R (a * g i)
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
h :
  ∀ (g'' : (i : ι) → i ∈ s → R) (hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i),
    ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
      (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0

Tactic:
choose g'' hg'' using hag
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
i : ι
hi : i ∈ s
⊢ (algebraMap R K : (a : R) → K) (g' i) = a * g i

Tactic:
(congr_arg _ (dif_pos hi)).trans (hg'' i hi)

Premises used: dif_pos, congr_arg, Eq.trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
i : ι
hi : i ∈ s
⊢ (algebraMap R K : (a : R) → K) (g' i) = a * g i

Tactic:
exact (congr_arg _ (dif_pos hi)).trans (hg'' i hi)

Premises used: dif_pos, congr_arg, Eq.trans
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
⊢ ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i

Tactic:
have hg' : ∀ i ∈ s, algebraMap _ _ (g' i) = a * g i := by
    intro i hi; exact (congr_arg _ (dif_pos hi)).trans (hg'' i hi)
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
⊢ ∀ (x : R), (algebraMap R K : (a : R) → K) x = a * g j → x ∉ RingHom.ker (F := R →+* S) f

Tactic:
simp only [FractionalIdeal.mem_coeIdeal, not_exists, not_and'] at hgI

Premises used: not_exists, FractionalIdeal.mem_coeIdeal, not_and'
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : ∀ (x : R), (algebraMap R K : (a : R) → K) x = a * g j → x ∉ RingHom.ker (F := R →+* S) f
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)

Tactic:
hgI _ (hg' j hjs)

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : ∀ (x : R), (algebraMap R K : (a : R) → K) x = a * g j → x ∉ RingHom.ker (F := R →+* S) f
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)

Tactic:
exact hgI _ (hg' j hjs)
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
⊢ Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)

Tactic:
have hgI : algebraMap R S (g' j) ≠ 0 := by
    simp only [FractionalIdeal.mem_coeIdeal, not_exists, not_and'] at hgI
    exact hgI _ (hg' j hjs)
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst_5 : AddCommGroup V
inst_6 : Module R V
inst_7 : Module K V
inst_8 : IsScalarTower R K V
inst_9 : AddCommGroup V'
inst_10 : Module R V'
inst_11 : Module S V'
inst_12 : IsScalarTower R S V'
inst_13 : AddCommGroup V''
inst_14 : Module R V''
hRK : IsFractionRing R K
inst_15 : IsDedekindDomain R
hRS : Ne (α := Ideal R) (RingHom.ker (F := R →+* S) f) ⊤
F : V'' →ₗ[R] V
hf : Function.Injective.{u_5 + 1, u_3 + 1} (α := V'') (β := V) (⇑F : (a : V'') → V)
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : Eq.{u_3 + 1} (α := V) (∑ i ∈ s, HSMul.hSMul (β := V) (g i) (((⇑F : (a : V'') → V) ∘ b) i)) 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI_1 : a * g j ∉ (↑(RingHom.ker (F := R →+* S) f) : FractionalIdeal R⁰ K)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K : (a : R) → K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : (i : ι) → R := fun (i : ι) ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K : (a : R) → K) (g' i) = a * g i
hgI : Ne.{v + 1} (α := S) ((f : (a : R) → S) (g' j) : S) (0 : S)
⊢ ∃ (x : ι → S) (_ : Eq.{u_4 + 1} (α := V') (∑ i ∈ s, HSMul.hSMul (β := V') (x i) (((⇑f' : (a : V'') → V') ∘ b) i)) 0)
    (x_1 : ι) (_ : x_1 ∈ s), ¬x x_1 = 0

Tactic:
⟨fun i => algebraMap R S (g' i), ?_, j, hjs, hgI⟩

Premises used: Algebra.algebraMap, Exists.intro, DFunLike.coe