-- Mathlib/Data/Finset/Fold.lean
theorem fold_op_rel_iff_and {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ r x y ∧ r x z)
    {c : β} : r c (s.fold op b f) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Proof state:
case insert.mp
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
⊢ (r c (f a) ∧ ∀ x ∈ s, r c (f x)) → ∀ x ∈ insert a s, r c (f x)

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case insert.mp.intro
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h₁ : r c (f a)
h₂ : ∀ x ∈ s, r c (f x)
⊢ ∀ x ∈ insert a s, r c (f x)

Proof state:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
⊢ r c (fold op b f (insert a s)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]

Result:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
⊢ (r c b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Proof state:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
⊢ (r c b ∧ r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ r c b ∧ ∀ x ∈ insert a s, r c (f x)

Tactic:
apply and_congr Iff.rfl

Result:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
⊢ (r c (f a) ∧ ∀ x ∈ s, r c (f x)) ↔ ∀ x ∈ insert a s, r c (f x)

Proof state:
case insert.mpr.left
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h : ∀ x ∈ insert a s, r c (f x)
⊢ r c (f a)

Tactic:
exact h a (Finset.mem_insert_self _ _)

Result:
no goals

Proof state:
case insert.mp.intro
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b✝ : β
s✝ : Finset α
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 ∈ s, r c (f x)
h₁ : r c (f a)
h₂ : ∀ x ∈ s, r c (f x)
b : α
hb : b = a ∨ b ∈ s
⊢ r c (f b)

Tactic:
rcases hb with (rfl | hb) <;> solve_by_elim

Result:
no goals

Proof state:
case insert.mpr
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h : ∀ x ∈ insert a s, r c (f x)
⊢ r c (f a) ∧ ∀ x ∈ s, r c (f x)

Tactic:
constructor

Result:
case insert.mpr.left
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h : ∀ x ∈ insert a s, r c (f x)
⊢ r c (f a)

case insert.mpr.right
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h : ∀ x ∈ insert a s, r c (f x)
⊢ ∀ x ∈ s, r c (f x)

Proof state:
case insert.mpr.right
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h : ∀ x ∈ insert a s, r c (f x)
⊢ ∀ x ∈ s, r c (f x)

Tactic:
exact fun b hb => h b <| Finset.mem_insert_of_mem hb

Result:
no goals

Proof state:
case insert.mp.intro
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h₁ : r c (f a)
h₂ : ∀ x ∈ s, r c (f x)
⊢ ∀ x ∈ insert a s, r c (f x)

Tactic:
intro b hb

Result:
case insert.mp.intro
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b✝ : β
s✝ : Finset α
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 ∈ s, r c (f x)
h₁ : r c (f a)
h₂ : ∀ x ∈ s, r c (f x)
b : α
hb : b ∈ insert a s
⊢ r c (f b)

Proof state:
case empty
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
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 ∈ ∅, r c (f x)

Tactic:
simp

Result:
no goals

Proof state:
case insert.mpr
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
⊢ (∀ x ∈ insert a s, r c (f x)) → r c (f a) ∧ ∀ x ∈ s, r c (f x)

Tactic:
intro h

Result:
case insert.mpr
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b : β
s✝ : Finset α
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 ∈ s, r c (f x)
h : ∀ x ∈ insert a s, r c (f x)
⊢ r c (f a) ∧ ∀ x ∈ s, r c (f x)

Proof state:
case insert.mp.intro
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b✝ : β
s✝ : Finset α
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 ∈ s, r c (f x)
h₁ : r c (f a)
h₂ : ∀ x ∈ s, r c (f x)
b : α
hb : b ∈ insert a s
⊢ r c (f b)

Tactic:
rw [Finset.mem_insert] at hb

Result:
case insert.mp.intro
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha✝ : Std.Associative op
f : α → β
b✝ : β
s✝ : Finset α
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 ∈ s, r c (f x)
h₁ : r c (f a)
h₂ : ∀ x ∈ s, r c (f x)
b : α
hb : b = a ∨ b ∈ s
⊢ r c (f b)