variable scope in a long function

Stream: new members

[Xipan Xiao]

I have a long theorem, and created a hypothesis at the beginning:

  have m_div_n : m ∣ n := by
    refine addOrderOf_dvd_iff_nsmul_eq_zero.mpr ?_
    exact nx'

At the end of the theorem

  have n_div_m: n ∣ m := by
    refine addOrderOf_dvd_iff_nsmul_eq_zero.mpr ?_
    exact mx_quotient_is_zero

  have m_eq_n : m = n := by exact Nat.dvd_antisymm m_div_n n_div_m

Lean complained that m_div_n is unknown:
unknown identifier 'm_div_n'Lean 4
and I had to repeat the m_div_n proof like:

  have m_eq_n : m = n := by -- exact Nat.dvd_antisymm m_div_n n_div_m
    have m_div_n : m ∣ n := by
      refine addOrderOf_dvd_iff_nsmul_eq_zero.mpr ?_
      exact nx'
    exact Nat.dvd_antisymm m_div_n n_div_m

Why this is the case? The complete code is also pasted here:

import Mathlib
import Mathlib.GroupTheory.OrderOfElement
import Mathlib.Algebra.Group.Defs

open scoped Classical

open AddSubgroup

variable {G : Type*} [AddCommGroup G]

/-- A subgroup `S` is pure in `G` if whenever `n • x ∈ S`, there exists `y ∈ S` such that `n • x = n • y`. -/
def isPure (S : AddSubgroup G) : Prop :=
  ∀ (x : G) (n : ℕ), n ≠ 0 → n • x ∈ S → ∃ y ∈ S, n • x = n • y

def order_lifting (S : AddSubgroup G) : Prop :=
  ∀ x : G,
    let n := addOrderOf (QuotientAddGroup.mk' S x)
    ∃ y : G, QuotientAddGroup.mk' S y = QuotientAddGroup.mk' S x ∧ addOrderOf y = n


theorem order_lifting_if_purity (S : AddSubgroup G) : isPure S → order_lifting S := by
  intro h x
  let n := addOrderOf (QuotientAddGroup.mk' S x)
  have nx_zero : n • (QuotientAddGroup.mk' S x) = 0 := by
    refine addOrderOf_nsmul_eq_zero (QuotientAddGroup.mk' S x)

  have hn : n ≠ 0 := by sorry
  have hnx : n • x ∈ S := by
    refine (QuotientAddGroup.eq_zero_iff (n • x)).mp ?_
    exact nx_zero


  obtain ⟨y, hyS, hxy⟩ := h x n hn hnx

  have pi_y_zero : QuotientAddGroup.mk' S y = 0 := by
    refine AddMonoidHom.mem_ker.mp ?_
    apply QuotientAddGroup.eq_iff_sub_mem.mpr
    rw [sub_zero]
    exact hyS

  let x' := x - y
  use x'
  constructor
  -- show QuotientAddGroup.mk' S x' = QuotientAddGroup.mk' S x
  calc
    QuotientAddGroup.mk' S x' = QuotientAddGroup.mk' S (x - y) := by exact rfl
    _ = QuotientAddGroup.mk' S x - QuotientAddGroup.mk' S y := by exact rfl
    _ = QuotientAddGroup.mk' S x - 0 := by exact congrArg (HSub.hSub ((QuotientAddGroup.mk' S) x)) pi_y_zero
    _ = QuotientAddGroup.mk' S x := by exact sub_zero _
  -- show addOrderOf x' = n
  have nx' : n • x' = 0 := by
    calc
      n • x' = n • (x - y) := by exact rfl
      _ = n • x - n • y := by rw [nsmul_sub]
      _ = 0 := by exact sub_eq_zero_of_eq hxy

  let m := addOrderOf x'
  have mx'_zero : m • x' = 0 := by refine addOrderOf_nsmul_eq_zero x'

  have m_div_n : m ∣ n := by
    refine addOrderOf_dvd_iff_nsmul_eq_zero.mpr ?_
    exact nx'

  obtain ⟨k, hk⟩ := m_div_n
  have nkm : n = k * m := by rw [hk, Nat.mul_comm]
  have mx_eq_my : m • x = m • y := by
    calc
      m • x = m • (x - y + y) := by simp
      _ = m • x' + m • y := by rw [nsmul_add]
      _ = 0 + m • y := by rw [mx'_zero]
      _ = m • y := by exact zero_add _
  have mx_in_S : m • x ∈ S := by
    rw [mx_eq_my]
    exact AddSubgroup.nsmul_mem S hyS m
  have mx_quotient_is_zero : QuotientAddGroup.mk' S (m • x) = 0 := by
    refine AddMonoidHom.mem_ker.mp ?_
    apply QuotientAddGroup.eq_iff_sub_mem.mpr
    refine AddSubgroup.sub_mem S mx_in_S ?_
    exact AddSubgroup.zero_mem S

  have n_div_m: n ∣ m := by
    refine addOrderOf_dvd_iff_nsmul_eq_zero.mpr ?_
    exact mx_quotient_is_zero

  have m_eq_n : m = n := by -- exact Nat.dvd_antisymm m_div_n n_div_m
    have m_div_n : m ∣ n := by
      refine addOrderOf_dvd_iff_nsmul_eq_zero.mpr ?_
      exact nx'
    exact Nat.dvd_antisymm m_div_n n_div_m

  exact m_eq_n

[Aaron Liu]

You cleared out m_div_n when running obtain ⟨k, hk⟩ := m_div_n.

[Aaron Liu]

To keep it, you can obtain ⟨k, hk⟩ := id m_div_n.

[Matt Diamond]

you could also use have instead of obtain