internlm/Lean-Github huggingface dataset:
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ A'.card = B.ncard * n
Tactic:
rw [Finset.card_biUnion h4]
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ ∑ u : ↑B, (Finset.filter {a | f a = u} Finset.univ).card = B.ncard * n
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ ∑ u : ↑B, (Finset.filter {a | f a = u} Finset.univ).card = B.ncard * n
Tactic:
rw [Finset.sum_congr rfl h3']
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ ∑ x : ↑B, n = B.ncard * n
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ ∑ x : ↑B, n = B.ncard * n
Tactic:
simp only [Finset.sum_const, smul_eq_mul]
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ Finset.univ.card * n = B.ncard * n
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ Finset.univ.card * n = B.ncard * n
Tactic:
have : (Finset.univ (α := ↑B)).card = Set.ncard B := by
  rw [Finset.card_univ, Fintype.card_eq_nat_card, Set.Nat.card_coe_set_eq]
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
this : Finset.univ.card = B.ncard
⊢ Finset.univ.card * n = B.ncard * n
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
this : Finset.univ.card = B.ncard
⊢ Finset.univ.card * n = B.ncard * n
Tactic:
exact congrFun (congrArg HMul.hMul this) n
Proof state after:
no goals
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
⊢ Finset.univ.card = B.ncard
Tactic:
rw [Finset.card_univ, Fintype.card_eq_nat_card, Set.Nat.card_coe_set_eq]
Proof state after:
no goals
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
⊢ A' = Finset.univ
Tactic:
ext a
Proof state after:
case a
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
⊢ a ∈ A' ↔ a ∈ Finset.univ
Theorem: Imo2008P5.lemma1
Proof state before:
case a
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
⊢ a ∈ A' ↔ a ∈ Finset.univ
Tactic:
constructor
Proof state after:
case a.mp
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
⊢ a ∈ A' → a ∈ Finset.univ

case a.mpr
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
⊢ a ∈ Finset.univ → a ∈ A'
Theorem: Imo2008P5.lemma1
Proof state before:
case a.mp
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
⊢ a ∈ A' → a ∈ Finset.univ
Tactic:
intro _
Proof state after:
case a.mp
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ A'
⊢ a ∈ Finset.univ
Theorem: Imo2008P5.lemma1
Proof state before:
case a.mp
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ A'
⊢ a ∈ Finset.univ
Tactic:
exact @Finset.mem_univ _ hfa a
Proof state after:
no goals
Theorem: Imo2008P5.lemma1
Proof state before:
case a.mpr
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
⊢ a ∈ Finset.univ → a ∈ A'
Tactic:
intro _
Proof state after:
case a.mpr
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ a ∈ A'
Theorem: Imo2008P5.lemma1
Proof state before:
case a.mpr
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ a ∈ A'
Tactic:
rw [Finset.mem_biUnion]
Proof state after:
case a.mpr
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ ∃ a_1 ∈ Finset.univ, a ∈ Finset.filter {a | f a = a_1} Finset.univ
Theorem: Imo2008P5.lemma1
Proof state before:
case a.mpr
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ ∃ a_1 ∈ Finset.univ, a ∈ Finset.filter {a | f a = a_1} Finset.univ
Tactic:
use f a
Proof state after:
case h
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ f a ∈ Finset.univ ∧ a ∈ Finset.filter {a_1 | f a_1 = f a} Finset.univ
Theorem: Imo2008P5.lemma1
Proof state before:
case h
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ f a ∈ Finset.univ ∧ a ∈ Finset.filter {a_1 | f a_1 = f a} Finset.univ
Tactic:
refine ⟨Finset.mem_univ _, ?_⟩
Proof state after:
case h
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ a ∈ Finset.filter {a_1 | f a_1 = f a} Finset.univ
Theorem: Imo2008P5.lemma1
Proof state before:
case h
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ a ∈ Finset.filter {a_1 | f a_1 = f a} Finset.univ
Tactic:
simp
Proof state after:
case h
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ {a_1 | f a_1 = f a} a
Theorem: Imo2008P5.lemma1
Proof state before:
case h
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
A' : Finset { x // A x } := Finset.univ.biUnion fun b => Finset.filter {a | f a = b} Finset.univ
h4 :
  ∀ b1 ∈ Finset.univ,
    ∀ b2 ∈ Finset.univ,
      b1 ≠ b2 → Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
h5 : A'.card = B.ncard * n
a : { x // A x }
a✝ : a ∈ Finset.univ
⊢ {a_1 | f a_1 = f a} a
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo1987P1.card_fixed_points
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card { σx // σx.2 σx.1 = σx.1 } = card α * (card α - 1)!
Tactic:
simp [card_congr (fixedPointsEquiv α), card_perm, Finset.filter_not, Finset.card_sdiff,
  Finset.filter_eq', Finset.card_univ]
Proof state after:
no goals
Theorem: Imo1987P1.main_fintype
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∑ k ∈ range (card α + 1), k * p α k = card α * (card α - 1)!
Tactic:
have A : ∀ (k) (σ : fiber α k), card (fixedPoints (↑σ : Perm α)) = k := fun k σ => σ.2
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
A : ∀ (k : ℕ) (σ : ↑(fiber α k)), card ↑(fixedPoints ⇑↑σ) = k
⊢ ∑ k ∈ range (card α + 1), k * p α k = card α * (card α - 1)!
Theorem: Imo1987P1.main_fintype
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
A : ∀ (k : ℕ) (σ : ↑(fiber α k)), card ↑(fixedPoints ⇑↑σ) = k
⊢ ∑ k ∈ range (card α + 1), k * p α k = card α * (card α - 1)!
Tactic:
simpa [A, ← Fin.sum_univ_eq_sum_range, -card_ofFinset, Finset.card_univ, card_fixed_points,
  mul_comm] using card_congr (fixedPointsEquiv' α)
Proof state after:
no goals
Theorem: Imo1987P1.main₀
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ ∑ k ∈ range (n + 1), k * p (Fin n) k = n * (n - 1)!
Tactic:
simpa using main_fintype (Fin n)
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
⊢ m ≤ n
Tactic:
by_contra h2
Proof state after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
⊢ False
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
⊢ False
Tactic:
have h3 : 1 = (n * (n - m) - m ^ 2) ^ 2 := by linear_combination - h1.eq_one
Proof state after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
⊢ False
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
⊢ False
Tactic:
have h4 : n * (n - m) - m ^ 2 < -1 := by nlinarith [h1.n_range.left]
Proof state after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
⊢ False
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
⊢ False
Tactic:
have h5 : 1 < (n * (n - m) - m ^ 2) ^ 2 := by nlinarith
Proof state after:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
h5 : 1 < (n * (n - m) - m ^ 2) ^ 2
⊢ False
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
h5 : 1 < (n * (n - m) - m ^ 2) ^ 2
⊢ False
Tactic:
exact h5.ne h3
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
⊢ 1 = (n * (n - m) - m ^ 2) ^ 2
Tactic:
linear_combination - h1.eq_one
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
⊢ n * (n - m) - m ^ 2 < -1
Tactic:
nlinarith [h1.n_range.left]
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.m_le_n
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : ¬m ≤ n
h3 : 1 = (n * (n - m) - m ^ 2) ^ 2
h4 : n * (n - m) - m ^ 2 < -1
⊢ 1 < (n * (n - m) - m ^ 2) ^ 2
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.eq_imp_1
Proof state before:
N : ℕ
n : ℤ
h1 : ProblemPredicate N n n
⊢ n * (n * (n * n)) = 1
Tactic:
linear_combination h1.eq_one
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
⊢ ProblemPredicate N (n - m) m
Tactic:
obtain (rfl : m = n) | (h3 : m < n) := h1.m_le_n.eq_or_lt
Proof state after:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
⊢ ProblemPredicate N (m - m) m

case inr
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ ProblemPredicate N (n - m) m
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
case inr
N : ℕ
m n : ℤ
h1 : ProblemPredicate N m n
h2 : 1 < n
h3 : m < n
⊢ ProblemPredicate N (n - m) m
Tactic:
exact
  { n_range := h1.m_range
    m_range := by
      have h5 : 0 < n - m := sub_pos.mpr h3
      have h6 : n - m < N := by
        calc
          _ < n := sub_lt_self n h1.m_range.left
          _ ≤ N := h1.n_range.right
      exact ⟨h5, h6.le⟩
    eq_one := by linear_combination h1.eq_one }
Proof state after:
no goals
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
⊢ ProblemPredicate N (m - m) m
Tactic:
have h4 : m = 1 := h1.eq_imp_1
Proof state after:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
h4 : m = 1
⊢ ProblemPredicate N (m - m) m
Theorem: Imo1981P3.ProblemPredicate.reduction
Proof state before:
case inl
N : ℕ
m : ℤ
h1 : ProblemPredicate N m m
h2 : 1 < m
h4 : m = 1
⊢ ProblemPredicate N (m - m) m
Tactic:
exact absurd h4.symm h2.ne
Proof state after:
no goals