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

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ t ∈ ∂⁺ ^[k + 1] 𝒜 ↔ ∃ u, #u = k + 1 ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ,
      subset_erase, erase_sdiff_comm, ← sdiff_insert]
    constructor
    · rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩
      exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩
    · rintro ⟨_, ⟨a, u, hau, rfl, rfl⟩, hut, htu⟩
      rw [insert_subset_iff] at hut
      exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (2 ^ #s * #(𝒜 ∩ ℬ))

Tactic:
have h₁ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.memberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_memberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
h₀ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.nonMemberSubfamily a 𝒞, t ⊆ s
h₁ : ∀ (𝒞 : Finset (Finset α)), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ Finset.memberSubfamily a 𝒞, t ⊆ s
⊢ 2 *
      (#(Finset.memberSubfamily a 𝒜) * #(Finset.memberSubfamily a ℬ) +
        #(Finset.nonMemberSubfamily a 𝒜) * #(Finset.nonMemberSubfamily a ℬ)) ≤
    2 * (2 ^ #s * #(𝒜 ∩ ℬ))
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:

Tactic:
(a₀ * b₁ + a₁ * b₀) * (c₀ * d₁)
      = a₀ * b₁ * (c₀ * d₁) + c₀ * d₁ * (a₁ * b₀) := by ring
    _ ≤ a₀ * b₁ * (a₁ * b₀) + c₀ * d₁ * (c₀ * d₁) := mul_add_mul_le_mul_add_mul h₀₁ h₁₀
    _ = a₀ * b₀ * (a₁ * b₁) + c₀ * d₁ * (c₀ * d₁) := by ring
    _ ≤ c₀ * d₀ * (c₁ * d₁) + c₀ * d₁ * (c₀ * d₁) := by gcongr
    _ = (c₀ * d₁ + c₁ * d₀) * (c₀ * d₁) := by ring

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset ι
f : ι → Finset (Finset α)
hf : ∀ i ∈ s, (↑(f i)).Intersecting
⊢ #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)

Tactic:
have : DecidableEq ι := by
    classical
    infer_instance
  obtain hs | hs := le_total (Fintype.card α) #s
  · rw [tsub_eq_zero_of_le hs, pow_zero]
    refine (card_le_card <| biUnion_subset.2 fun i hi a ha ↦
      mem_compl.2 <| notMem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq ?_
    rw [card_compl, Fintype.card_finset, card_singleton]
  induction s using Finset.cons_induction generalizing f with
  | empty => simp
  | cons i s hi ih =>
  set f' : ι → Finset (Finset α) :=
    fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
  have hf₁ : ∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * #(f' j) =
      2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting := by
    rintro j hj
    simp_rw [f', dif_pos hj, ← Fintype.card_finset]
    exact Classical.choose_spec (hf j hj).exists_card_eq
  have hf₂ : ∀ j, j ∈ cons i s hi → IsUpperSet (f' j : Set (Finset α)) := by
    refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)
    rw [Fintype.card_finset]
    exact (hf₁ _ hj).2.1
  refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
  nth_rw 1 [cons_eq_insert i]
  rw [biUnion_insert]
  refine (card_mono <| @le_sup_sdiff _ _ (f' i) _).trans ((card_union_le _ _).trans ?_)
  rw [union_sdiff_left, sdiff_eq_inter_compl]
  refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
  rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
  refine (add_le_add
      ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2
      (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
      (mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans ?_
  · rw [coe_biUnion]
    exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
  · rw [coe_compl]
    exact (hf₂ _ <| mem_cons_self _ _).compl
  rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub,
    (hf₁ _ <| mem_cons_self _ _).2.1, two_mul, add_tsub_cancel_left, ← mul_tsub, ← mul_two,
    mul_assoc, ← add_mul, mul_comm]
  gcongr
  refine (add_le_add_right
    (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2)
    ((card_le_card <| subset_cons _).trans hs)) _).trans ?_
  rw [mul_tsub, two_mul, ← pow_succ',
    ← add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self),
    tsub_add_eq_add_tsub hs, card_cons, add_tsub_add_eq_tsub_right]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
u : Finset α
hu : u ⊆ t
⊢ ∃ u_1 ∈ 𝒜, t ∩ u_1 = u

Tactic:
obtain ⟨v, hv, rfl⟩ := hs (hu.trans h); exact ⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : 𝒜.Shatters s
⊢ (∃ u ∈ 𝒜, s ∩ u = t) → t ⊆ s

Tactic:
rintro ⟨u, _, rfl⟩; exact inter_subset_left

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex (compress (A \ B) (B \ A) B)
sizeA : #B = r
hB : B ∉ ℬ
hAB : compress (A \ B) (B \ A) B ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
hlt : (A \ B).max' hU < (B \ A).max' hV
⊢ (B \ A).max' hV < (A \ B).max' hU

Tactic:
cases hBA.not_gt <| toColex_compress_lt_toColex hlt hAB

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

Goal state before:
pp: case left
α : 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
q_a q_b : Quotient r
h_eq : Quot.lift f f_respects_relation q_a = Quot.lift f f_respects_relation q_b
⊢ q_a = q_b

Tactic:
induction q_a using Quotient.ind with

Goal state after:
case left.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
q_b : Quotient r
a : α
h_eq : Quot.lift f f_respects_relation ⟦a⟧ = Quot.lift f f_respects_relation q_b
⊢ ⟦a⟧ = q_b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
huv : u ≠ v
h : G.Reachable u v
p : G.Walk u v := Classical.choice h
hp : ¬p.Nil
⊢ u ∈ G.support

Tactic:
exact mem_support_of_mem_walk_support p hp p.start_mem_support

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
x✝ : hs.Quotient
x : α
⊢ hs.proj ⁻¹' {Quotient.mk'' x} = s (hs.equivQuotient.symm (Quotient.mk'' x))

Tactic:
ext y
    simp only [Set.mem_preimage, hs.mem_iff_index_eq]
    exact Quotient.eq''

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

Goal state before:
pp: n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
this✝² : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ)
this✝¹ : r ≤ n
this✝ : 1 ≤ n
z : (n - 1).choose (n - r) < #𝒜ᶜˢ
h𝒜bar : Set.Sized (n - r) ↑𝒜ᶜˢ
kk : (n - 1).choose r ≤ #(∂^[n - 2 * r] 𝒜ᶜˢ)
this : n - r - (n - 2 * r) = r
⊢ n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r

Tactic:
convert! Nat.choose_succ_succ _ _ using 3 <;> rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ↑(card α) ≤ G.chromaticNumber
C : G.Coloring α
⊢ Surjective ⇑C

Tactic:
C.colorable.chromaticNumber_eq_sInf,

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
h : ↑(card α) ≤ ↑(sInf {n' | G.Colorable n'})
C : G.Coloring α
⊢ Surjective ⇑C
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case neg
α : 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 ∉ 𝒜
⊢ (0 + 0) * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
· simp_rw [add_zero, zero_mul]
    exact mul_nonneg (collapse_nonneg h₃ _) <| collapse_nonneg h₄ _

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

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hw : w ∈ t
⊢ G.neighborSet w ⊆ s

Tactic:
rw [isBipartiteWith_neighborSet' h hw]
  exact Set.sep_subset s (G.Adj · w)

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk✝ : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < ↑k
⊢ s.encard + {e}.encard < ↑(k + 1)

Tactic:
Set.encard_singleton

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
hk✝ : k ≠ 0
h : G.IsEdgeReachable (k + 1) u v
e : Sym2 V
s : Set (Sym2 V)
hk : s.encard < ↑k
⊢ s.encard + 1 < ↑(k + 1)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
⊢ ∀ x ∈ s ∪ t, x ∉ G.support.toFinset → G.degree x = 0

Tactic:
intro v _ hv

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : G.IsBipartiteWith ↑s ↑t
hsub : G.support.toFinset ⊆ s ∪ t
v : V
a✝ : v ∈ s ∪ t
hv : v ∉ G.support.toFinset
⊢ G.degree v = 0
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.IsBipartite
⊢ ∃ s t, G.IsBipartiteWith s t

Tactic:
obtain ⟨c, hc⟩ := h
  refine ⟨{v | c v = 0}, {v | c v = 1}, by aesop (add simp [Set.disjoint_left]), ?_⟩
  rintro v w hvw
  apply hc at hvw
  simp [Set.mem_ofPred_eq] at hvw ⊢
  lia

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

Goal state before:
pp: case cons
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))
i : ℕ
hi : i < (cons hxy i').length
⊢ (cons hxy i').toSubgraph.Adj ((cons hxy i').getVert i) ((cons hxy i').getVert (i + 1))

Tactic:
cases i
    · simp
    · simp only [Walk.toSubgraph, getVert_cons_succ, Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq,
        Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]
      right
      exact ih (Nat.succ_lt_succ_iff.mp hi)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
k : ℕ
h : G.edist u v = ↑k
⊢ G.edist u v ≠ ⊤

Tactic:
by rw [h]; exact ENat.natCast_ne_top _

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
completeBipartiteGraph_isContained_iff

Goal state after:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝³ : Finite α
inst✝² : Finite β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
this✝ : Fintype α
this : Fintype β
⊢ (∃ left right,
      #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right) ↔
    ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ G.edist u v

Tactic:
← hw,

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : ↑w✝.length = G.edist u v
⊢ G'.edist u v ≤ ↑w✝.length
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ #s * #t ≤ #(s \\ t) * #(t \\ s)

Tactic:
by
  have : ∀ s t : Finset α, (s \\ t).map ⟨_, liftLatticeHom_injective⟩ =
      s.map ⟨_, liftLatticeHom_injective⟩ \\ t.map ⟨_, liftLatticeHom_injective⟩ := by
    rintro s t
    simp_rw [map_eq_image]
    exact image_image₂_distrib fun a b ↦ rfl
  simpa [← card_compls (_ ⊻ _), ← map_sup, ← map_inf, ← this] using
    (s.map ⟨_, liftLatticeHom_injective⟩).le_card_infs_mul_card_sups
      (t.map ⟨_, liftLatticeHom_injective⟩)ᶜˢ

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ G.dist u v

Tactic:
← hw,

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
G' : SimpleGraph V
h : G ≤ G'
hr : G.Reachable u v
w✝ : G.Walk u v
hw : w✝.length = G.dist u v
⊢ G'.dist u v ≤ w✝.length
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
H.connected_iff,

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected ∧ H.verts.Nonempty ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: case neg.refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : ↑w.length = (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ (G □ H).edist x y

Tactic:
← hw,

Goal state after:
case neg.refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G □ H).edist x y = ⊤
rGH : G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤
wG : G.Walk x.1 y.1
hwG : ↑wG.length = G.edist x.1 y.1
wH : H.Walk x.2 y.2
hwH : ↑wH.length = H.edist x.2 y.2
w_app : (G □ H).Walk (x.1, x.2) (y.1, y.2) := (Walk.boxProdLeft H x.2 wG).append (Walk.boxProdRight G y.1 wH)
w_len : w_app.length = wG.length + wH.length
w : (G □ H).Walk x y
hw : ↑w.length = (G □ H).edist x y
⊢ G.edist x.1 y.1 + H.edist x.2 y.2 ≤ ↑w.length
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free (SimpleGraph.map (⇑e) G)

Tactic:
← free_congr .refl (.map e G)

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
G : SimpleGraph (Fin n)
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free (SimpleGraph.map (⇑e) G)

Tactic:
← free_congr .refl (.map e G)

Goal state after:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst✝ : Fintype V
hc : Fintype.card V = n
e : V ≃ Fin n := Fintype.equivFinOfCardEq hc
G : SimpleGraph V
h : G ∈ {G | H.Free G}
⊢ SimpleGraph.map (⇑e) G ∈ univ ∧ H.Free G
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: n : ℕ
h : Even n
⊢ ∀ {v w : Fin n}, (cycleGraph n).Adj v w → decide (↑v % 2 = 0) ≠ decide (↑w % 2 = 0)

Tactic:
intro u v hadj
    match n with
    | 0 => exact u.elim0
    | 1 => simp at h
    | n + 2 =>
      simp only [ne_eq, decide_eq_decide]
      simp only [cycleGraph_adj] at hadj
      cases hadj with
      | inl huv | inr huv =>
        rw [← add_eq_of_eq_sub' huv.symm, ← Fin.even_iff_mod_of_even h,
          ← Fin.even_iff_mod_of_even h, Fin.even_add_one_iff_odd]
        apply Classical.not_iff.mpr
        simp [Fin.not_odd_iff_even_of_even h, Fin.not_even_iff_odd_of_even h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).edgeFinset.card + 1 < Nat.card V

Tactic:
← h₂,

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).edgeFinset.card + 1 < Nat.card ↑G.edgeSet + 1
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
⊢ (∃ n, (G.finsetWalkLength (↑n) u v).Nonempty) → G.Reachable u v

Tactic:
rintro ⟨_, p, _⟩
    exact ⟨p⟩

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
h : G.IsAcyclic
n : ℕ
hn : n ≥ 3
hle : cycleGraph n ⊑ G
⊢ False

pp: case refine_2
V : Type u_1
G : SimpleGraph V
h : ∀ n ≥ 3, (cycleGraph n).Free G
v : V
p : G.Walk v v
hcyc : p.IsCycle
⊢ cycleGraph p.length ⊑ G

Tactic:
· have ⟨v, p, hcyc, hlen⟩ := cycleGraph_isContained_iff hn |>.mp hle
    exact h p hcyc

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
h : ∀ n ≥ 3, (cycleGraph n).Free G
v : V
p : G.Walk v v
hcyc : p.IsCycle
⊢ cycleGraph p.length ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
ediam_eq : G.ediam = e
⊢ G.radius = e

Tactic:
exact le_antisymm ((h Classical.ofNonempty) ▸ radius_le_eccent) (le_iInf fun u ↦ (h u).ge)

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

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
x✝¹ x✝ : V
w✝³ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝³
w✝² : Fin r
h₂ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝²
w✝¹ : Fin t
h₁' : f (w✝³, w✝¹) = x✝¹
w✝ : Fin t
h₂' : f (w✝², w✝) = x✝
heq : w✝³ = w✝²
⊢ map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝²

Tactic:
← h₂,

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
x✝¹ x✝ : V
w✝³ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = x✝³
w✝² : Fin r
h₂ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝²
w✝¹ : Fin t
h₁' : f (w✝³, w✝¹) = x✝¹
w✝ : Fin t
h₂' : f (w✝², w✝) = x✝
heq : w✝³ = w✝²
⊢ map { toFun := fun j ↦ f (w✝³, j), inj' := ⋯ } univ = map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
⊢ G.CompleteEquipartiteSubgraph r t

Tactic:
by_cases ht : t = 0
  · exact ⟨∅, .inr ht, by simp, by simp⟩
  · refine ⟨univ.map ⟨fun i ↦ univ.map ⟨fun j ↦ f (i, j), fun _ _ h ↦ ?_⟩, fun i₁ i₂ h ↦ ?_⟩,
      ?_, fun h ↦ ?_, fun _ h₁ _ h₂ hne _ h₁' _ h₂' ↦ ?_⟩
    · simpa using f.injective h
    · simp_rw [Finset.ext_iff] at h
      have : NeZero t := ⟨ht⟩
      obtain ⟨_, heq⟩ : ∃ j, f (i₁, j) = f (i₂, 0) := by simpa using h <| f (i₂, 0)
      apply f.injective at heq
      rw [Prod.mk.injEq] at heq
      exact heq.left
    · simp
    · simp_rw [mem_map, mem_univ, Embedding.coeFn_mk, true_and] at h
      replace ⟨_, h⟩ := h
      simp [← h]
    · simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁ h₂
      replace ⟨_, h₁⟩ := h₁
      replace ⟨_, h₂⟩ := h₂
      rw [← h₁] at h₁'
      rw [← h₂] at h₂'
      simp_rw [coe_map, Embedding.coeFn_mk, coe_univ, Set.image_univ, Set.mem_range] at h₁' h₂'
      replace ⟨_, h₁'⟩ := h₁'
      replace ⟨_, h₂'⟩ := h₂'
      rw [← h₁', ← h₂']
      apply f.toHom.map_adj
      simp_rw [completeEquipartiteGraph_adj]
      contrapose hne with heq
      simp_rw [← h₁, ← h₂, heq]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ #parts = r ∨ t = 0

Tactic:
hparts_card,

Goal state after:
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : Nonempty (G.CompleteEquipartiteSubgraph (r + 1) t)
K' : G.CompleteEquipartiteSubgraph (r + 1) t
parts : Finset (Finset V)
hparts_sub : parts ⊆ K'.parts
hparts_card : #parts = (#K'.parts).pred
⊢ (#K'.parts).pred = r ∨ t = 0