awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match (motive := Option α → α) none with
      | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))

Tactic:
(Classical.choose_spec (hf p p)).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p : α
⊢ r (f p)
    (f
      (match (motive := Option α → α) none with
      | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))

Tactic:
exact (Classical.choose_spec (hf p p)).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
⊢ r (f p)
    (f
      (match (motive := Option α → α) some a with
      | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))

Tactic:
(Classical.choose_spec (hf p a)).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
p a : α
⊢ r (f p)
    (f
      (match (motive := Option α → α) some a with
      | none => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f p) (f x)) ⋯
      | some a => Classical.choose (p := fun (x : α) ↦ r (f p) (f x) ∧ r (f a) (f x)) ⋯))

Tactic:
exact (Classical.choose_spec (hf p a)).1

Premises used: Classical.choose_spec, And.left
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
simp :
  r (f a)
    (f
      (Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf (encode a))) (f x) ∧ r (f a) (f x))
        ⋯))
⊢ r (f a) (f (Directed.sequence (r := r) f hf (encode a + 1)))

Tactic:
simp only [Directed.sequence, encodek]

Premises used: Encodable.encodek, Directed.sequence
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a)
    (f
      (Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf (encode a))) (f x) ∧ r (f a) (f x))
        ⋯))

Tactic:
(Classical.choose_spec (hf _ a)).2

Premises used: Classical.choose_spec, And.right
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
a : α
⊢ r (f a)
    (f
      (Classical.choose (p := fun (x : α) ↦ r (f (Directed.sequence (r := r) f hf (encode a))) (f x) ∧ r (f a) (f x))
        ⋯))

Tactic:
exact (Classical.choose_spec (hf _ a)).2

Premises used: Classical.choose_spec, And.right
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
inst_2 : Preorder β
f : α → β
hf : Directed (fun (x1 x2 : β) ↦ x1 ≤ x2) f
⊢ Monotone (f ∘ Directed.sequence (r := fun (x1 x2 : β) ↦ x1 ≤ x2) f hf)

Tactic:
monotone_nat_of_le_succ <| hf.sequence_mono_nat

Premises used: Directed.sequence_mono_nat, monotone_nat_of_le_succ
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
inst_2 : Preorder β
f : α → β
hf : Directed (fun (x1 x2 : β) ↦ x1 ≤ x2) f
a : α
⊢ f a ≤ f (Directed.sequence (r := fun (x1 x2 : β) ↦ x1 ≤ x2) f hf (encode a + 1))

Tactic:
hf.rel_sequence a

Premises used: Directed.rel_sequence
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
inst_2 : Preorder β
f : α → β
hf : Directed (fun (x1 x2 : β) ↦ x1 ≥ x2) f
⊢ Antitone (f ∘ Directed.sequence (r := fun (x1 x2 : β) ↦ x1 ≥ x2) f hf)

Tactic:
antitone_nat_of_succ_le <| hf.sequence_mono_nat

Premises used: Directed.sequence_mono_nat, antitone_nat_of_succ_le
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Encodable α
inst_1 : Inhabited α
inst_2 : Preorder β
f : α → β
hf : Directed (fun (x1 x2 : β) ↦ x1 ≥ x2) f
a : α
⊢ f (Directed.sequence (r := fun (x1 x2 : β) ↦ x1 ≥ x2) f hf (encode a + 1)) ≤ f a

Tactic:
hf.rel_sequence a

Premises used: Directed.rel_sequence
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
s : Setoid α
inst : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
inst_1 : Encodable α
q : Quotient s
⊢ ⟦q.rep⟧ = q

Tactic:
choose_spec (exists_rep q)

Premises used: Encodable.choose_spec, Quotient.exists_rep, Quotient.rep
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
s : Setoid α
inst : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
inst_1 : Encodable α
a : Quotient s
l : α
mk :
  Eq (α := Option (Quotient s))
    (Option.map Quotient.mk'' (decode (encode (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l)))))
    (some (Quot.mk (⇑s : α → α → Prop) l))
⊢ Eq (α := Option (Quotient s))
    ((fun (n : ℕ) ↦ (Quotient.mk'' <$> decode n : Option (Quotient s)))
      ((fun (q : Quotient s) ↦ encode q.rep) (Quot.mk (⇑s : α → α → Prop) l)))
    (some (Quot.mk (⇑s : α → α → Prop) l))

