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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₁ s * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∈ 𝒜
h✝² : insert a s ∉ 𝒜
h✝¹ : t ∉ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₁ s * f₂ (insert a t) ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
]

Goal state after:
case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
U V : Finset (Fin n)
hUV : (U, V) ∈ univ ∧ UsefulCompression (U, V).1 (U, V).2 ∧ ¬IsCompressed (U, V).1 (U, V).2 𝒜
t : ∀ x' ∈ usable, #(U, V).1 ≤ #x'.1
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
s : Set (Sym2 V)
⊢ Relation.TransGen (Relation.ReflGen (fromEdgeSet s).Adj) = Relation.TransGen (Relation.ReflGen (Sym2.ToRel s))

Tactic:
]

Goal state after:
V : Type u
s : Set (Sym2 V)
⊢ Relation.TransGen (Relation.ReflGen (fromEdgeSet s).Adj) = Relation.TransGen (Relation.ReflGen (Sym2.ToRel s))
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
u : V
v : V'
⊢ G'.Reachable v (φ u) ↔ G'.Reachable v (φ u)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ a ∈ {x | r x a}

Tactic:
]

Goal state after:
case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ a ∈ {x | r x a}
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        _x →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.tail.length + 1

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        _x →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.tail.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
u v : V
⊢ G.Reachable v v

Tactic:
]

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case right
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Surjective f

Tactic:
]

Goal state after:
case right
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Surjective f
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : Fintype ↑(G.neighborSet v)
huv : u ≠ v
hu : G.degree v = 0
⊢ ¬G.Reachable v u

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : Fintype ↑(G.neighborSet v)
huv : u ≠ v
hu : G.degree v = 0
⊢ ¬G.Reachable v u
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
x y : V
h : x = y
⊢ ⊤.Reachable y y

Tactic:
]

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

Goal state before:
pp: V : Type u
inst✝² : Nontrivial V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
⊢ 0 < G.degree v

Tactic:
]

Goal state after:
V : Type u
inst✝² : Nontrivial V
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.Preconnected
v : V
hv : G.minDegree = G.degree v
⊢ 0 < G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ v, ∀ (w : V), G.Reachable v w

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ v, ∀ (w : V), G.Reachable v w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
inst✝ : Nonempty V
⊢ Nonempty V

Tactic:
]

Goal state after:
V : Type u
inst✝ : Nonempty V
⊢ Nonempty V
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ (¬∃ v, ∀ (w : V), G.Reachable v w) → Gᶜ.Preconnected

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
⊢ (¬∃ v, ∀ (w : V), G.Reachable v w) → Gᶜ.Preconnected
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
⊢ G.Reachable w w

Tactic:
]

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
m : ℕ
⊢ m < k → m < n

Tactic:
]

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
m : ℕ
⊢ m < k → m < n
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right✝ : ∀ (y_1 : Set α), (fun b ↦ b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
⊢ b ∈ c

Tactic:
]

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right✝ : ∀ (y_1 : Set α), (fun b ↦ b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
⊢ b ∈ c
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ((f₁ (insert a s) * if t ∈ ℬ then f₂ t else 0) + f₁ (insert a s) * if insert a t ∈ ℬ then f₂ (insert a t) else 0) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ ((f₁ (insert a s) * if t ∈ ℬ then f₂ t else 0) + f₁ (insert a s) * if insert a t ∈ ℬ then f₂ (insert a t) else 0) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑(H.coe.connectedComponentMk w✝) ∧ ↑⟨w, hw⟩ = w

Tactic:
]

Goal state after:
case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑(H.coe.connectedComponentMk w✝) ∧ ↑⟨w, hw⟩ = w
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
x y : Partitions α
hx : x ≤ y
hy : y ≤ x
h : mkClasses x.toSet ⋯ = mkClasses y.toSet ⋯ := le_antisymm hx hy
⊢ (mkClasses y.toSet ⋯).classes = (mkClasses y.toSet ⋯).classes

Tactic:
]

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ k.choose (r - i) = k.choose (r - i)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
C : Partitions α
⊢ Partitions.toSet ((fun r ↦ ⟨r.classes, ⋯⟩) ((fun C ↦ mkClasses ↑C ⋯) C)) = (mkClasses C.toSet ⋯).classes

