internlm/Lean-Github huggingface dataset:
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ (!List.length l % 2 == 1) = true ↔ (Nat.succ (List.length l) % 2 == 1) = true
Tactic:
conv =>
  lhs; rewrite [Nat.not_beq_eq_true_eq]
Proof state after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (Nat.succ (List.length l) % 2 == 1) = true
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (Nat.succ (List.length l) % 2 == 1) = true
Tactic:
conv =>
  rhs; rewrite [beq_iff_eq, Nat.succ_eq_add_one, Nat.add_mod]
  change (l.length % 2 + 1) % 2 = 1
Proof state after:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
cases l.length.mod_two_eq_zero_or_one
Proof state after:
case cons.inl
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 0
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1

case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons.inl
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 0
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1

case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
all_goals (rename_i h; simp only [h])
Proof state after:
no goals
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
(rename_i h; simp only [h])
Proof state after:
no goals
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h : ¬i = j ∧ ¬i ∈ l
h✝ : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
rename_i h
Proof state after:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h✝ : ¬i = j ∧ ¬i ∈ l
h : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Theorem: Permutation.sign_cyclic_cons
Proof state before:
case cons.inr
m n✝ n : Nat
i j : Fin n
l : List (Fin n)
IH : ¬i ∈ l → sign (List.foldr (fun j x => swap x i j) 1 l) = (List.length l % 2 == 1)
h✝ : ¬i = j ∧ ¬i ∈ l
h : List.length l % 2 = 1
⊢ ¬List.length l % 2 = 1 ↔ (List.length l % 2 + 1) % 2 = 1
Tactic:
simp only [h]
Proof state after:
no goals
Theorem: BishopFin.card_subsingleton
Proof state before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ card α ≤ 1
Tactic:
dsimp [card]
Proof state after:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ List.length (elems α) ≤ 1
Theorem: BishopFin.card_subsingleton
Proof state before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
⊢ List.length (elems α) ≤ 1
Tactic:
cases hl : elems α <;> dsimp
Proof state after:
case nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
hl : elems α = []
⊢ 0 ≤ 1

case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1
Theorem: BishopFin.card_subsingleton
Proof state before:
case nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
hl : elems α = []
⊢ 0 ≤ 1

case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1
Tactic:
. decide
Proof state after:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
head✝ : α
tail✝ : List α
hl : elems α = head✝ :: tail✝
⊢ Nat.succ (List.length tail✝) ≤ 1
Tactic:
rename_i a l
Proof state after:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: l
⊢ Nat.succ (List.length l) ≤ 1
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: l
⊢ Nat.succ (List.length l) ≤ 1
Tactic:
cases l <;> dsimp
Proof state after:
case cons.nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
hl : elems α = [a]
⊢ Nat.succ 0 ≤ 1

case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons.nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
hl : elems α = [a]
⊢ Nat.succ 0 ≤ 1

case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1
Tactic:
. decide
Proof state after:
case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons.cons
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ Nat.succ (Nat.succ (List.length tail✝)) ≤ 1
Tactic:
exfalso
Proof state after:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ False
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a head✝ : α
tail✝ : List α
hl : elems α = a :: head✝ :: tail✝
⊢ False
Tactic:
rename_i b l
Proof state after:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a b : α
l : List α
hl : elems α = a :: b :: l
⊢ False
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons.cons.h
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a b : α
l : List α
hl : elems α = a :: b :: l
⊢ False
Tactic:
cases Subsingleton.allEq a b
Proof state after:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
⊢ False
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
⊢ False
Tactic:
have : List.Nodup (a :: a :: l) := hl ▸ nodup_elems
Proof state after:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
this : List.Nodup (a :: a :: l)
⊢ False
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons.cons.h.refl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
l : List α
hl : elems α = a :: a :: l
this : List.Nodup (a :: a :: l)
⊢ False
Tactic:
exact this.head (List.mem_cons_self a l)
Proof state after:
no goals
Theorem: BishopFin.card_subsingleton
Proof state before:
case nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
hl : elems α = []
⊢ 0 ≤ 1
Tactic:
decide
Proof state after:
no goals
Theorem: BishopFin.card_subsingleton
Proof state before:
case cons.nil
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Subsingleton α
a : α
hl : elems α = [a]
⊢ Nat.succ 0 ≤ 1
Tactic:
decide
Proof state after:
no goals
Theorem: BishopFin.card_nonempty
Proof state before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
⊢ card α ≥ 1
Tactic:
cases Nat.eq_zero_or_pos (card α) with
| inl h0 =>
  dsimp [card] at h0
  rcases ‹Nonempty α› with ⟨a⟩
  have := List.eq_nil_of_length_eq_zero h0
  have : a ∈ [] := this ▸ mem_elems a
  cases this
