Theorem: List.Perm.find?_unique (LeanSAT/Upstream/ToMathlib.lean)

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

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

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?]
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₂✝

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

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

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

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

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

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

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