Tactic:
dsimp
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
s : Setoid α
inst : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
inst_1 : Encodable α
a : Quotient s
l : α
mk :
  Eq (α := Option (Quotient s)) (Option.map Quotient.mk'' (some (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l))))
    (some (Quot.mk (⇑s : α → α → Prop) l))
⊢ Eq (α := Option (Quotient s))
    (Option.map Quotient.mk'' (decode (encode (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l)))))
    (some (Quot.mk (⇑s : α → α → Prop) l))

Tactic:
rw [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
s : Setoid α
inst : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
inst_1 : Encodable α
a : Quotient s
l : α
⊢ Eq (α := Option (Quotient s)) (Option.map Quotient.mk'' (some (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l))))
    (some (Quot.mk (⇑s : α → α → Prop) l))

Tactic:
congr_arg some ⟦l⟧.rep_spec

Premises used: Quotient.rep_spec, Option.some, Quotient.mk, congr_arg
-- Module: Mathlib.Logic.Encodable.Basic
Goal:
α : Type u_1
s : Setoid α
inst : DecidableRel fun (x1 x2 : α) ↦ x1 ≈ x2
inst_1 : Encodable α
a : Quotient s
l : α
⊢ Eq (α := Option (Quotient s)) (Option.map Quotient.mk'' (some (rep (s := s) (Quot.mk (⇑s : α → α → Prop) l))))
    (some (Quot.mk (⇑s : α → α → Prop) l))

Tactic:
exact congr_arg some ⟦l⟧.rep_spec

Premises used: Quotient.rep_spec, Option.some, Quotient.mk, congr_arg
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
inst_1 : CompleteLattice α
f : β → α
rw : Eq.{u_1 + 1} (α := α) (⨆ (j : β), ⨆ (i : ℕ), ⨆ (_ : j ∈ decode₂ β i), f j) (⨆ (b : β), f b)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), ⨆ b ∈ decode₂ β i, f b) (⨆ (b : β), f b)

Tactic:
rw [iSup_comm]

Premises used: iSup_comm
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
inst_1 : CompleteLattice α
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (j : β), ⨆ (i : ℕ), ⨆ (_ : j ∈ decode₂ β i), f j) (⨆ (b : β), f b)

Tactic:
simp only [mem_decode₂, iSup_iSup_eq_right]

Premises used: Encodable.mem_decode₂, iSup_iSup_eq_right
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), ⋃ b ∈ decode₂ β i, f b) (⋃ (b : β), f b)

Tactic:
iSup_decode₂ f

Premises used: Encodable.iSup_decode₂, Set.iUnion
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
simp : C ∅
⊢ C (⋃ (b : β), ⋃ (_ : Membership.mem (γ := Option β) none b), f b)

Tactic:
simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]

Premises used: reduceCtorEq, Set.iUnion_of_empty, Set.iUnion_empty, Option.mem_def
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C ∅

Tactic:
apply H0
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ C (f b)

Tactic:
H1 b
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
h : ⋃ b_1 ∈ some b, f b_1 = f b
⊢ C (⋃ b_1 ∈ some b, f b_1)

Tactic:
convert! H1 b
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
b : β
⊢ ⋃ b_1 ∈ some b, f b_1 = f b

Tactic:
simp
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint (fun (i : ℕ) ↦ ⋃ b ∈ decode₂ β i, f b) i j

Tactic:
disjoint_left.mpr fun x => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
refine :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) i) x →
      x ∉ (fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) j
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint (fun (i : ℕ) ↦ ⋃ b ∈ decode₂ β i, f b) i j

Tactic:
refine disjoint_left.mpr fun x => ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
this : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b
⊢ Membership.mem (γ := Set α) ((fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) i) x →
    x ∉ (fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) j

Tactic:
simpa [decode₂_eq_some]

Premises used: Encodable.decode₂_eq_some
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
suffices : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b
⊢ Membership.mem (γ := Set α) ((fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) i) x →
    x ∉ (fun (i : ℕ) ↦ (⋃ b ∈ decode₂ β i, f b : Set α)) j

Tactic:
suffices ∀ a, encode a = i → x ∈ f a → ∀ b, encode b = j → x ∉ f b by simpa [decode₂_eq_some]
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False