| inr h => exact h
Proof state after:
no goals
Theorem: BishopFin.card_nonempty
Proof state before:
case inl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : card α = 0
⊢ card α ≥ 1
Tactic:
dsimp [card] at h0
Proof state after:
case inl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
⊢ card α ≥ 1
Theorem: BishopFin.card_nonempty
Proof state before:
case inl
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
⊢ card α ≥ 1
Tactic:
rcases ‹Nonempty α› with ⟨a⟩
Proof state after:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
⊢ card α ≥ 1
Theorem: BishopFin.card_nonempty
Proof state before:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
⊢ card α ≥ 1
Tactic:
have := List.eq_nil_of_length_eq_zero h0
Proof state after:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this : elems α = []
⊢ card α ≥ 1
Theorem: BishopFin.card_nonempty
Proof state before:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this : elems α = []
⊢ card α ≥ 1
Tactic:
have : a ∈ [] := this ▸ mem_elems a
Proof state after:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this✝ : elems α = []
this : a ∈ []
⊢ card α ≥ 1
Theorem: BishopFin.card_nonempty
Proof state before:
case inl.intro
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h0 : List.length (elems α) = 0
a : α
this✝ : elems α = []
this : a ∈ []
⊢ card α ≥ 1
Tactic:
cases this
Proof state after:
no goals
Theorem: BishopFin.card_nonempty
Proof state before:
case inr
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ : BishopFin β
inst✝ : Nonempty α
h : card α > 0
⊢ card α ≥ 1
Tactic:
exact h
Proof state after:
no goals
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β
Tactic:
dsimp only [card]
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.length (elems α) ≤ List.length (elems β)
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.length (elems α) ≤ List.length (elems β)
Tactic:
conv =>
  lhs; equals ((elems α).map f).length => rw [List.length_map]
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.length (List.map f (elems α)) ≤ List.length (elems β)
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.length (List.map f (elems α)) ≤ List.length (elems β)
Tactic:
refine List.Nodup.length_le_of_subset ?_ ?_
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.Nodup (List.map f (elems α))

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.Nodup (List.map f (elems α))

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Tactic:
. exact nodup_elems.map f f_inj
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Tactic:
. exact subset_elems _
Proof state after:
no goals
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.length (elems α) = List.length (List.map f (elems α))
Tactic:
rw [List.length_map]
Proof state after:
no goals
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.Nodup (List.map f (elems α))
Tactic:
exact nodup_elems.map f f_inj
Proof state after:
no goals
Theorem: BishopFin.card_le_card_of_inj
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ List.map f (elems α) ⊆ elems β
Tactic:
exact subset_elems _
Proof state after:
no goals
Theorem: BishopFin.card_ge_card_of_surj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ card α ≥ card β
Tactic:
dsimp only [card]
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (elems α) ≥ List.length (elems β)
Theorem: BishopFin.card_ge_card_of_surj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (elems α) ≥ List.length (elems β)
Tactic:
conv =>
  lhs; equals ((elems α).map f).length => rw [List.length_map]
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (List.map f (elems α)) ≥ List.length (elems β)
Theorem: BishopFin.card_ge_card_of_surj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (List.map f (elems α)) ≥ List.length (elems β)
Tactic:
refine nodup_elems.length_le_of_subset ?_
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ elems β ⊆ List.map f (elems α)
Theorem: BishopFin.card_ge_card_of_surj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ elems β ⊆ List.map f (elems α)
Tactic:
intro b _
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ b ∈ List.map f (elems α)
Theorem: BishopFin.card_ge_card_of_surj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ b ∈ List.map f (elems α)
Tactic:
simp only [List.mem_map, mem_elems, true_and]
Proof state after:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ ∃ a, f a = b
Theorem: BishopFin.card_ge_card_of_surj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ ∃ a, f a = b
Tactic:
exact f_surj b
Proof state after:
no goals
Theorem: BishopFin.card_ge_card_of_surj
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
⊢ List.length (elems α) = List.length (List.map f (elems α))
Tactic:
rw [List.length_map]
Proof state after:
no goals
Theorem: BishopFin.card_eq_card_of_bij
Proof state before:
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α = card β
Tactic:
refine Nat.le_antisymm ?_ ?_
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Theorem: BishopFin.card_eq_card_of_bij
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Tactic:
. exact card_le_card_of_inj f f_inj
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Theorem: BishopFin.card_eq_card_of_bij
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Tactic:
. exact card_ge_card_of_surj f f_surj
Proof state after:
no goals
Theorem: BishopFin.card_eq_card_of_bij
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β
Tactic:
exact card_le_card_of_inj f f_inj
Proof state after:
no goals
Theorem: BishopFin.card_eq_card_of_bij
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α
Tactic:
exact card_ge_card_of_surj f f_surj
Proof state after:
no goals
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α = card β
Tactic:
refine Nat.le_antisymm ?_ ?_
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Tactic:
. show card α ≤ card β
  refine card_le_card_of_inj f ?_
  intros a₁ a₂ hfa
  rw [← hgf a₁, ← hgf a₂, hfa]
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Tactic:
. show card β ≤ card α
  refine card_le_card_of_inj g ?_
  intro b₁ b₂ hgb
  rw [← hfg b₁, ← hfg b₂, hgb]
Proof state after:
no goals
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α ≤ card β
Tactic:
refine card_le_card_of_inj f ?_
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
Tactic:
intros a₁ a₂ hfa
Proof state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
a₁ a₂ : α
hfa : f a₁ = f a₂
⊢ a₁ = a₂
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
a₁ a₂ : α
hfa : f a₁ = f a₂
⊢ a₁ = a₂
Tactic:
rw [← hgf a₁, ← hgf a₂, hfa]
Proof state after:
no goals
Theorem: BishopFin.card_eq_card_of_inv
Proof state before:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α
Tactic:
refine card_le_card_of_inj g ?_
Proof state after:
case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ ∀ (a₁ a₂ : β), g a₁ = g a₂ → a₁ = a₂