Theorem: HFSet.induction' (Hfzfa.lean)

State before:
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
⊢ motive y
Tactic:
cases H : y.isAtom
State after:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y

case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y

State before:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y

case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y
Tactic:
swap
State after:
case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y

case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y

State before:
case true
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = true
⊢ motive y
Tactic:
rcases isAtom_eq_true_iff.mp H with ⟨a, rfl⟩
State after:
case true.intro
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
a : atoms
ih : ∀ (z : HFSet atoms), z ∈ atom a → motive z
H : isAtom (atom a) = true
⊢ motive (atom a)

State before:
case true.intro
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
a : atoms
ih : ∀ (z : HFSet atoms), z ∈ atom a → motive z
H : isAtom (atom a) = true
⊢ motive (atom a)
Tactic:
exact h₁ a
State after:
no goals

State before:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y
Tactic:
classical
simpa [H] using h₂ y.toFinset (by simpa)
State after:
no goals

State before:
case false
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ motive y
Tactic:
simpa [H] using h₂ y.toFinset (by simpa)
State after:
no goals

State before:
atoms : Type u_1
motive : HFSet atoms → Prop
x : HFSet atoms
h₁ : ∀ (a : atoms), motive (atom a)
h₂ : ∀ (s : Finset (HFSet atoms)), (∀ (y : HFSet atoms), y ∈ s → motive y) → motive (ofFinset s)
y : HFSet atoms
ih : ∀ (z : HFSet atoms), z ∈ y → motive z
H : isAtom y = false
⊢ ∀ (y_1 : HFSet atoms), y_1 ∈ toFinset y → motive y_1
Tactic:
simpa
State after:
no goals