mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inl.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ 1 + 1 ≠ c ^ n

Tactic:
hc

Goal state after:
case neg.inl.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ 1 + 1 ≠ -1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inl.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ 1 + -1 ≠ c ^ n

Tactic:
hc

Goal state after:
case neg.inl.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ 1 + -1 ≠ 1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inl.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ 1 + -1 ≠ c ^ n

Tactic:
hc

Goal state after:
case neg.inl.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = 1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ 1 + -1 ≠ -1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inr.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = 1
⊢ -1 + 1 ≠ c ^ n

Tactic:
hc

Goal state after:
case neg.inr.inl.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = 1
⊢ -1 + 1 ≠ 1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inr.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ -1 + 1 ≠ c ^ n

Tactic:
hc

Goal state after:
case neg.inr.inl.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = 1
hc : c ^ n = -1
⊢ -1 + 1 ≠ -1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inr.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ -1 + -1 ≠ c ^ n

Tactic:
hc

Goal state after:
case neg.inr.inr.inl
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = 1
⊢ -1 + -1 ≠ 1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case neg.inr.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ -1 + -1 ≠ c ^ n

Tactic:
hc

Goal state after:
case neg.inr.inr.inr
n : ℕ
tfae_2_iff_1 : FermatLastTheoremWith' ℕ n ↔ FermatLastTheoremFor n
a b c : ℤ
hn : ¬n = 0
ha : a ^ n = -1
hb : b ^ n = -1
hc : c ^ n = -1
⊢ -1 + -1 ≠ -1
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
⊢ c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

Tactic:
hc

Goal state after:
n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ n + b ^ n ≠ c ^ n
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ 1

Tactic:
← Hgcd

Goal state after:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ {a, b, c}.gcd id
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0

Tactic:
by
  classical
  let S : Set ℕ := { n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2 }
  have S_nonempty : S.Nonempty := by
    use Int.natAbs c
    rw [Set.mem_ofPred_eq]
    use ⟨a, ⟨b, c⟩⟩
  let m : ℕ := Nat.find S_nonempty
  have m_mem : m ∈ S := Nat.find_spec S_nonempty
  rcases m_mem with ⟨s0, hs0, hs1⟩
  use s0.1, s0.2.1, s0.2.2, hs0
  intro a1 b1 c1 h1
  rw [← hs1]
  apply Nat.find_min'
  use ⟨a1, ⟨b1, c1⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ False

Tactic:
have hpc : (p : ℤ) ^ 2 ∣ c := by
    rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]
    apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
    ring

Goal state after:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
hpc : ↑p ^ 2 ∣ c
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
simp [h0, hz]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ x.gcd y ≠ 0

Tactic:
hc

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 1 ≠ 0
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x = 0
⊢ h.IsPrimitiveClassified

Tactic:
subst x

Goal state after:
y z : ℤ
h : PythagoreanTriple 0 y z
hc : Int.gcd 0 y = 1
⊢ h.IsPrimitiveClassified
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
set w := wronskian a b with wab

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
⊢ a.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧
      b.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∧ c.natDegree + 1 ≤ (radical (a * b * c)).natDegree ∨
    derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case cons
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih : (↑s).Pairwise (Function.onFun IsRelPrime f) → radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i)
h : (insert i ↑s).Pairwise (Function.onFun IsRelPrime f)
⊢ radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)

Tactic:
Set.pairwise_insert_of_symm_of_notMem <| by simpa

Goal state after:
case cons
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih : (↑s).Pairwise (Function.onFun IsRelPrime f) → radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i)
h : (↑s).Pairwise (Function.onFun IsRelPrime f) ∧ ∀ b ∈ ↑s, Function.onFun IsRelPrime f i b
⊢ radical (f i * ∏ i ∈ s, f i) = radical (f i) * ∏ i ∈ s, radical (f i)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 0
⊢ m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0

Tactic:
apply Or.intro_right
      exact And.intro hm2 hn2

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
set ι : K → K.topologicalClosure := ⇑(Subfield.inclusion K.le_topologicalClosure)

Goal state after:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} • I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' :
  Submodule.map (Algebra.linearMap R K) (Ideal.span {↑I.den} • I₀) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {↑a} • I.num)
⊢ (Algebra.linearMap R K).ker = ⊥

Tactic:
smul_eq_mul

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} * I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' :
  Submodule.map (Algebra.linearMap R K) (Ideal.span {↑I.den} • I₀) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {↑a} • I.num)
