internlm/Lean-Github huggingface dataset:
Theorem: Finset.getUnique_eq
Proof state before:
case intro.hmotive
α : Type u_1
v x : α
L : List ?intro.α
hL : ↑L = ?intro.s.val
heq : elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb
Tactic:
rw [heq]
Proof state after:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
heq :
  elim {x}
      (fun L _hL =>
        match L, _hL with
        | [], _hL => ⋯.elim
        | x_1 :: tail, _hL => x_1)
      ⋯ =
    match L, hL with
    | [], _hL => ⋯.elim
    | x_1 :: tail, _hL => x_1
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Theorem: Finset.getUnique_eq
Proof state before:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
heq :
  elim {x}
      (fun L _hL =>
        match L, _hL with
        | [], _hL => ⋯.elim
        | x_1 :: tail, _hL => x_1)
      ⋯ =
    match L, hL with
    | [], _hL => ⋯.elim
    | x_1 :: tail, _hL => x_1
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
clear heq
Proof state after:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Theorem: Finset.getUnique_eq
Proof state before:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL : ↑L = {x}.val
⊢ (match L, hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
simp at hL
Proof state after:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL✝ : ↑L = {x}.val
hL : L = [x]
⊢ (match L, hL✝ with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Theorem: Finset.getUnique_eq
Proof state before:
case intro.hmotive
α : Type u_1
v x : α
L : List α
hL✝ : ↑L = {x}.val
hL : L = [x]
⊢ (match L, hL✝ with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
cases hL
Proof state after:
case intro.hmotive.refl
α : Type u_1
v x : α
hL : ↑[x] = {x}.val
⊢ (match [x], hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Theorem: Finset.getUnique_eq
Proof state before:
case intro.hmotive.refl
α : Type u_1
v x : α
hL : ↑[x] = {x}.val
⊢ (match [x], hL with
      | [], _hL => ⋯.elim
      | x_1 :: tail, _hL => x_1) =
      v ↔
    x = v
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.getUnique_mem
Proof state before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
⊢ getUnique xs h ∈ y ↔ xs ⊆ y
Tactic:
generalize hv : getUnique xs h = v
Proof state after:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : getUnique xs h = v
⊢ v ∈ y ↔ xs ⊆ y
Theorem: Finset.getUnique_mem
Proof state before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : getUnique xs h = v
⊢ v ∈ y ↔ xs ⊆ y
Tactic:
simp at hv
Proof state after:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : xs = {v}
⊢ v ∈ y ↔ xs ⊆ y
Theorem: Finset.getUnique_mem
Proof state before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
y : Finset α
v : α
hv : xs = {v}
⊢ v ∈ y ↔ xs ⊆ y
Tactic:
simp [hv]
Proof state after:
no goals
Theorem: List.Perm.find?_unique
Proof state before:
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
h : a ~ b
⊢ find? f a = find? f b
Tactic:
induction h with
| nil => simp
| cons => simp [find?]; split <;> simp [*]
| swap =>
  simp [find?]; split <;> split <;> simp
  apply hunique; repeat assumption
| trans =>
  simp_all
Proof state after:
no goals
Theorem: List.Perm.find?_unique
Proof state before:
case nil
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
⊢ find? f [] = find? f []
Tactic:
simp
Proof state after:
no goals
Theorem: List.Perm.find?_unique
Proof state before:
case cons
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : find? f l₁✝ = find? f l₂✝
⊢ find? f (x✝ :: l₁✝) = find? f (x✝ :: l₂✝)
Tactic:
simp [find?]
Proof state after:
case cons
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : find? f l₁✝ = find? f l₂✝
⊢ (match f x✝ with
    | true => some x✝
    | false => find? f l₁✝) =
    match f x✝ with
    | true => some x✝
    | false => find? f l₂✝
Theorem: List.Perm.find?_unique
Proof state before:
case cons
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
a_ih✝ : find? f l₁✝ = find? f l₂✝
⊢ (match f x✝ with
    | true => some x✝
    | false => find? f l₁✝) =
    match f x✝ with
    | true => some x✝
    | false => find? f l₂✝
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: List.Perm.find?_unique
Proof state before:
case swap
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ y✝ : α
l✝ : List α
⊢ find? f (y✝ :: x✝ :: l✝) = find? f (x✝ :: y✝ :: l✝)
Tactic:
simp [find?]
Proof state after:
case swap
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ y✝ : α
l✝ : List α
⊢ (match f y✝ with
    | true => some y✝
    | false =>
      match f x✝ with
      | true => some x✝
      | false => find? f l✝) =
    match f x✝ with
    | true => some x✝
    | false =>
      match f y✝ with
      | true => some y✝
      | false => find? f l✝
Theorem: List.Perm.find?_unique
Proof state before:
case swap
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝ y✝ : α
l✝ : List α
⊢ (match f y✝ with
    | true => some y✝
    | false =>
      match f x✝ with
      | true => some x✝
      | false => find? f l✝) =
    match f x✝ with
    | true => some x✝
    | false =>
      match f y✝ with
      | true => some y✝
      | false => find? f l✝
Tactic:
split <;> split <;> simp
Proof state after:
case swap.h_1.h_1
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ y✝ = x✝²
Theorem: List.Perm.find?_unique
Proof state before:
case swap.h_1.h_1
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ y✝ = x✝²
Tactic:
apply hunique
Proof state after:
case swap.h_1.h_1.a
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ f y✝ = true

case swap.h_1.h_1.a
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ f x✝² = true
Theorem: List.Perm.find?_unique
Proof state before:
case swap.h_1.h_1.a
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ f y✝ = true

case swap.h_1.h_1.a
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ f x✝² = true
Tactic:
repeat assumption
Proof state after:
no goals
Theorem: List.Perm.find?_unique
Proof state before:
case swap.h_1.h_1.a
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x✝² y✝ : α
l✝ : List α
x✝¹ : Bool
heq✝¹ : f y✝ = true
x✝ : Bool
heq✝ : f x✝² = true
⊢ f x✝² = true
Tactic:
assumption
Proof state after:
no goals
Theorem: List.Perm.find?_unique
Proof state before:
case trans
α : Type u_1
a b : List α
f : α → Bool
hunique : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
a_ih✝¹ : find? f l₁✝ = find? f l₂✝
a_ih✝ : find? f l₂✝ = find? f l₃✝
⊢ find? f l₁✝ = find? f l₃✝
Tactic:
simp_all
Proof state after:
no goals
Theorem: Multiset.find?_eq_some
Proof state before:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
xs : Multiset α
⊢ find? f xs h = some x ↔ x ∈ xs ∧ f x = true
Tactic:
have ⟨L,hL⟩ := xs.exists_rep
Proof state after:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
xs : Multiset α
L : List α
hL : ⟦L⟧ = xs
⊢ find? f xs h = some x ↔ x ∈ xs ∧ f x = true
Theorem: Multiset.find?_eq_some
Proof state before:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
xs : Multiset α
L : List α
hL : ⟦L⟧ = xs
⊢ find? f xs h = some x ↔ x ∈ xs ∧ f x = true
Tactic:
cases hL
Proof state after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ find? f ⟦L⟧ h = some x ↔ x ∈ ⟦L⟧ ∧ f x = true
Theorem: Multiset.find?_eq_some
Proof state before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ find? f ⟦L⟧ h = some x ↔ x ∈ ⟦L⟧ ∧ f x = true
Tactic:
simp [-quot_mk_to_coe, find?]
Proof state after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ ⟦L⟧ ∧ f x = true
Theorem: Multiset.find?_eq_some
Proof state before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ ⟦L⟧ ∧ f x = true
Tactic:
simp
Proof state after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ L ∧ f x = true
Theorem: Multiset.find?_eq_some
Proof state before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x ↔ x ∈ L ∧ f x = true
Tactic:
constructor
Proof state after:
case refl.mp
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x → x ∈ L ∧ f x = true

case refl.mpr
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ x ∈ L ∧ f x = true → List.find? f L = some x
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mp
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ List.find? f L = some x → x ∈ L ∧ f x = true
Tactic:
intro h
Proof state after:
case refl.mp
α : Type u_1
f : α → Bool
h✝ : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h : List.find? f L = some x
⊢ x ∈ L ∧ f x = true
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mp
α : Type u_1
f : α → Bool
h✝ : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h : List.find? f L = some x
⊢ x ∈ L ∧ f x = true
Tactic:
simp [List.find?_some h, List.find?_mem h]
Proof state after:
no goals
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mpr
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
⊢ x ∈ L ∧ f x = true → List.find? f L = some x
Tactic:
rintro ⟨h1,h2⟩
Proof state after:
case refl.mpr.intro
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h1 : x ∈ L
h2 : f x = true
⊢ List.find? f L = some x
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mpr.intro
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h1 : x ∈ L
h2 : f x = true
⊢ List.find? f L = some x
Tactic:
induction h1 <;> simp [List.find?, *]
Proof state after:
case refl.mpr.intro.tail
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
⊢ (match f b✝ with
    | true => some b✝
    | false => some x) =
    some x
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mpr.intro.tail
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
⊢ (match f b✝ with
    | true => some b✝
    | false => some x) =
    some x
Tactic:
split
Proof state after:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ some b✝ = some x

case refl.mpr.intro.tail.h_2
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = false
⊢ some x = some x
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ some b✝ = some x
Tactic:
simp
Proof state after:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ b✝ = x
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ b✝ = x
Tactic:
apply h <;> assumption
Proof state after:
no goals
Theorem: Multiset.find?_eq_some
Proof state before:
case refl.mpr.intro.tail.h_2
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = false
⊢ some x = some x
Tactic:
rfl
Proof state after:
no goals
Theorem: Multiset.find?_eq_none
Proof state before:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
xs : Multiset α
⊢ find? f xs h = none ↔ ∀ x ∈ xs, f x = false
Tactic:
have ⟨L,hL⟩ := xs.exists_rep
Proof state after:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
xs : Multiset α
L : List α
hL : ⟦L⟧ = xs
⊢ find? f xs h = none ↔ ∀ x ∈ xs, f x = false
Theorem: Multiset.find?_eq_none
Proof state before:
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
xs : Multiset α
L : List α
hL : ⟦L⟧ = xs
⊢ find? f xs h = none ↔ ∀ x ∈ xs, f x = false
Tactic:
cases hL
Proof state after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ find? f ⟦L⟧ h = none ↔ ∀ x ∈ ⟦L⟧, f x = false
Theorem: Multiset.find?_eq_none
Proof state before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ find? f ⟦L⟧ h = none ↔ ∀ x ∈ ⟦L⟧, f x = false
Tactic:
simp only [find?, Quotient.lift_mk, List.find?_eq_none, Bool.not_eq_true]
Proof state after:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ (∀ x ∈ L, f x = false) ↔ ∀ x ∈ ⟦L⟧, f x = false
Theorem: Multiset.find?_eq_none
Proof state before:
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ (∀ x ∈ L, f x = false) ↔ ∀ x ∈ ⟦L⟧, f x = false
Tactic:
simp only [quot_mk_to_coe, mem_coe]
Proof state after:
no goals
Theorem: Setoid.prod.pair
Proof state before:
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
⊢ (a1, b1) ≈ (a2, b2) ↔ a1 ≈ a2 ∧ b1 ≈ b2
Tactic:
constructor <;> (intro h; cases h; constructor <;> assumption)
Proof state after:
no goals
Theorem: Setoid.prod.pair
Proof state before:
case mpr
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
⊢ a1 ≈ a2 ∧ b1 ≈ b2 → (a1, b1) ≈ (a2, b2)
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
h : a1 ≈ a2 ∧ b1 ≈ b2
⊢ (a1, b1) ≈ (a2, b2)
Theorem: Setoid.prod.pair
Proof state before:
case mpr
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
h : a1 ≈ a2 ∧ b1 ≈ b2
⊢ (a1, b1) ≈ (a2, b2)
Tactic:
cases h
Proof state after:
case mpr.intro
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
left✝ : a1 ≈ a2
right✝ : b1 ≈ b2
⊢ (a1, b1) ≈ (a2, b2)
Theorem: Setoid.prod.pair
Proof state before:
case mpr.intro
α : Type u_1
β : Type u_2
a1 a2 : α
b1 b2 : β
sa : Setoid α
sb : Setoid β
left✝ : a1 ≈ a2
right✝ : b1 ≈ b2
⊢ (a1, b1) ≈ (a2, b2)
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: Quotient.prod_mk
Proof state before:
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
a : α
b : β
⊢ prod ⟦a⟧ ⟦b⟧ = ⟦(a, b)⟧
Tactic:
simp [prod]
Proof state after:
no goals
Theorem: Quotient.prod_eq_mk
Proof state before:
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
aa : Quotient sa
bb : Quotient sb
a : α
b : β
⊢ prod aa bb = ⟦(a, b)⟧ ↔ aa = ⟦a⟧ ∧ bb = ⟦b⟧
Tactic:
rcases aa.exists_rep with ⟨a',rfl⟩
Proof state after:
case intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
bb : Quotient sb
a : α
b : β
a' : α
⊢ prod ⟦a'⟧ bb = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ bb = ⟦b⟧
Theorem: Quotient.prod_eq_mk
Proof state before:
case intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
bb : Quotient sb
a : α
b : β
a' : α
⊢ prod ⟦a'⟧ bb = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ bb = ⟦b⟧
Tactic:
rcases bb.exists_rep with ⟨b',rfl⟩
Proof state after:
case intro.intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
a : α
b : β
a' : α
b' : β
⊢ prod ⟦a'⟧ ⟦b'⟧ = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ ⟦b'⟧ = ⟦b⟧
Theorem: Quotient.prod_eq_mk
Proof state before:
case intro.intro
α : Type u_1
β : Type u_2
sa : Setoid α
sb : Setoid β
a : α
b : β
a' : α
b' : β
⊢ prod ⟦a'⟧ ⟦b'⟧ = ⟦(a, b)⟧ ↔ ⟦a'⟧ = ⟦a⟧ ∧ ⟦b'⟧ = ⟦b⟧
Tactic:
simp [Setoid.prod]
Proof state after:
no goals
Theorem: Finset.mapEquiv_symm_eq
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑((mapEquiv s f).symm x) = y ↔ ↑x = f y
Tactic:
rcases x with ⟨x,hx⟩
Proof state after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : x ∈ map f s
⊢ ↑((mapEquiv s f).symm { val := x, property := hx }) = y ↔ ↑{ val := x, property := hx } = f y
Theorem: Finset.mapEquiv_symm_eq
Proof state before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : x ∈ map f s
⊢ ↑((mapEquiv s f).symm { val := x, property := hx }) = y ↔ ↑{ val := x, property := hx } = f y
Tactic:
simp [mapEquiv]
Proof state after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : x ∈ map f s
⊢ filter (fun x_1 => f x_1 = x) s = {y} ↔ x = f y
Theorem: Finset.mapEquiv_symm_eq
Proof state before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : x ∈ map f s
⊢ filter (fun x_1 => f x_1 = x) s = {y} ↔ x = f y
Tactic:
simp at hx
Proof state after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : ∃ a ∈ s, f a = x
⊢ filter (fun x_1 => f x_1 = x) s = {y} ↔ x = f y
Theorem: Finset.mapEquiv_symm_eq
Proof state before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
x : α'
hx : ∃ a ∈ s, f a = x
⊢ filter (fun x_1 => f x_1 = x) s = {y} ↔ x = f y
Tactic:
rcases hx with ⟨y',h1,rfl⟩
Proof state after:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ filter (fun x => f x = f y') s = {y} ↔ f y' = f y
Theorem: Finset.mapEquiv_symm_eq
Proof state before:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ filter (fun x => f x = f y') s = {y} ↔ f y' = f y
Tactic:
simp [eq_singleton_iff_unique_mem]
Proof state after:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ ((y ∈ s ∧ y = y') ∧ ∀ x ∈ s, x = y' → x = y) ↔ y' = y
Theorem: Finset.mapEquiv_symm_eq
Proof state before:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y y' : α
h1 : y' ∈ s
⊢ ((y ∈ s ∧ y = y') ∧ ∀ x ∈ s, x = y' → x = y) ↔ y' = y
Tactic:
aesop
Proof state after:
no goals
Theorem: Finset.eq_mapEquiv_symm
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ y = ↑((mapEquiv s f).symm x) ↔ f y = ↑x
Tactic:
rw [eq_comm]
Proof state after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑((mapEquiv s f).symm x) = y ↔ f y = ↑x
Theorem: Finset.eq_mapEquiv_symm
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑((mapEquiv s f).symm x) = y ↔ f y = ↑x
Tactic:
simp
Proof state after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑x = f y ↔ f y = ↑x
Theorem: Finset.eq_mapEquiv_symm
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
y : α
⊢ ↑x = f y ↔ f y = ↑x
Tactic:
apply eq_comm
Proof state after:
no goals
Theorem: Finset.app_mapEquiv_symm
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
f' : α → α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
⊢ f' = f.toFun → f' ↑((mapEquiv s f).symm x) = ↑x
Tactic:
rintro rfl
Proof state after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
⊢ f.toFun ↑((mapEquiv s f).symm x) = ↑x
Theorem: Finset.app_mapEquiv_symm
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : { x // x ∈ map f s }
⊢ f.toFun ↑((mapEquiv s f).symm x) = ↑x
Tactic:
rcases x with ⟨x,hx⟩
Proof state after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx : x ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx }) = ↑{ val := x, property := hx }
Theorem: Finset.app_mapEquiv_symm
Proof state before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx : x ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx }) = ↑{ val := x, property := hx }
Tactic:
simp at hx
Proof state after:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx✝ : x ∈ map f s
hx : ∃ a ∈ s, f a = x
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx✝ }) = ↑{ val := x, property := hx✝ }
Theorem: Finset.app_mapEquiv_symm
Proof state before:
case mk
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α'
hx✝ : x ∈ map f s
hx : ∃ a ∈ s, f a = x
⊢ f.toFun ↑((mapEquiv s f).symm { val := x, property := hx✝ }) = ↑{ val := x, property := hx✝ }
Tactic:
rcases hx with ⟨y,_,rfl⟩
Proof state after:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
left✝ : y ∈ s
hx : f y ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := f y, property := hx }) = ↑{ val := f y, property := hx }