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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
⊢ logHeight (x ∘ ⇑e) = logHeight x

Tactic:
by
  simp only [logHeight_eq_log_mulHeight, mulHeight_comp_equiv]

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
i : Fin 2
⊢ v (![x, 1] i) = ![v x, 1] i

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x✝ : K
v : AbsoluteValue K ℝ
x : K
⊢ v (![x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![v x, 1] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
i : Fin (Nat.succ 0).succ
⊢ (x • ![x⁻¹, 1]) i = ![1, x] i

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun i ↦ i) ⟨0, ⋯⟩) = ![1, x] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
⊢ (x • ![x⁻¹, 1]) ((fun i ↦ i) ⟨1, ⋯⟩) = ![1, x] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod ≤
    (map (fun x ↦ ↑(Nat.card ι)) archAbsVal).prod *
      (map (fun i ↦ (⨆ i_1, i (x i_1)) * ⨆ i_1, i (A i_1)) archAbsVal).prod

Tactic:
← prod_map_mul

Goal state after:
case h₁
K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ (map (fun v ↦ ⨆ i, v (∑ i_1, A (i, i_1) * x i_1)) archAbsVal).prod ≤
    (map (fun i ↦ ↑(Nat.card ι) * ((⨆ i_1, i (x i_1)) * ⨆ i_1, i (A i_1))) archAbsVal).prod
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
i : Fin (Nat.succ 0).succ
⊢ ![x ^ n, 1] i = (![x, 1] ^ n) i

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℕ
⊢ ![x ^ n, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (![x, 1] ^ n) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N

Tactic:
grw [AbsoluteValue.sum_le]

Goal state after:
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ ∑ i ∈ p.support, v (coeff i p * ∏ i_1 ∈ i.support, x i_1 ^ i i_1) ≤
    ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: ⊢ FermatLastTheoremFor 3

Tactic:
by
  let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]