⊢ (Algebra.linearMap R K).ker = ⊥
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
contrapose hφ

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (mk φ).embedding
⊢ ComplexEmbedding.IsReal φ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ #({w.embedding} ∪ {w.embedding}) = 1

Tactic:
Finset.union_idempotent,

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsReal
⊢ #{w.embedding} = 1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ ↑k

Tactic:
exact orderOf_dvd_of_pow_eq_one h

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ c ≠ 0 →
    a ^ n + b ^ n = c ^ n → ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
hc

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a ^ n + b ^ n = c ^ n → ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: case inl
F : Type u_1
inst✝⁴ : Field F
K : Type u_2
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : Algebra.IsAlgebraic ℚ K
ι : Type u_3
k : ι → Subfield K
inst✝ : ∀ (i : ι), IsTotallyReal ↥(k i)
hι : IsEmpty ι
⊢ IsTotallyReal ↥(⨆ i, k i)

Tactic:
rw [iSup_of_empty]
    infer_instance

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : ∃ σ, ComplexEmbedding.IsConj w.embedding σ
⊢ Nat.card ↑↑(Stab (mk w.embedding)) = 1 ∨ Nat.card ↑↑(Stab (mk w.embedding)) = 2

Tactic:
obtain ⟨σ, hσ⟩ := h
    rw [hσ.coe_stabilizer_mk]
    simp

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
i : ChooseBasisIndex ℤ ↥↑↑I
⊢ (fractionalIdealLatticeBasis K I) i = (mixedEmbedding K) ((basisOfFractionalIdeal K I) i)

Tactic:
by
  simp only [fractionalIdealLatticeBasis, Basis.coe_reindex, Basis.coe_mk, Function.comp_apply,
    Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∈ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
exact hy.2 w

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
exact hy.2 w

Goal state after:
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
⊢ (aeval d) (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) q)) = 0

Tactic:
q,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
⊢ (aeval d) (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) (p.comp (C a * X)))) = 0
Module: Mathlib.RingTheory.LocalRing.Quotient

Goal state before:
pp: case mp.hN'
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalRing R
inst✝ : Module.Finite R S
s : Set S
H :
  Submodule.restrictScalars R (span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s)) =
    map (↑(IsScalarTower.toAlgHom R S (S ⧸ pS))) (span R s)
hs : span (R ⧸ p) (⇑(Ideal.Quotient.mk pS) '' s) = ⊤
⊢ ⊤.FG

Tactic:
exact Module.finite_def.mp ‹_›

Goal state after:
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := ⋯
Sₚ : Type u_2 := ⋯
this✝⁷ : Algebra Rₚ Sₚ := ⋯
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (equivQuotMaximalIdeal p Rₚ) ((trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x)) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))

Tactic:
trace_quotient_eq_trace_localization_quotient S p Rₚ Sₚ,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (equivQuotMaximalIdeal p Rₚ)
      ((equivQuotMaximalIdeal p Rₚ).symm ((trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap S (Sₚ ⧸ pSₚ)) x))) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (equivQuotMaximalIdeal p Rₚ)
      ((equivQuotMaximalIdeal p Rₚ).symm
        ((trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((algebraMap Sₚ (Sₚ ⧸ pSₚ)) ((algebraMap S Sₚ) x)))) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))

Tactic:
Ideal.Quotient.algebraMap_eq,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (equivQuotMaximalIdeal p Rₚ)
      ((equivQuotMaximalIdeal p Rₚ).symm
        ((trace (Rₚ ⧸ maximalIdeal Rₚ) (Sₚ ⧸ pSₚ)) ((Ideal.Quotient.mk pSₚ) ((algebraMap S Sₚ) x)))) =
    (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ((intTrace R S) x))
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_2
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁸ : CommRing A
inst✝¹⁷ : IsDomain A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : IsDomain B
inst✝¹⁴ : Algebra A B
inst✝¹³ : IsTorsionFree A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra A K
inst✝⁹ : Algebra B L
inst✝⁸ : IsFractionRing A K
inst✝⁷ : IsFractionRing B L
I : FractionalIdeal A⁰ K
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : Algebra.IsIntegral A B
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsIntegrallyClosed B
x : K
hx₁ : x ∈ I
hx₂ : x ∉ 1
⊢ (algebraMap K L) x ∉ 1

Tactic:
contrapose hx₂
    rw [mem_one_iff, ← IsIntegrallyClosed.isIntegral_iff] at hx₂ ⊢
    exact IsIntegral.tower_bot_of_field <| isIntegral_trans _ hx₂

Goal state after: