Theorem: Imo2008P5.lemma1 (Compfiles/Imo2008P5.lean)

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
⊢ B.ncard * n = A.ncard
Tactic:
haveI hfa : Fintype ↑A := Set.Finite.fintype hA
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
⊢ B.ncard * n = A.ncard

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
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

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
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

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
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

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]
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

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
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

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)))
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

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
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

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
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

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]
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

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]
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

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]
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

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
State after:
no goals

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
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 }

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
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 }

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
State after:
no goals

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
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 }

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]
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 }

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
State after:
no goals

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 _
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

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]
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

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]
State after:
no goals

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
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)

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]
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

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
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

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
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

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
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

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
State after:
no goals

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]
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

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']
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

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]
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

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]
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

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
State after:
no goals

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]
State after:
no goals

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
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

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
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'

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 _
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

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
State after:
no goals

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 _
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'

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]
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

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
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

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 _, ?_⟩
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

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
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

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
State after:
no goals