awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi : P a s
refine : ∀ (a : α) (t : Finset α) (_ta : a ∉ t) (hi : P {x} t), P (insert a t) {x}
⊢ P {x} a

Tactic:
refine Finset.induction_on a empty_right fun a t _ta hi => symm ?_
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a_1 b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi_1 : P a_1 s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
rw : P ({a} ∪ t) {x}
⊢ P (insert a t) {x}

Tactic:
rw [Finset.insert_eq]

Premises used: Finset.insert_eq
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a_1 b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi_1 : P a_1 s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P ({a} ∪ t) {x}

Tactic:
union_of singletons (symm hi)
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a_1 b : Finset α
x : α
s : Finset α
_xs : x ∉ s
hi_1 : P a_1 s
a : α
t : Finset α
_ta : a ∉ t
hi : P {x} t
⊢ P ({a} ∪ t) {x}

Tactic:
exact union_of singletons (symm hi)
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x : α
⊢ x ∈ s ∧ Membership.mem (γ := Finset α) ∅ x ↔ Membership.mem (γ := Finset α) ∅ x

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x : α
⊢ Membership.mem (γ := Finset α) ∅ x ∧ x ∈ s ↔ Membership.mem (γ := Finset α) ∅ x

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂

Tactic:
h
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂

Tactic:
exact h
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x = a ∨ x ∈ s₂ ↔ x ∈ s₂

Tactic:
have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
this : x = a ∨ x ∈ s₂ ↔ x ∈ s₂
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)

Tactic:
simp only [mem_inter, mem_insert, or_and_left, this]

Premises used: Finset.mem_insert, or_and_left, Finset.mem_inter
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
rw : insert a s₂ ∩ s₁ = insert a (s₁ ∩ s₂)
rw₁ : insert a (s₂ ∩ s₁) = insert a (s₁ ∩ s₂)
rw₂ rw₃ : insert a (s₁ ∩ s₂) = insert a (s₁ ∩ s₂)
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Tactic:
rw [inter_comm, insert_inter_of_mem h, inter_comm]

Premises used: Finset.inter_comm, Finset.insert_inter_of_mem
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : x ∉ s₂
⊢ False

Tactic:
h H
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : x ∉ s₂
⊢ False

Tactic:
exact h H
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
⊢ ¬(x = a ∧ x ∈ s₂)

Tactic:
have : ¬(x = a ∧ x ∈ s₂) := by rintro ⟨rfl, H⟩; exact h H
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
this : ¬(x = a ∧ x ∈ s₂)
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂

Tactic:
simp only [mem_inter, mem_insert, or_and_right, this, false_or]

Premises used: Finset.mem_insert, false_or, Finset.mem_inter, or_and_right
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
rw : insert a s₂ ∩ s₁ = s₁ ∩ s₂
rw₁ : s₂ ∩ s₁ = s₁ ∩ s₂
rw₂ rw₃ : s₁ ∩ s₂ = s₁ ∩ s₂
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂

Tactic:
rw [inter_comm, insert_inter_of_notMem h, inter_comm]

Premises used: Finset.insert_inter_of_notMem, Finset.inter_comm
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
pos : a ∈ s₂ → insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)
neg : a ∉ s₂ → insert a s₁ ∩ s₂ = s₁ ∩ s₂
⊢ insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
split_ifs
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
⊢ insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
⊢ insert a s₁ ∩ s₂ = s₁ ∩ s₂

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
pos : a ∈ s₁ → s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
neg : a ∉ s₁ → s₁ ∩ insert a s₂ = s₁ ∩ s₂
⊢ s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
split_ifs
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
H : a ∈ s
rw : insert a (∅ ∩ s) = insert a ∅
rw₁ rw₂ : Eq (α := Finset α) (insert a ∅) (insert a ∅)
⊢ insert a ∅ ∩ s = insert a ∅

Tactic:
rw [insert_inter_of_mem H, empty_inter]

Premises used: Finset.empty_inter, Finset.insert_inter_of_mem
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
H : a ∉ s
simp : ∀ (x : α), ¬(x = a ∧ x ∈ s)
⊢ ∀ (x : α), x ∉ {a} ∩ s

Tactic:
simp only [mem_inter, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_inter
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x : α
h : x ∈ s
H : x ∉ s
⊢ False

Tactic:
H h
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
x : α
h : x ∈ s
H : x ∉ s
⊢ False

Tactic:
exact H h
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
pos : ∀ (h : a ∈ s), {a} ∩ s = {a}
neg : ∀ (h : a ∉ s), {a} ∩ s = ∅
⊢ {a} ∩ s = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} ∩ s = {a}

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ {a} ∩ s = ∅

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∈ s
rw : {a} ∩ s = {a}
rw₁ rw₂ : Eq (α := Finset α) {a} {a}
⊢ s ∩ {a} = {a}

Tactic:
rw [inter_comm, singleton_inter_of_mem h]

