Theorem: Set.one_lt_encard_iff_nontrivial (Jordan/Mathlib/Set.lean)

State before:
α : Type u_1
s : Set α
⊢ 1 < encard s ↔ Set.Nontrivial s
Tactic:
unfold Set.Nontrivial
State after:
α : Type u_1
s : Set α
⊢ 1 < encard s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

State before:
α : Type u_1
s : Set α
⊢ 1 < encard s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
Tactic:
rw [Set.one_lt_encard_iff]
State after:
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

State before:
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y
Tactic:
constructor
State after:
case mp
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) → ∃ x ∈ s, ∃ y ∈ s, x ≠ y

case mpr
α : Type u_1
s : Set α
⊢ (∃ x ∈ s, ∃ y ∈ s, x ≠ y) → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

State before:
case mp
α : Type u_1
s : Set α
⊢ (∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b) → ∃ x ∈ s, ∃ y ∈ s, x ≠ y

case mpr
α : Type u_1
s : Set α
⊢ (∃ x ∈ s, ∃ y ∈ s, x ≠ y) → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic:
all_goals {
  rintro ⟨a, b, c, d, e⟩
  exact ⟨a, c, b, d, e⟩ }
State after:
no goals

State before:
case mpr
α : Type u_1
s : Set α
⊢ (∃ x ∈ s, ∃ y ∈ s, x ≠ y) → ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic:
rintro ⟨a, b, c, d, e⟩
State after:
case mpr.intro.intro.intro.intro
α : Type u_1
s : Set α
a : α
b : a ∈ s
c : α
d : c ∈ s
e : a ≠ c
⊢ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

State before:
case mpr.intro.intro.intro.intro
α : Type u_1
s : Set α
a : α
b : a ∈ s
c : α
d : c ∈ s
e : a ≠ c
⊢ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic:
exact ⟨a, c, b, d, e⟩
State after:
no goals