Tactic:
]

Goal state after:
α : Type u_1
C : Partitions α
⊢ Partitions.toSet ((fun r ↦ ⟨r.classes, ⋯⟩) ((fun C ↦ mkClasses ↑C ⋯) C)) = (mkClasses C.toSet ⋯).classes
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : G.connectedComponentMk v = c
hc' : G.connectedComponentMk v = c'
⊢ G.connectedComponentMk v = G.connectedComponentMk v

Tactic:
]

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = c'

Tactic:
]

Goal state after:
V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
v' : V
hv' : G.Reachable v' v
⊢ G'.connectedComponentMk v = c'
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
]

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ #B = r - i ↔ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ r ≤ k

Tactic:
]

Goal state after:
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
⊢ r ≤ k
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : G.connectedComponentMk u = C
hv : G.connectedComponentMk v = C
⊢ G.Reachable u v

Tactic:
]

Goal state after:
V : Type u
G : SimpleGraph V
C : G.ConnectedComponent
u v : V
hu : G.connectedComponentMk u = C
hv : G.connectedComponentMk v = C
⊢ G.Reachable u v
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
i : ι
x : α
hx : x ∈ s i
⊢ f i x = f i x

Tactic:
]

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

Goal state before:
pp: case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
]

Goal state after:
case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ i, s i)
⊢ BijOn g (⋃ i, s i) (⋃ i, t i)

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : ι → Set β
ht : IndexedPartition t
hf : ∀ (i : ι), BijOn (f i) (s i) (t i)
g : α → β := hs.piecewise f
hg : g = hs.piecewise f
hg_bij : ∀ (i : ι), BijOn g (s i) (t i)
hg_inj : InjOn g (⋃ i, s i)
⊢ BijOn g (⋃ i, s i) (⋃ i, t i)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ #(s \ B) = i

Tactic:
refine ⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩

Goal state after:
case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ #(C \ B) = i
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ f (hs.index x) ⁻¹' t
⊢ x ∈ ⋃ i, s i ∩ f i ⁻¹' t

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
hx : x ∈ f (hs.index x) ⁻¹' t
⊢ x ∈ ⋃ i, s i ∩ f i ⁻¹' t
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
x✝ : x ∈ ⋃ i, s i ∩ f i ⁻¹' t
a : Set α
i : ι
hi : (fun i ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ (fun i ↦ s i ∩ f i ⁻¹' t) (hs.index x)
⊢ x ∈ hs.piecewise f ⁻¹' t

Tactic:
]

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
x✝ : x ∈ ⋃ i, s i ∩ f i ⁻¹' t
a : Set α
i : ι
hi : (fun i ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ (fun i ↦ s i ∩ f i ⁻¹' t) (hs.index x)
⊢ x ∈ hs.piecewise f ⁻¹' t
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ i = i

Tactic:
]

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

Goal state before:
pp: case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i

Tactic:
]

Goal state after:
case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ B ⊆ range'k ∧ #B = r - i
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mpr
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ #A = r
hBA : B ⊆ A
card_sdiff_i : #(A \ B) = i
⊢ #A = #A

Tactic:
]

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

Goal state before:
pp: case e'_1
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ ((G.connectedComponentMk b✝).toSimpleGraph →g H) = ((G.connectedComponentMk b✝).toSimpleGraph.Adj →r H.Adj)

Tactic:
]

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

Goal state before:
pp: case e'_2
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
H : SimpleGraph V'
C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H
a✝ b✝ : V
hab : G.Adj a✝ b✝
h : (G.connectedComponentMk a✝).toSimpleGraph.Adj ⟨a✝, ⋯⟩ ⟨b✝, ⋯⟩
⊢ (fun x ↦ x ∈ G.connectedComponentMk b✝) = fun x ↦ x ∈ G.connectedComponentMk b✝

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∉ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∉ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * f₄ (insert a s ∪ insert a t) ≤
    (f₃ (s ∩ t) + f₃ (insert a (s ∩ t))) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)