Theorem: Weight.dom_of_mem (Weights/Dimension2.lean)

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
have help {a b c d : ℕ} (hyp : a * b = c * d) : d * c = b * a
State after:
case help
d✝ : ℕ
inst✝ : NeZero d✝
a✝ b✝ : ℕ
I : BasicInterval
hab : a✝ ≠ 0 ∨ b✝ ≠ 0
hm : mem a✝ b✝ I
h :
  (∀ (a' b' : ℕ), mem_S_le d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
a b c d : ℕ
hyp : a * b = c * d
⊢ d * c = b * a

d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

State before:
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
rcases eq_or_eq_or_mem_interior_of_mem hm with H | H | H
State after:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₁ = b * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₂ = b * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

State before:
case help
d✝ : ℕ
inst✝ : NeZero d✝
a✝ b✝ : ℕ
I : BasicInterval
hab : a✝ ≠ 0 ∨ b✝ ≠ 0
hm : mem a✝ b✝ I
h :
  (∀ (a' b' : ℕ), mem_S_le d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d✝ ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
a b c d : ℕ
hyp : a * b = c * d
⊢ d * c = b * a
Tactic:
rw [mul_comm b, mul_comm d, hyp]
State after:
no goals

State before:
case inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₁ = b * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inl <| dom_of_proportional d hab I.coprime₁ <| help H
State after:
no goals

State before:
case inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : a * I.b₂ = b * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inr <| dom_of_proportional d hab I.coprime₂ <| help H
State after:
no goals

State before:
case inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
h :
  (∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂) ∨
    ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
rcases h with h | h
State after:
case inr.inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

case inr.inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b

State before:
case inr.inr.inl
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inl <| dom_of_mem_interior_left d H h
State after:
no goals

State before:
case inr.inr.inr
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hab : a ≠ 0 ∨ b ≠ 0
hm : mem a b I
help : ∀ {a b c d : ℕ}, a * b = c * d → d * c = b * a
H : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_ge d ↑a' ↑b' → mem a' b' I → a' * I.b₁ = b' * I.a₁
⊢ of_fraction d I.a₁ I.b₁ ≤ of_fraction d a b ∨ of_fraction d I.a₂ I.b₂ ≤ of_fraction d a b
Tactic:
exact Or.inr <| dom_of_mem_interior_right d H h
State after:
no goals