Tactic:
(hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩

Premises used: Disjoint.le_bot, Set.Mem, mt, congr_arg, And.intro, Encodable.encode
-- Module: Mathlib.Logic.Encodable.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
x : α
a : β
ha : x ∈ f a
b : β
ij : encode a ≠ encode b
hb : x ∈ f b
⊢ False

Tactic:
exact (hd (mt (congr_arg encode) ij)).le_bot ⟨ha, hb⟩

Premises used: Disjoint.le_bot, mt, congr_arg, And.intro, Encodable.encode
-- Module: Mathlib.Logic.Encodable.Pi
Goal:
α : Type u_1
inst : Countable α
n : ℕ
⊢ Countable.{u_1 + 1} (List.Vector α n)

Tactic:
inferInstanceAs <| Countable (Subtype _)

Premises used: _private.0.Encodable.List.Vector.countable._proof_1
-- Module: Mathlib.Logic.Equiv.Array
Goal:
α : Type u_1
inst : Countable α
⊢ Countable.{u_1 + 1} (Array α)

Tactic:
Countable.of_equiv _ (Equiv.arrayEquivList α).symm

Premises used: Countable.of_equiv, Equiv.arrayEquivList, Equiv.symm
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_10
β : Option α → Type u_9
f : (a : Option α) → β a
a : Option α
none :
  Eq (α := β Option.none)
    ((fun (x : β Option.none × ((a : α) → β (Option.some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦
          ((f Option.none, fun (a : α) ↦ f (Option.some a)) : β Option.none × ((a : α) → β (Option.some a))))
        f)
      Option.none)
    (f Option.none)
some :
  ∀ (val : α),
    Eq (α := β (Option.some val))
      ((fun (x : β Option.none × ((a : α) → β (Option.some a))) (a : Option α) ↦
          Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
        ((fun (f : (a : Option α) → β a) ↦
            ((f Option.none, fun (a : α) ↦ f (Option.some a)) : β Option.none × ((a : α) → β (Option.some a))))
          f)
        (Option.some val))
      (f (Option.some val))
⊢ (fun (x : β Option.none × ((a : α) → β (Option.some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦
          ((f Option.none, fun (a : α) ↦ f (Option.some a)) : β Option.none × ((a : α) → β (Option.some a))))
        f)
      a =
    f a

Tactic:
cases a
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_10
β : Option α → Type u_9
f : (a : Option α) → β a
⊢ Eq (α := β none)
    ((fun (x : β none × ((a : α) → β (some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦ ((f none, fun (a : α) ↦ f (some a)) : β none × ((a : α) → β (some a)))) f)
      none)
    (f none)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_10
β : Option α → Type u_9
f : (a : Option α) → β a
val : α
⊢ Eq (α := β (some val))
    ((fun (x : β none × ((a : α) → β (some a))) (a : Option α) ↦
        Option.casesOn (motive := fun (x : Option α) ↦ β x) a x.fst x.snd)
      ((fun (f : (a : Option α) → β a) ↦ ((f none, fun (a : α) ↦ f (some a)) : β none × ((a : α) → β (some a)))) f)
      (some val))
    (f (some val))

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : ε
pos :
  ∀ (h : p a),
    Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
      (if h : p a then
          (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
        else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
        ε)
neg :
  ∀ (h : ¬p a),
    Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
      (if h : p a then
          (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
        else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
        ε)
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    (if h : p a then (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
      else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
      ε)

Tactic:
by_cases h : p a
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : ε
h : p a
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    (if h : p a then (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
      else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
      ε)

Tactic:
simp [Perm.subtypeCongr, h]

Premises used: Equiv.Perm.subtypeCongr
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : ε
h : ¬p a
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    (if h : p a then (↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε)
      else (↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) :
      ε)

Tactic:
simp [Perm.subtypeCongr, h]

Premises used: Equiv.Perm.subtypeCongr
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : ε
h : p a
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    ((↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) (Subtype.mk (p := fun (a : ε) ↦ p a) a h)) : ε) : ε)

Tactic:
simp [Perm.subtypeCongr.apply, h]

Premises used: Equiv.Perm.subtypeCongr.apply
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : { a : ε // p a }
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) (↑a : ε) : ε)
    ((↑((ep : (a : { a : ε // p a }) → { a : ε // p a }) a) : ε) : ε)

Tactic:
Perm.subtypeCongr.left_apply ep en a.property

Premises used: Equiv.Perm.subtypeCongr.left_apply, Subtype.property
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : ε
h : ¬p a
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) a : ε)
    ((↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) (Subtype.mk (p := fun (a : ε) ↦ ¬p a) a h)) : ε) : ε)

Tactic:
simp [Perm.subtypeCongr.apply, h]

Premises used: Equiv.Perm.subtypeCongr.apply
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
a : { a : ε // ¬p a }
⊢ Eq (α := ε) ((ep.subtypeCongr (p := p) en : (a : ε) → ε) (↑a : ε) : ε)
    ((↑((en : (a : { a : ε // ¬p a }) → { a : ε // ¬p a }) a) : ε) : ε)

Tactic:
Perm.subtypeCongr.right_apply ep en a.property

Premises used: Equiv.Perm.subtypeCongr.right_apply, Subtype.property
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
H :
  ∀ (x : ε),
    Eq (α := ε)
      ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
      ((Equiv.refl ε : (a : ε) → ε) x : ε)
⊢ subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) = Equiv.refl ε

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
x : ε
pos :
  ∀ (h : p x),
    Eq (α := ε)
      ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
      ((Equiv.refl ε : (a : ε) → ε) x : ε)
neg :
  ∀ (h : ¬p x),
    Eq (α := ε)
      ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
      ((Equiv.refl ε : (a : ε) → ε) x : ε)
⊢ Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)

Tactic:
by_cases h : p x
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
x : ε
h : p x
⊢ Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
x : ε
h : ¬p x
⊢ Eq (α := ε) ((subtypeCongr (p := p) (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) : (a : ε) → ε) x : ε)
    ((Equiv.refl ε : (a : ε) → ε) x : ε)

Tactic:
simp [h]
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep : Perm { a : ε // p a }
en : Perm { a : ε // ¬p a }
⊢ Equiv.symm (ep.subtypeCongr (p := p) en) = subtypeCongr (p := p) (Equiv.symm ep) (Equiv.symm en)

Tactic:
rfl

Premises used: Sum.map, Equiv.trans, Equiv.Perm.subtypeCongr, Equiv.symm, rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
ε : Type u_9
p : ε → Prop
inst : DecidablePred p
ep ep' : Perm { a : ε // p a }
en en' : Perm { a : ε // ¬p a }
⊢ Equiv.trans (ep.subtypeCongr (p := p) en) (ep'.subtypeCongr (p := p) en') =
    subtypeCongr (p := p) (Equiv.trans ep ep') (Equiv.trans en en')

Tactic:
grind [eq_def, coe_trans]

Premises used: Equiv.Perm.subtypeCongr.eq_def, Equiv.coe_trans
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
dsimp : (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x a) = x a
⊢ (↑((fun (x : { a : α // ¬p a } → β) ↦
              (Subtype.mk (p := fun (x : α → β) ↦ x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀)
                  (fun (a : α) ↦
                    if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h)
                    else x (Subtype.mk (p := fun (a : α) ↦ ¬p a) a h))
                  ⋯ :
                { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }))
            ((fun (x : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }) (a : { a : α // ¬p a }) ↦
                (↑x : α → β) (↑a : α))
              (Subtype.mk (p := fun (x : α → β) ↦ x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀) x hx))) :
        α → β)
      a =
    (↑(Subtype.mk (p := fun (x : α → β) ↦ x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀) x hx) : α → β) a

Tactic:
dsimp only
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
pos : ∀ (h : p a), x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a
neg : ¬p a → x a = x a
⊢ (if h : p a then x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) else x a) = x a

Tactic:
split_ifs
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
h : p a
pos : (x ∘ Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a
⊢ x₀ (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a

Tactic:
rw [← hx]
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
h : p a
⊢ (x ∘ Subtype.val (p := fun (a : α) ↦ p a)) (Subtype.mk (p := fun (a : α) ↦ p a) a h) = x a

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Basic
Goal:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
inst : DecidablePred p
x₀ : { a : α // p a } → β
x_1 : { x : α → β // x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀ }
x : α → β
hx : x ∘ Subtype.val (p := fun (a : α) ↦ p a) = x₀
a : α
h : ¬p a
⊢ x a = x a

Tactic:
rfl