internlm/Lean-Github huggingface dataset:
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp4' : ∃ a ∈ α, { toFun := fun x => ↑x, inj' := ⋯ } a = p4'
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p3, p3_ne⟩ = p3'
⊢ discusses p3' p4' = ↑t3
Tactic:
obtain ⟨⟨p4, p4_ne⟩, p4_mem_α, p4_eq⟩ := hp4'
Proof state after:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p3, p3_ne⟩ = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p4, p4_ne⟩ = p4'
⊢ discusses p3' p4' = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p3, p3_ne⟩ = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : { toFun := fun x => ↑x, inj' := ⋯ } ⟨p4, p4_ne⟩ = p4'
⊢ discusses p3' p4' = ↑t3
Tactic:
dsimp at p3_eq p4_eq
Proof state after:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3' p4' = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3' p4' = ↑t3
Tactic:
rw [←p3_eq, ←p4_eq]
Proof state after:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3 p4 = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ discusses p3 p4 = ↑t3
Tactic:
have hne : p3 ≠ p4 := by rwa [p3_eq, p4_eq]
Proof state after:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
⊢ discusses p3 p4 = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
⊢ discusses p3 p4 = ↑t3
Tactic:
have h8 := h6 ⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ⟨⟨p4, p4_ne⟩, p4_mem_α⟩
              (by simp[hne, Person', Topic'])
Proof state after:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
⊢ discusses p3 p4 = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
⊢ discusses p3 p4 = ↑t3
Tactic:
let t3': Topic' := ⟨discusses p3 p4, h8⟩
Proof state after:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
⊢ discusses p3 p4 = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
⊢ discusses p3 p4 = ↑t3
Tactic:
have h9 := ht3 t3'
Proof state after:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
h9 : t3' = t3
⊢ discusses p3 p4 = ↑t3
Theorem: Imo1964P4.lemma1
Proof state before:
case h.right.intro.mk.intro.intro.mk.intro
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
h8 : discusses ↑↑⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ↑↑⟨⟨p4, p4_ne⟩, p4_mem_α⟩ ≠ t2
t3' : Topic' := ⟨discusses p3 p4, h8⟩
h9 : t3' = t3
⊢ discusses p3 p4 = ↑t3
Tactic:
rw [←h9]
Proof state after:
no goals
Theorem: Imo1964P4.lemma1
Proof state before:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
⊢ p3 ≠ p4
Tactic:
rwa [p3_eq, p4_eq]
Proof state after:
no goals
Theorem: Imo1964P4.lemma1
Proof state before:
Person Topic : Type
inst✝³ : Fintype Person
inst✝² : DecidableEq Person
inst✝¹ : Fintype Topic
inst✝ : DecidableEq Topic
card_person : 5 < Fintype.card Person
card_topic : Fintype.card Topic = 2
discusses : Person → Person → Topic
discussion_sym : ∀ (p1 p2 : Person), discusses p1 p2 = discusses p2 p1
p2 : Person
Person' : Type := { p3 // p3 ≠ p2 }
hfcα : 4 < Fintype.card Person'
h1 : Fintype.card Topic * 2 < Fintype.card Person'
t2 : Topic
ht2 : 2 < (Finset.filter (fun x => (fun p3 => discusses p2 ↑p3) x = t2) Finset.univ).card
α : Finset Person' := Finset.filter (fun x => discusses p2 ↑x = t2) Finset.univ
Topic' : Type := { t3 // t3 ≠ t2 }
h4 : Fintype.card Topic' = 1
t3 : Topic'
ht3 : ∀ (y : Topic'), y = t3
h6 : ∀ (p3 p4 : { x // x ∈ α }), p3 ≠ p4 → discusses ↑↑p3 ↑↑p4 ≠ t2
α' : Finset Person := Finset.map { toFun := fun x => ↑x, inj' := ⋯ } α
p3' p4' : Person
hp3p4' : p3' ≠ p4'
p3 : Person
p3_ne : p3 ≠ p2
p3_mem_α : ⟨p3, p3_ne⟩ ∈ α
p3_eq : p3 = p3'
p4 : Person
p4_ne : p4 ≠ p2
p4_mem_α : ⟨p4, p4_ne⟩ ∈ α
p4_eq : p4 = p4'
hne : p3 ≠ p4
⊢ ⟨⟨p3, p3_ne⟩, p3_mem_α⟩ ≠ ⟨⟨p4, p4_ne⟩, p4_mem_α⟩
Tactic:
simp[hne, Person', Topic']
Proof state after:
no goals
Theorem: Imo1965P2.lemma0
Proof state before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
⊢ propEqs (x ∘ p) fun i j => a (p i) (p j)
Tactic:
intro i
Proof state after:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, (fun i j => a (p i) (p j)) i j * (x ∘ p) j = 0
Theorem: Imo1965P2.lemma0
Proof state before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, (fun i j => a (p i) (p j)) i j * (x ∘ p) j = 0
Tactic:
dsimp
Proof state after:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0
Theorem: Imo1965P2.lemma0
Proof state before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0
Tactic:
have hi := he (p i)
Proof state after:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
hi : ∑ j : Fin 3, a (p i) j * x j = 0
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0
Theorem: Imo1965P2.lemma0
Proof state before:
x : Fin 3 → ℝ
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
he : propEqs x a
i : Fin 3
hi : ∑ j : Fin 3, a (p i) j * x j = 0
⊢ ∑ j : Fin 3, a (p i) (p j) * x (p j) = 0
Tactic:
rwa [Function.Bijective.sum_comp hp (fun j ↦ a (p i) j * x j)]
Proof state after:
no goals
Theorem: Imo1965P2.lemma1
Proof state before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
⊢ propsAB fun i j => a (p i) (p j)
Tactic:
intro i j
Proof state after:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0
Theorem: Imo1965P2.lemma1
Proof state before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0
Tactic:
have h0 := hab (p i) (p j)
Proof state after:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0
Theorem: Imo1965P2.lemma1
Proof state before:
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
⊢ if i = j then 0 < (fun i j => a (p i) (p j)) i j else (fun i j => a (p i) (p j)) i j < 0
Tactic:
split_ifs with h1
Proof state after:
case pos
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : i = j
⊢ 0 < (fun i j => a (p i) (p j)) i j

case neg
a : Fin 3 → Fin 3 → ℝ
p : Fin 3 → Fin 3
hp : Function.Bijective p
hab : propsAB a
i j : Fin 3
h0 : if p i = p j then 0 < a (p i) (p j) else a (p i) (p j) < 0
h1 : ¬i = j
⊢ (fun i j => a (p i) (p j)) i j < 0