case empty
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∨ ∃ x, x ∈ ∅ ∧ r c (f x)

case insert
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
induction' s using Finset.induction_on with a s ha IH
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ ∃ x, x ∈ insert a s ∧ r c (f x)
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c b ∨ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ r c b ∨ ∃ x, x ∈ insert a s ∧ r c (f x)
apply or_congr Iff.rfl
case insert.mp
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) → ∃ x, x ∈ insert a s ∧ r c (f x)

case insert.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (∃ x, x ∈ insert a s ∧ r c (f x)) → r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
case insert
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) ↔ ∃ x, x ∈ insert a s ∧ r c (f x)
constructor
no goals
case empty
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
⊢ r c (fold op b f ∅) ↔ r c b ∨ ∃ x, x ∈ ∅ ∧ r c (f x)
simp
case insert.mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)

case insert.mp.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ s
h₂ : r c (f x)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)
case insert.mp
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)) → ∃ x, x ∈ insert a s ∧ r c (f x)
rintro (h₁ | ⟨x, hx, h₂⟩)
case insert.mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ a ∈ insert a s ∧ r c (f a)
case insert.mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)
use a
no goals
case insert.mp.inl
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
h₁ : r c (f a)
⊢ a ∈ insert a s ∧ r c (f a)
simp [h₁]
no goals
case insert.mp.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ s
h₂ : r c (f x)
⊢ ∃ x, x ∈ insert a s ∧ r c (f x)
refine' ⟨x, by simp [hx], h₂⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ s
h₂ : r c (f x)
⊢ x ∈ insert a s
simp [hx]
case insert.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ insert a s
h : r c (f x)
⊢ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
case insert.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
⊢ (∃ x, x ∈ insert a s ∧ r c (f x)) → r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
rintro ⟨x, hx, h⟩
no goals
case insert.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx : x ∈ insert a s
h : r c (f x)
⊢ r c (f a) ∨ ∃ x, x ∈ s ∧ r c (f x)
exact (mem_insert.mp hx).imp (fun hx => by rwa [hx] at h) (fun hx => ⟨x, hx, h⟩)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.60299
op : β → β → β
hc : IsCommutative β op
ha✝ : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a✝ : α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∨ r x z
c : β
a : α
s : Finset α
ha : ¬a ∈ s
IH : r c (fold op b f s) ↔ r c b ∨ ∃ x, x ∈ s ∧ r c (f x)
x : α
hx✝ : x ∈ insert a s
h : r c (f x)
hx : x = a
⊢ r c (f a)
rwa [hx] at h