-- Module: Mathlib.Combinatorics.SetFamily.FourFunctions
Goal:
α : Type u_1
β_1 : Type u_2
inst : DistribLattice α
inst_1 : CommSemiring β_1
inst_2 : LinearOrder β_1
inst_3 : IsStrictOrderedRing β_1
inst_4 : ExistsAddOfLE β_1
f₁ f₂ f₃ f₄ : α → β_1
inst_5 : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t_1 : Finset α
L : Sublattice α :=
  { carrier := (latticeClosure : (a : Set α) → Set α) ((↑s : Set α) ∪ (↑t_1 : Set α)), supClosed' := ⋯,
    infClosed' := ⋯ }
this : Finite.{u_1 + 1} ↥L
s' t' : Finset ↥L
hs' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } s' = s
ht' : map { toFun := (⇑L.subtype : (a : ↥L) → α), inj' := ⋯ : ↥L ↪ α } t' = t_1
β : Type u_1
w : DecidableEq β
w_1 : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective (α := ↥L) (β := Finset β) (⇑g : (a : ↥L) → Finset β)
t : Finset β
a : ↥L
refine_1 :
  ∀ (b : ↥L),
    extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1) ((g : (a : ↥L) → Finset β) a : Finset β) *
        extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1) ((g : (a : ↥L) → Finset β) b : Finset β) ≤
      extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1)
          ((g : (a : ↥L) → Finset β) a ∩ (g : (a : ↥L) → Finset β) b : Finset β) *
        extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1)
          ((g : (a : ↥L) → Finset β) a ∪ (g : (a : ↥L) → Finset β) b : Finset β)
refine_1₁ :
  ∀ (ht : ¬∃ (b : ↥L), (g : (a : ↥L) → Finset β) b = t),
    extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1) ((g : (a : ↥L) → Finset β) a : Finset β) *
        extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 t ≤
      extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1)
          ((g : (a : ↥L) → Finset β) a ∩ t : Finset β) *
        extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
          (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1)
          ((g : (a : ↥L) → Finset β) a ∪ t : Finset β)
⊢ extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
        (f₁ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1) ((g : (a : ↥L) → Finset β) a : Finset β) *
      extend (α := ↥L) (⇑g : (a : ↥L) → Finset β) (f₂ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) 0 t ≤
    extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
        (f₃ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1)
        ((g : (a : ↥L) → Finset β) a ∩ t : Finset β) *
      extend (α := ↥L) (β := Finset β) ((⇑g : (a : ↥L) → Finset β) : (a : ↥L) → Finset β)
        (f₄ ∘ Subtype.val (p := fun (x : α) ↦ x ∈ L)) (0 : Finset β → β_1) ((g : (a : ↥L) → Finset β) a ∪ t : Finset β)

Tactic:
obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)

Premises used: Exists, em, Eq, DFunLike.coe, rfl