Theorem: Imo2022P2.lemma0 (Compfiles/Imo2022P2.lean)

State before:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
⊢ ∀ (x : α), Classical.choose ⋯ = x
Tactic:
intro x
State after:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x : α
⊢ Classical.choose ⋯ = x

State before:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x : α
⊢ Classical.choose ⋯ = x
Tactic:
obtain ⟨y, h1e, h1u⟩ := h1 x
State after:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
⊢ Classical.choose ⋯ = x

State before:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
⊢ Classical.choose ⋯ = x
Tactic:
have h2' : Classical.choose (h1 x).exists = y :=
  h1u _ (Classical.choose_spec (h1 x).exists)
State after:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
⊢ Classical.choose ⋯ = x

State before:
case intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
⊢ Classical.choose ⋯ = x
Tactic:
obtain ⟨w, h1e', h1u'⟩ := h1 y
State after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
⊢ Classical.choose ⋯ = x

State before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
⊢ Classical.choose ⋯ = x
Tactic:
have h4 := Classical.choose_spec (h1 y).exists
State after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ Classical.choose ⋯ = x

State before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ Classical.choose ⋯ = x
Tactic:
have hxw : x = w := by
  apply h1u'
  rw [h2]
  exact h1e
State after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = x

State before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = x
Tactic:
rw [hxw]
State after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = w

State before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = w
Tactic:
exact h1u' _ h4
State after:
no goals

State before:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ x = w
Tactic:
apply h1u'
State after:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p y x

State before:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p y x
Tactic:
rw [h2]
State after:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p x y

State before:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p x y
Tactic:
exact h1e
State after:
no goals