mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)

pp: case refine_1.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s✝ ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s✝
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
s t : Finset β
hs : ¬∃ a, g a = s
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 s * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (s ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (s ∪ t)

Tactic:
·

Goal state after:
case refine_1.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case pos
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∈ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

pp: case neg
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
·

Goal state after:
case pos
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∈ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.toSubgraph ≤ ⊤.induce {v_1 | v_1 ∈ p.support}

Tactic:
convert! Subgraph.le_induce_top_verts
  exact p.verts_toSubgraph.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case neg
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s

Tactic:
·

Goal state after:
case neg
V : Type u_1
v : V
G : SimpleGraph V
s : Set V
hv : v ∈ s
w : V
hadj : w ∈ G.neighborSet v
hw : w ∉ s
⊢ G.Adj v w ∧ (v ∈ s ∧ w ∈ sᶜ ∨ v ∈ sᶜ ∧ w ∈ s) ∨ w ∈ s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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 : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ g b)

pp: case refine_1.inl.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
ht : ¬∃ b, g b = t
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)

Tactic:
·

Goal state after:
case refine_1.inl.inl
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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 : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
a b : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 (g b) ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ g b) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ g b)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
hi : 0 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (0 + 1))

pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))

Tactic:
·

Goal state after:
case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
hi : 0 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert 0) ((cons hxy i').getVert (0 + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))

Tactic:
·

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
hxy : G.Adj u✝ v✝
i' : G.Walk v✝ w✝
ih : ∀ {i : ℕ}, i < i'.length → i'.toSubgraph.Adj (i'.getVert i) (i'.getVert (i + 1))
n✝ : ℕ
hi : n✝ + 1 < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert (n✝ + 1)) ((cons hxy i').getVert (n✝ + 1 + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case pos
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∈ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

pp: case neg
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
·

Goal state after:
case pos
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∈ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case neg
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ

Tactic:
·

Goal state after:
case neg
V : Type u_1
w : V
G : SimpleGraph V
s : Set V
hw : w ∈ sᶜ
v : V
hadj : v ∈ G.neighborSet w
hv : v ∉ s
⊢ G.Adj w v ∧ (w ∈ s ∧ v ∈ sᶜ ∨ w ∈ sᶜ ∧ v ∈ s) ∨ v ∈ sᶜ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : 0 < w.length
⊢ w.length - 1 < w.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case left
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ p.bypass.toSubgraph.verts ⊆ p.toSubgraph.verts

pp: case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w

Tactic:
·

Goal state after:
case left
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ p.bypass.toSubgraph.verts ⊆ p.toSubgraph.verts
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w

Tactic:
·

Goal state after:
case right
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
inst✝ : DecidableEq V
⊢ ∀ ⦃v_1 w : V⦄, p.bypass.toSubgraph.Adj v_1 w → p.toSubgraph.Adj v_1 w
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inl.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
ht : ¬∃ b, g b = t
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)

Tactic:
·

Goal state after:
case refine_1.inl.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
ht : ¬∃ b, g b = t
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
h : s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(u, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)

pp: case refine_2
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
x✝ : s(u, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
a : W₁
b : W₂
z : (fun x ↦ s(Sum.inl x.1, Sum.inr x.2)) (a, b) = s(u, v)
⊢ s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet

Tactic:
·

Goal state after:
case refine_1
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
h : s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
⊢ s(u, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_2
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
x✝ : s(u, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
a : W₁
b : W₂
z : (fun x ↦ s(Sum.inl x.1, Sum.inr x.2)) (a, b) = s(u, v)
⊢ s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet

Tactic:
·

Goal state after:
case refine_2
W₁ : Type u_2
W₂ : Type u_3
u v : W₁ ⊕ W₂
x✝ : s(u, v) ∈ Set.range fun x ↦ s(Sum.inl x.1, Sum.inr x.2)
a : W₁
b : W₂
z : (fun x ↦ s(Sum.inl x.1, Sum.inr x.2)) (a, b) = s(u, v)
⊢ s(u, v) ∈ (completeBipartiteGraph W₁ W₂).edgeSet
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case refine_1.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s✝ ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s✝
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
s t : Finset β
hs : ¬∃ a, g a = s
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 s * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (s ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (s ∪ t)

Tactic:
·

Goal state after:
case refine_1.inr
α : Type u_1
β✝ : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β✝
inst✝³ : LinearOrder β✝
inst✝² : IsStrictOrderedRing β✝
inst✝¹ : ExistsAddOfLE β✝
f₁ f₂ f₃ f₄ : α → β✝
inst✝ : 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✝ : Finset α
L : Sublattice α := { carrier := latticeClosure (↑s✝ ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s✝
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
s t : Finset β
hs : ¬∃ a, g a = s
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 s * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (s ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : 0 ≤ 0
hfg : ∑ a, 0 a = ∑ a, g a
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
⊢ ∑ a, μ a * 0 a ≤ ∑ a, μ a * g a

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hg : 0 ≤ g
hμ : Monotone μ
hf : 0 ≤ 0
hfg : ∑ a, 0 a = ∑ a, g a
h : ∀ (a b : α), 0 a * g b ≤ 0 (a ⊓ b) * g (a ⊔ b)
⊢ ∑ a, μ a * 0 a ≤ ∑ a, μ a * g a
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
⊢ i - 1 < p.length

Tactic:
by lia

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
hfg : ∑ a, f a = ∑ a, 0 a
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * 0 a

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hμ : Monotone μ
hf : 0 < f
hg : 0 ≤ 0
hfg : ∑ a, f a = ∑ a, 0 a
h : ∀ (a b : α), f a * 0 b ≤ f (a ⊓ b) * 0 (a ⊔ b)
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * 0 a
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ G.Adj u v

pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.edist u v = 1

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 1
⊢ G.Adj u v
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.edist u v = 1

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ G.edist u v = 1
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
huv : u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

Tactic:
·

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
huv : u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v

Tactic:
·

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : ¬u = v
⊢ G.edist u v ≤ 1 ↔ G.Adj u v ∨ u = v
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ u ≠ v

pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ ¬G.Adj u v

pp: case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty

pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ G.edist u v ≤ 2

pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
·

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ u ≠ v
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ ¬G.Adj u v

pp: case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty

pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ G.edist u v ≤ 2

pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
·

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ ¬G.Adj u v
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
this : (∑ a, g a) * ∑ a, (μ * f) a ≤ (∑ a ∈ univ ⊼ univ, f a) * ∑ a ∈ univ ⊻ univ, (μ * g) a
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a

pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
a b : α
⊢ g a * (μ * f) b ≤ f (a ⊓ b) * (μ * g) (a ⊔ b)

Tactic:
·

Goal state after:
case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f g μ : α → β
inst✝ : Fintype α
hμ₀ : 0 ≤ μ
hf✝ : 0 ≤ f
hg✝ : 0 ≤ g
hμ : Monotone μ
hfg : ∑ a, f a = ∑ a, g a
h : ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b)
hf : 0 < f
hg : 0 < g
this : (∑ a, g a) * ∑ a, (μ * f) a ≤ (∑ a ∈ univ ⊼ univ, f a) * ∑ a ∈ univ ⊻ univ, (μ * g) a
⊢ ∑ a, μ a * f a ≤ ∑ a, μ a * g a
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty

pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ G.edist u v ≤ 2

pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
·

Goal state after:
case refine_3
V : Type u_1
G : SimpleGraph V
u v : V
h : G.edist u v = 2
⊢ (G.commonNeighbors u v).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ G.edist u v ≤ 2

pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
·

Goal state after:
case refine_4
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ G.edist u v ≤ 2
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v

Tactic:
·

Goal state after:
case refine_5
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ (G.commonNeighbors u v).Nonempty
⊢ 2 ≤ G.edist u v