Proving intersection of two proofs

Stream: lean4

[Kevin Ikeland]

example : 9 ∈ odd_perfects :=
nine_is_odd : 9 ∈ odds := ⟨4, rfl⟩
nine_is_perfect_square : 9 ∈ perfect_squares :=  ⟨3, rfl⟩

How do I prove 9 is odd and a perfect square using a proof within a proof?

[Mario Carneiro]

Could you give a complete #mwe for this example?

[Mario Carneiro]

what you have written is not valid syntax

[Kevin Ikeland]

def odds : Set Nat := { n : Nat | ∃ m, n = 2 * m + 1 }
def perfect_squares : Set Nat := { n : Nat | ∃ m, n = m^2 }
def odd_perfects : Set Nat := odds ∩ perfect_squares
example : 9 ∈ odd_perfects :=
nine_is_odd : 9 ∈ odds := ⟨4, rfl⟩
nine_is_perfect_square : 9 ∈ perfect_squares :=  ⟨3, rfl⟩ ```  This is the complete code, I am not sure how to write it in valid syntax.

[Mario Carneiro]

import Mathlib.Data.Set.Basic

def odds : Set Nat := { n : Nat | ∃ m, n = 2 * m + 1 }
def perfect_squares : Set Nat := { n : Nat | ∃ m, n = m^2 }
def odd_perfects : Set Nat := odds ∩ perfect_squares
example : 9 ∈ odd_perfects :=
  have nine_is_odd : 9 ∈ odds := ⟨4, rfl⟩
  have nine_is_perfect_square : 9 ∈ perfect_squares :=  ⟨3, rfl⟩
  show 9 ∈ odd_perfects from
  show 9 ∈ odds ∧ 9 ∈ perfect_squares from
  ⟨nine_is_odd, nine_is_perfect_square⟩

[Mario Carneiro]

don't forget the imports

[Mario Carneiro]

the show lines are unnecessary but show what the goal is. In particular lean knows that 9 ∈ odd_perfects means the same thing as 9 ∈ odds ∧ 9 ∈ perfect_squares by the definition of intersection

[Kevin Ikeland]

Okay got it. Thank you!