Theorem: Weight.gcd_eq_one_of_in_M (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
⊢ Finset.gcd Finset.univ w = 1
Tactic:
set g := Finset.univ.gcd w
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
⊢ g = 1

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
⊢ g = 1
Tactic:
by_contra hfg
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ False

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ False
Tactic:
have hg : 1 < g
State after:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ 1 < g

n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
⊢ False

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
⊢ False
Tactic:
let w' : Weight n d := fun i ↦ (w i) / g
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ False

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ False
Tactic:
have hww' : w = g • w'
State after:
case hww'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ w = g • w'

n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
⊢ False

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
⊢ False
Tactic:
have hww'i i : w i = g * w' i := congrFun hww' i
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ False

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ False
Tactic:
refine (not_in_M_of_dom_ne ⟨w', ⟨?_, ?_⟩, ?_, ?_⟩) hM
State after:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' 0 = 0

case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone w'

case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≤ w

case refine_4
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≠ w

State before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ 1 < g
Tactic:
refine lt_of_le_of_ne (Nat.one_le_iff_ne_zero.mpr ?_) (Ne.symm hfg)
State after:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ g ≠ 0

State before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
⊢ g ≠ 0
Tactic:
by_contra! hg
State after:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ False

State before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ False
Tactic:
have h₀' : w = 0
State after:
case h₀'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ w = 0

case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
h₀' : w = 0
⊢ False

State before:
case hg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
h₀' : w = 0
⊢ False
Tactic:
exact h₀ h₀'
State after:
no goals

State before:
case h₀'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
⊢ w = 0
Tactic:
ext
State after:
case h₀'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
i✝ : Fin (Nat.succ n)
⊢ w i✝ = 0 i✝

State before:
case h₀'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : g = 0
i✝ : Fin (Nat.succ n)
⊢ w i✝ = 0 i✝
Tactic:
simp only [Finset.mem_univ, Finset.gcd_eq_zero_iff.mp hg, zero_apply]
State after:
no goals

State before:
case hww'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
⊢ w = g • w'
Tactic:
ext i
State after:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (g • w') i

State before:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (g • w') i
Tactic:
simp only [Pi.smul_apply, Algebra.id.smul_eq_mul]
State after:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (Finset.gcd Finset.univ w • fun i => w i / Finset.gcd Finset.univ w) i

State before:
case hww'.h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
i : Fin (Nat.succ n)
⊢ w i = (Finset.gcd Finset.univ w • fun i => w i / Finset.gcd Finset.univ w) i
Tactic:
exact (Nat.mul_div_cancel_left' (Finset.gcd_dvd (Finset.mem_univ i))).symm
State after:
no goals

State before:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' 0 = 0
Tactic:
simp only
State after:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w 0 / Finset.gcd Finset.univ w = 0

State before:
case refine_1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w 0 / Finset.gcd Finset.univ w = 0
Tactic:
rw [hM.1.1, Nat.zero_div]
State after:
no goals

State before:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone w'
Tactic:
simp only
State after:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone fun i => w i / Finset.gcd Finset.univ w

State before:
case refine_2
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ Monotone fun i => w i / Finset.gcd Finset.univ w
Tactic:
exact fun i j hij ↦ Nat.div_le_div_right (hM.1.2 hij)
State after:
no goals

State before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≤ w
Tactic:
rw [hww', dom_iff]
State after:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ f w' ≤ f (g • w')

State before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ f w' ≤ f (g • w')
Tactic:
have := f_le_mul w' g.pred
State after:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
this : f w' ≤ f (Nat.succ (Nat.pred g) • w')
⊢ f w' ≤ f (g • w')

State before:
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
this : f w' ≤ f (Nat.succ (Nat.pred g) • w')
⊢ f w' ≤ f (g • w')
Tactic:
rwa [Nat.succ_pred_eq_of_pos (zero_lt_one.trans hg)] at this
State after:
no goals

State before:
case refine_4
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ w' ≠ w
Tactic:
obtain ⟨i, hi⟩ : ∃ i, w i ≠ 0 := by by_contra! hf; exact h₀ (funext hf)
State after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
⊢ w' ≠ w

State before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
⊢ w' ≠ w
Tactic:
have hi' : w' i ≠ 0 := fun hf ↦ hi <| mul_zero g ▸ hf ▸ hww'i i
State after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
⊢ w' ≠ w

State before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
⊢ w' ≠ w
Tactic:
intro hf
State after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = w
⊢ False

State before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = w
⊢ False
Tactic:
rw [hww'] at hf
State after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
⊢ False

State before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
⊢ False
Tactic:
have h₁ := congr_fun hf i
State after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = (g • w') i
⊢ False

State before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = (g • w') i
⊢ False
Tactic:
rw [smul_apply] at h₁
State after:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = g * w' i
⊢ False

State before:
case refine_4.intro
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
i : Fin (Nat.succ n)
hi : w i ≠ 0
hi' : w' i ≠ 0
hf : w' = g • w'
h₁ : w' i = g * w' i
⊢ False
Tactic:
exact hfg (mul_right_cancel₀ hi' ((one_mul _).trans h₁)).symm
State after:
no goals

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
⊢ ∃ i, w i ≠ 0
Tactic:
by_contra! hf
State after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
hf : ∀ (i : Fin (Nat.succ n)), w i = 0
⊢ False

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h₀ : w ≠ 0
hM : w ∈ M n d
g : ℕ := Finset.gcd Finset.univ w
hfg : ¬g = 1
hg : 1 < g
w' : Weight n d := fun i => w i / g
hww' : w = g • w'
hww'i : ∀ (i : Fin (Nat.succ n)), w i = g * w' i
hf : ∀ (i : Fin (Nat.succ n)), w i = 0
⊢ False
Tactic:
exact h₀ (funext hf)
State after:
no goals