Goal state after:
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
i : Fin (Nat.succ 0).succ
⊢ ![x * y, 1] i = (![x, 1] * ![y, 1]) i

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun i ↦ i) ⟨0, ⋯⟩) = (![x, 1] * ![y, 1]) ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ![x * y, 1] ((fun i ↦ i) ⟨1, ⋯⟩) = (![x, 1] * ![y, 1]) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤
    (Multiset.map (Function.const (AbsoluteValue K ℝ) ↑(#s)) archAbsVal).prod *
        (Multiset.map (fun i ↦ ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod *
      ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1

Tactic:
← prod_map_mul

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤
    (Multiset.map (fun i ↦ Function.const (AbsoluteValue K ℝ) (↑(#s)) i * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod *
      ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    ((Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
        ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) *
      ((Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N

Tactic:
rw [mul_pow, mul_mul_mul_comm]

Goal state after:
case inr.inr
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
        (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod ^ N *
      ((∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) *
        (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₁
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
      (Multiset.map (fun i ↦ (⨆ i_1, i (x i_1)) ^ N) archAbsVal).prod

Tactic:
← prod_map_mul

Goal state after:
case h₁
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod ≤
    (Multiset.map (fun i ↦ (⨆ j, (p j).coeff.sum fun x c ↦ i c) * (⨆ i_1, i (x i_1)) ^ N) archAbsVal).prod
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = (Multiset.map (fun x ↦ 1) archAbsVal).sum

Tactic:
← Multiset.sum_map_toList,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = (List.map (fun x ↦ 1) archAbsVal.toList).sum
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ completedRiemannZeta₀ (1 - 0) = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
simp [completedRiemannZeta₀_one]

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inl
K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : IsEmpty ι'
⊢ (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

Tactic:
simp [show q = 0 from Subsingleton.elim .., max_mulHeightBound_zero_one_eq_one K ι (ι × ι'),
      mulHeight_eval_ge_aux p h]
    grind [zero_pow_eq]

Goal state after:
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬y = -1
⊢ ¬y = 1 + y

Tactic:
right_eq_add

Goal state after:
case refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
y : F
hy : ¬y = -1
⊢ ¬1 = 0
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case e'_2.e'_5
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
i : Fin (Nat.succ 0).succ × Fin (Nat.succ 0).succ
⊢ ![a, b] i.1 * ![c, d] i.2 = (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) i

Tactic:
fin_cases i

Goal state after:
case e'_2.e'_5.«0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩)

case e'_2.e'_5.«1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨0, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩)

case e'_2.e'_5.«2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨0, ⋯⟩)

case e'_2.e'_5.«3»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
a b c d : K
hab : ![a, b] ≠ 0
hcd : ![c, d] ≠ 0
⊢ ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).1 * ![c, d] ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩).2 =
    (![a * c, a * d, b * c, b * d] ∘ ⇑finProdFinEquiv) ((fun i ↦ i) ⟨1, ⋯⟩, (fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
i : Fin 3
⊢ (p i).IsHomogeneous 1

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨0, ⋯⟩)).IsHomogeneous 1

case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨1, ⋯⟩)).IsHomogeneous 1

case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
⊢ (p ((fun i ↦ i) ⟨2, ⋯⟩)).IsHomogeneous 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] i = 0 i

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ ![0 * c, 0 * d + 0 * c, 0 * d] ((fun i ↦ i) ⟨2, ⋯⟩) = 0 ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case h₂
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
i : Fin (Nat.succ 0).succ
⊢ x✝ ↑(![a, ↑n] i) = x✝ (![↑a, ↑n] i)

Tactic:
fin_cases i

Goal state after:
case h₂.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ x✝ ↑(![a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)) = x✝ (![↑a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩))

case h₂.«1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
x✝ : FinitePlace K
⊢ x✝ ↑(![a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)) = x✝ (![↑a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case pos
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ![a, b] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

pp: case neg
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]

Tactic:
· rw [hab, mulHeight_zero, mul_one, show a = 0 from congrFun hab 0,
      show b = 0 from congrFun hab 1,
      show ![0 * c, 0 * d + 0 * c, 0 * d] = 0 by ext i; fin_cases i <;> simp, mulHeight_zero]
    grw [← one_le_mulHeight]
    grind

Goal state after:
case neg
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![a, b] * mulHeight ![c, d]
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
i : Fin 2
⊢ ↑(![a, ↑n] i) = ![↑a, ↑n] i

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
⊢ ↑(![a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)) = ![↑a, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
⊢ ↑(![a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)) = ![↑a, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![a * 0, a * 0 + b * 0, b * 0] i = 0 i

Tactic:
fin_cases i

Goal state after:
case «0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

case «2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ![c, d] = 0
⊢ ![a * 0, a * 0 + b * 0, b * 0] ((fun i ↦ i) ⟨2, ⋯⟩) = 0 ((fun i ↦ i) ⟨2, ⋯⟩)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case e'_3
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
i : Fin (Nat.succ 0).succ.succ
⊢ ![a * c, a * d + b * c, b * d] i = (eval ![a * c, a * d, b * c, b * d]) (p i)

Tactic:
fin_cases i

Goal state after:
case e'_3.«0»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨0, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨0, ⋯⟩))

case e'_3.«1»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨1, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨1, ⋯⟩))

case e'_3.«2»
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
a b c d : K
hab : ¬![a, b] = 0
hcd : ¬![c, d] = 0
⊢ ![a * c, a * d + b * c, b * d] ((fun i ↦ i) ⟨2, ⋯⟩) = (eval ![a * c, a * d, b * c, b * d]) (p ((fun i ↦ i) ⟨2, ⋯⟩))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_2
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
i : Fin (Nat.succ 0).succ
⊢ ![↑q.num, ↑↑q.den] i = (Int.cast ∘ ![q.num, ↑q.den]) i

Tactic:
fin_cases i

Goal state after:
case e'_2.«0»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ![↑q.num, ↑↑q.den] ((fun i ↦ i) ⟨0, ⋯⟩) = (Int.cast ∘ ![q.num, ↑q.den]) ((fun i ↦ i) ⟨0, ⋯⟩)

case e'_2.«1»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ![↑q.num, ↑↑q.den] ((fun i ↦ i) ⟨1, ⋯⟩) = (Int.cast ∘ ![q.num, ↑q.den]) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ↑↑(max q.num.natAbs q.den) = ↑(⨆ i, |![q.num, ↑q.den] i|)

Tactic:
Int.cast_inj

Goal state after:
case e'_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ ↑(max q.num.natAbs q.den) = ⨆ i, |![q.num, ↑q.den] i|
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_3.refine_3
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
i : Fin 2
⊢ |![q.num, ↑q.den] i| ≤ max |q.num| ↑q.den

Tactic:
fin_cases i

Goal state after:
case e'_3.refine_3.«0»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |![q.num, ↑q.den] ((fun i ↦ i) ⟨0, ⋯⟩)| ≤ max |q.num| ↑q.den

case e'_3.refine_3.«1»
q : ℚ
this : Finset.univ.gcd ![q.num, ↑q.den] = 1
⊢ |![q.num, ↑q.den] ((fun i ↦ i) ⟨1, ⋯⟩)| ≤ max |q.num| ↑q.den