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 : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
⊢ B.ncard * n = A.ncard
Tactic:
haveI hfb : Fintype ↑B := Set.Finite.fintype hB
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
⊢ B.ncard * n = A.ncard
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
⊢ B.ncard * n = A.ncard
Tactic:
have hbf : ∀ b,  Fintype { a // f a = b } := by
  intro b
  have : Fintype { x // A x } := hfa
  exact setFintype fun x ↦ f x = b
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
⊢ B.ncard * n = A.ncard
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
⊢ B.ncard * n = A.ncard
Tactic:
have h2 : ∀ b, Set.ncard { a | f a = b } = Fintype.card { a // f a = b} := by
  intro b
  rw [Set.setOf_set, Fintype.card_eq_nat_card, ←Set.Nat.card_coe_set_eq]
  rfl
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
⊢ B.ncard * n = A.ncard
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
⊢ B.ncard * n = A.ncard
Tactic:
have h3' : ∀ b ∈ Finset.univ (α := ↑B), (Finset.filter {a | f a = b } (Finset.univ (α := ↑A))).card = n := by
  intro b _
  rw [← @Fintype.card_subtype]
  rw [← h1
      b, h2,
      Set.setOf_set, Fintype.card_eq_nat_card,
      Mathlib.Tactic.Zify.natCast_eq, Fintype.card_eq_nat_card]
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
⊢ B.ncard * n = A.ncard
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
h3' : ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
⊢ B.ncard * n = A.ncard
Tactic:
clear h1 h2
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
⊢ B.ncard * n = A.ncard
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
⊢ B.ncard * n = A.ncard
Tactic:
let A' := Finset.biUnion
           (Finset.univ (α := ↑B))
           (fun b ↦ Finset.filter { a | f a = b } (Finset.univ (α := ↑A)))
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
⊢ B.ncard * n = A.ncard
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
⊢ B.ncard * n = A.ncard
Tactic:
have h4 :
  ∀ b1 ∈ (Finset.univ (α := ↑B)),
    ∀ b2 ∈ (Finset.univ (α := ↑B)),
      b1 ≠ b2 →
        Disjoint
          (Finset.filter { a | f a = b1 } (Finset.univ (α := ↑A)))
          (Finset.filter { a | f a = b2 } (Finset.univ (α := ↑A))) := by
  intro b1 _ b2 _ hb12
  rw [Finset.disjoint_filter]
  intro x _ hx2 hx3
  rw [Set.setOf_app_iff] at hx2 hx3
  rw [hx2] at hx3
  exact hb12 hx3
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)
⊢ B.ncard * n = A.ncard
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)
⊢ B.ncard * n = A.ncard
Tactic:
have h5 : A'.card = Set.ncard B * n := by
  rw [Finset.card_biUnion h4]
  rw [Finset.sum_congr rfl h3']
  simp only [Finset.sum_const, smul_eq_mul]
  have : (Finset.univ (α := ↑B)).card = Set.ncard B := by
    rw [Finset.card_univ, Fintype.card_eq_nat_card, Set.Nat.card_coe_set_eq]
  exact congrFun (congrArg HMul.hMul this) n
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)
h5 : A'.card = B.ncard * n
⊢ B.ncard * n = A.ncard
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
⊢ B.ncard * n = A.ncard
Tactic:
rw [←h5]
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)
h5 : A'.card = B.ncard * n
⊢ A'.card = A.ncard
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
h6 : A' = Finset.univ
⊢ A'.card = A.ncard
Tactic:
rw[h6]
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)
h5 : A'.card = B.ncard * n
h6 : A' = Finset.univ
⊢ Finset.univ.card = A.ncard
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
h6 : A' = Finset.univ
⊢ Finset.univ.card = A.ncard
Tactic:
rw [@Finset.card_univ, ←Set.Nat.card_coe_set_eq, Fintype.card_eq_nat_card]
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)
h5 : A'.card = B.ncard * n
h6 : A' = Finset.univ
⊢ Nat.card { x // A x } = Nat.card ↑A
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
h6 : A' = Finset.univ
⊢ Nat.card { x // A x } = Nat.card ↑A
Tactic:
rfl
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 : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
⊢ (b : { x // B x }) → Fintype { a // f a = b }
Tactic:
intro b
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
b : { x // B x }
⊢ Fintype { a // f a = b }
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
b : { x // B x }
⊢ Fintype { a // f a = b }
Tactic:
have : Fintype { x // A x } := hfa
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
b : { x // B x }
this : Fintype { x // A x }
⊢ Fintype { a // f a = b }
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
b : { x // B x }
this : Fintype { x // A x }
⊢ Fintype { a // f a = b }
Tactic:
exact setFintype fun x ↦ f x = b
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 : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
⊢ ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
Tactic:
intro b
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
b : { x // B x }
⊢ {a | f a = b}.ncard = Fintype.card { a // f a = b }
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
b : { x // B x }
⊢ {a | f a = b}.ncard = Fintype.card { a // f a = b }
Tactic:
rw [Set.setOf_set, 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 : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
b : { x // B x }
⊢ (Nat.card ↑fun a => f a = b) = Nat.card { a // f a = b }
Theorem: Imo2008P5.lemma1
Proof state before:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
b : { x // B x }
⊢ (Nat.card ↑fun a => f a = b) = Nat.card { a // f a = b }
Tactic:
rfl
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 : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
⊢ ∀ b ∈ Finset.univ, (Finset.filter {a | f a = b} Finset.univ).card = n
Tactic:
intro b _
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
b : ↑B
a✝ : b ∈ Finset.univ
⊢ (Finset.filter {a | f a = b} Finset.univ).card = 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 : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
b : ↑B
a✝ : b ∈ Finset.univ
⊢ (Finset.filter {a | f a = b} Finset.univ).card = n
Tactic:
rw [← @Fintype.card_subtype]
Proof state after:
α : Type
A B : Set α
hA : A.Finite
hB : B.Finite
f : { x // A x } → { x // B x }
n : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
b : ↑B
a✝ : b ∈ Finset.univ
⊢ Fintype.card { x // {a | f a = b} x } = 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 : ℕ
h1 : ∀ (b : { x // B x }), {a | f a = b}.ncard = n
hfa : Fintype ↑A
hfb : Fintype ↑B
hbf : (b : { x // B x }) → Fintype { a // f a = b }
h2 : ∀ (b : { x // B x }), {a | f a = b}.ncard = Fintype.card { a // f a = b }
b : ↑B
a✝ : b ∈ Finset.univ
⊢ Fintype.card { x // {a | f a = b} x } = n
Tactic:
rw [← h1
    b, h2,
    Set.setOf_set, Fintype.card_eq_nat_card,
    Mathlib.Tactic.Zify.natCast_eq, Fintype.card_eq_nat_card]
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
⊢ ∀ 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)
Tactic:
intro b1 _ b2 _ hb12
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
b1 : ↑B
a✝¹ : b1 ∈ Finset.univ
b2 : ↑B
a✝ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
⊢ Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
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
b1 : ↑B
a✝¹ : b1 ∈ Finset.univ
b2 : ↑B
a✝ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
⊢ Disjoint (Finset.filter {a | f a = b1} Finset.univ) (Finset.filter {a | f a = b2} Finset.univ)
Tactic:
rw [Finset.disjoint_filter]
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
b1 : ↑B
a✝¹ : b1 ∈ Finset.univ
b2 : ↑B
a✝ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
⊢ ∀ x ∈ Finset.univ, {a | f a = b1} x → ¬{a | f a = b2} x
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
b1 : ↑B
a✝¹ : b1 ∈ Finset.univ
b2 : ↑B
a✝ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
⊢ ∀ x ∈ Finset.univ, {a | f a = b1} x → ¬{a | f a = b2} x
Tactic:
intro x _ hx2 hx3
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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : {a | f a = b1} x
hx3 : {a | f a = b2} x
⊢ False
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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : {a | f a = b1} x
hx3 : {a | f a = b2} x
⊢ False
Tactic:
rw [Set.setOf_app_iff] at hx2 hx3
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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : f x = b1
hx3 : f x = b2
⊢ False
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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : f x = b1
hx3 : f x = b2
⊢ False
Tactic:
rw [hx2] at hx3
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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : f x = b1
hx3 : b1 = b2
⊢ False
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
b1 : ↑B
a✝² : b1 ∈ Finset.univ
b2 : ↑B
a✝¹ : b2 ∈ Finset.univ
hb12 : b1 ≠ b2
x : { x // A x }
a✝ : x ∈ Finset.univ
hx2 : f x = b1
hx3 : b1 = b2
⊢ False
Tactic:
exact hb12 hx3
Proof state after:
no goals