Premises used: Finset.inter_comm, Finset.singleton_inter_of_mem
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
rw : {a} ∩ s = ∅
rw₁ rw₂ : Eq.{u_1 + 1} (α := Finset α) ∅ ∅
⊢ s ∩ {a} = ∅

Tactic:
rw [inter_comm, singleton_inter_of_notMem h]

Premises used: Finset.inter_comm, Finset.singleton_inter_of_notMem
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
pos : ∀ (h : a ∈ s), s ∩ {a} = {a}
neg : ∀ (h : a ∉ s), s ∩ {a} = ∅
⊢ s ∩ {a} = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
sup_eq_bot_iff

Premises used: sup_eq_bot_iff
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty

Tactic:
mod_cast Set.union_nonempty (α := α) (s := s) (t := t)

Premises used: Set.union_nonempty, Finset.coe_nonempty._simp_1, congrArg, Finset.coe_union._simp_1, cast, Iff, Set.Nonempty, congr, Or, Eq.trans
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
a : α
rw : insert a (s ∪ t) = s ∪ insert a t
rw₁ rw₂ : insert a (s ∪ t) = insert a (s ∪ t)
⊢ insert a s ∪ t = s ∪ insert a t

Tactic:
rw [insert_union, union_insert]

Premises used: Finset.insert_union, Finset.union_insert
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
⊢ ([] ++ l').toFinset = toFinset [] ∪ l'.toFinset

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
hd : α
tl : List α
hl : (tl ++ l').toFinset = tl.toFinset ∪ l'.toFinset
⊢ (hd :: tl ++ l').toFinset = (hd :: tl).toFinset ∪ l'.toFinset

Tactic:
simp [hl]
-- Module: Mathlib.Data.Finset.Lattice.Lemmas
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
nil : ([] ++ l').toFinset = toFinset [] ∪ l'.toFinset
cons :
  ∀ (hd : α) (tl : List α) (hl : (tl ++ l').toFinset = tl.toFinset ∪ l'.toFinset),
    (hd :: tl ++ l').toFinset = (hd :: tl).toFinset ∪ l'.toFinset
⊢ (l ++ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
induction l with
  | nil => simp
  | cons hd tl hl => simp [hl]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := α) (inf ∅ fun (i : ι) ↦ (t i).sup (f i))
    (sup (pi (β := κ) ∅ t) fun (g : (a : ι) → Membership.mem (γ := Finset ι) ∅ a → κ a) ↦
      inf (attach ∅) fun (i : ↥∅) ↦ f (↑i : ι) (g (↑i : ι) ⋯))

Tactic:
simp
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
⊢ Eq.{u_1 + 1} (α := α) ((insert i s).inf fun (i : ι) ↦ (t i).sup (f i))
    (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
      (insert i s).attach.inf fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))

Tactic:
?_
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (ih :
      Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
        ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦
          s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))),
    Eq.{u_1 + 1} (α := α) ((Insert.insert i s).inf fun (i : ι) ↦ (t i).sup (f i))
      (((Insert.insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ Insert.insert i s → κ a) ↦
        (Insert.insert i s).attach.inf fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))
⊢ Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert i s hi ih => ?_

Premises used: Insert.insert
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
insert :
  Eq.{u_1 + 1} (α := α)
    ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
      f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) ⋯))
    (((Insert.insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ Insert.insert i s → κ a) ↦
      inf
        (Insert.insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) i ⋯)
          (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) s.attach))
        fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))
⊢ Eq.{u_1 + 1} (α := α) ((Insert.insert i s).inf fun (i : ι) ↦ (t i).sup (f i))
    (((Insert.insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ Insert.insert i s → κ a) ↦
      (Insert.insert i s).attach.inf fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))

Tactic:
rw [inf_insert, ih, attach_insert, sup_inf_sup]

Premises used: Finset.attach_insert, Finset.inf_insert, Finset.sup_inf_sup
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
⊢ Eq.{u_1 + 1} (α := α)
    ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
      f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) ⋯))
    (((insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ insert i s → κ a) ↦
      inf
        (insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) i ⋯)
          (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) s.attach))
        fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))

Tactic:
eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
insert :
  ∀ (c : α),
    ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
          f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) ⋯)) ≤
        c ↔
      (((Insert.insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ Insert.insert i s → κ a) ↦
          inf
            (Insert.insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) i ⋯)
              (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) s.attach))
            fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯)) ≤
        c
⊢ Eq.{u_1 + 1} (α := α)
    ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
      f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) ⋯))
    (((Insert.insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ Insert.insert i s → κ a) ↦
      inf
        (Insert.insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) i ⋯)
          (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) s.attach))
        fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯))

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
insert :
  (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
      a ∈ t i →
        (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (b (↑i : ι) ⋯)) ≤ c) ↔
    ∀ (b : (a : ι) → a ∈ Insert.insert i s → κ a),
      (∀ (a : ι) (h : a ∈ Insert.insert i s), b a h ∈ t a) →
        f i (b i ⋯) ⊓
            s.attach.inf
              ((fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
                Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) ≤
          c
⊢ ((t i ×ˢ s.pi (β := κ) t).sup fun (i_1 : κ i × ((a : ι) → a ∈ s → κ a)) ↦
        f i i_1.1 ⊓ s.attach.inf fun (i_2 : ↥s) ↦ f (↑i_2 : ι) (i_1.2 (↑i_2 : ι) ⋯)) ≤
      c ↔
    (((Insert.insert i s).pi (β := κ) t).sup fun (g : (a : ι) → a ∈ Insert.insert i s → κ a) ↦
        inf
          (Insert.insert (Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) i ⋯)
            (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) s.attach))
          fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (g (↑i_1 : ι) ⋯)) ≤
      c

Tactic:
simp only [Finset.sup_le_iff, mem_product, mem_pi, and_imp, Prod.forall,
    inf_insert, inf_image]

Premises used: and_imp, Finset.inf_image, Finset.inf_insert, Finset.mem_pi, Prod.forall, Finset.sup_le_iff, Finset.mem_product
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
⊢ (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
      a ∈ t i →
        (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (b (↑i : ι) ⋯)) ≤ c) ↔
    ∀ (b : (a : ι) → a ∈ insert i s → κ a),
      (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
        f i (b i ⋯) ⊓
            s.attach.inf
              ((fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
                Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) ≤
          c

Tactic:
⟨fun h g hg =>
      h (g i <| mem_insert_self _ _) (fun j hj => g j <| mem_insert_of_mem hj)
        (hg _ <| mem_insert_self _ _) fun j hj => hg _ <| mem_insert_of_mem hj,
      fun h a g ha hg => ?_⟩

Premises used: Finset.mem_insert_self, Finset.mem_insert_of_mem, Iff.intro
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
insert :
  ∀
    (h :
      ∀ (b : (a : ι) → a ∈ Insert.insert i s → κ a),
        (∀ (a : ι) (h : a ∈ Insert.insert i s), b a h ∈ t a) →
          f i (b i ⋯) ⊓
              s.attach.inf
                ((fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
                  Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) ≤
            c)
    (a : κ i) (g : (a : ι) → a ∈ s → κ a) (ha : a ∈ t i) (hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a),
    (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c
⊢ (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
      a ∈ t i →
        (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (b (↑i : ι) ⋯)) ≤ c) ↔
    ∀ (b : (a : ι) → a ∈ Insert.insert i s → κ a),
      (∀ (a : ι) (h : a ∈ Insert.insert i s), b a h ∈ t a) →
        f i (b i ⋯) ⊓
            s.attach.inf
              ((fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
                Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) ≤
          c

Tactic:
refine
    ⟨fun h g hg =>
      h (g i <| mem_insert_self _ _) (fun j hj => g j <| mem_insert_of_mem hj)
        (hg _ <| mem_insert_self _ _) fun j hj => hg _ <| mem_insert_of_mem hj,
      fun h a g ha hg => ?_⟩
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ insert i s) (↑x : ι) ⋯) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
⊢ ∀ (j : ↥s), (↑j : ι) ≠ i

Tactic:
have aux : ∀ j : { x // x ∈ s }, ↑j ≠ i := fun j : s => ne_of_mem_of_not_mem j.2 hi
-- Module: Mathlib.Data.Finset.Lattice.Pi
Goal:
α : Type u_1
ι : Type u_2
inst : DistribLattice α
inst_1 : BoundedOrder α
inst_2 : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih :
  Eq.{u_1 + 1} (α := α) (s.inf fun (i : ι) ↦ (t i).sup (f i))
    ((s.pi (β := κ) t).sup fun (g : (a : ι) → a ∈ s → κ a) ↦ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯))
c : α
h :
  ∀ (b : (a : ι) → a ∈ Insert.insert i s → κ a),
    (∀ (a : ι) (h : a ∈ Insert.insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(Insert.insert i s)) ↦ f (↑i_1 : ι) (b (↑i_1 : ι) ⋯)) ∘ fun (x : ↥s) ↦
              Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) ≤
        c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), (↑j : ι) ≠ i
insert :
  ∀
    (this :
      f i ((fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) i ⋯) ⊓
          s.attach.inf
            ((fun (i_1 : ↥(Insert.insert i s)) ↦
                f (↑i_1 : ι)
                  ((fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j))
                    (↑i_1 : ι) ⋯)) ∘
              fun (x : ↥s) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ Insert.insert i s) (↑x : ι) ⋯) ≤
        c),
    (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c
insert₁ :
  ∀ (j : ι) (hj : j ∈ Insert.insert i s),
    (fun (j : ι) (hj : j ∈ Insert.insert i s) ↦ (if hji : j = i then cast ⋯ a else g j ⋯ : κ j)) j hj ∈ t j
⊢ (f i a ⊓ s.attach.inf fun (i : ↥s) ↦ f (↑i : ι) (g (↑i : ι) ⋯)) ≤ c

Tactic:
have := h (fun j hj => if hji : j = i then cast (congr_arg κ hji.symm) a
      else g _ <| mem_of_mem_insert_of_ne hj hji) (fun j hj => ?_)