mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: ⊢ Nat.cast =O[atTop] fun n ↦ ↑n / 3

Tactic:
simp_rw [div_eq_inv_mul]

Goal state after:
⊢ Nat.cast =O[atTop] fun n ↦ 3⁻¹ * ↑n
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
⊢ E(G.deleteVerts X) = {e | ∃ x y, G.IsLink e x y ∧ x ∉ X ∧ y ∉ X}

Tactic:
by
  simp [edgeSet_eq_setOfPred_exists_isLink]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D

Tactic:
rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (n + 1) a) ⊆ FP a

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f✝ : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : ↥s
⊢ ↑(↑f ↑x) < Fintype.card ↥s

Tactic:
by simp [← mem_prefixed.1 f.2 x]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
induction s using Finset.eraseInduction with | H s ih => _

Goal state after:
case H
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
⊢ ∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X C

Tactic:
rw [← contract_inter_ground_eq, contract_spanning_iff, and_congr_right_iff]

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
⊢ M.Spanning (X ∪ C ∩ M.E) → (Disjoint X (C ∩ M.E) ↔ Disjoint X C)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hC : M.IsCircuit C
hK : K.Nonempty
hKC : K ⊆ C
⊢ C \ K ⊂ C

Tactic:
rwa [sdiff_ssubset_left_iff, inter_eq_self_of_subset_right hKC]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: α : Type u
β : Type v
M : Matroid α
N : Matroid β
I X : Set (α ⊕ β)
⊢ (M.sum N).IsBasis I X ↔ M.IsBasis (Sum.inl ⁻¹' I) (Sum.inl ⁻¹' X) ∧ N.IsBasis (Sum.inr ⁻¹' I) (Sum.inr ⁻¹' X)

Tactic:
simp only [Matroid.sum, mapEquiv_isBasis_iff, Equiv.sumCongr_symm,
    Equiv.sumCongr_apply, Equiv.symm_symm, sigma_isBasis_iff, Bool.forall_bool,
    Equiv.sumEquivSigmaBool, Equiv.coe_fn_mk, Equiv.ulift]
  convert! Iff.rfl <;> exact ext <| by simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case succ
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
n : ℕ
ih : ∀ (b : V), height b < n → Nonempty (Path r b)
b : V
hn : height b < n + 1
⊢ Nonempty (Path r b)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
w : V
⊢ w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))

Tactic:
hw_ne

Goal state after:
case mp
V : Type u_2
inst✝ : Quiver V
v : V
h_singleton : ∀ (w : V), StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v → w = v
w : V
hw_ne : w ≠ v
⊢ ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : φ.IsCovering
hφψ : (φ ⋙q ψ).IsCovering
φsur : Surjective φ.obj
⊢ ψ.IsCovering

Tactic:
by
  refine ⟨fun v => ?_, fun v => ?_⟩ <;> obtain ⟨u, rfl⟩ := φsur v
  exacts [(Bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u),
    (Bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: case pos
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
p'_len : p'.length = n
u : V
hu_not_S : ¬u ∈ S
v : V
hv_S : v ∈ S
e_uv : u ⟶ v
p₁ : Path a u
p₂ : Path v c
hp' : p' = p₁.comp (e_uv.toPath.comp p₂)
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e_1 p₁ p₂, p'.cons e = p₁.comp (e_1.toPath.comp p₂)

Tactic:
refine ⟨u, hu_not_S, v, hv_S, e_uv, p₁, p₂.comp e.toPath, ?_⟩

Goal state after:
case pos
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
c : V
p' : Path a c
e : c ⟶ b
h_len : (p'.cons e).length = n + 1
h_pos : 0 < (p'.cons e).length
hc_in_S : c ∈ S
p'_len : p'.length = n
u : V
hu_not_S : ¬u ∈ S
v : V
hv_S : v ∈ S
e_uv : u ⟶ v
p₁ : Path a u
p₂ : Path v c
hp' : p' = p₁.comp (e_uv.toPath.comp p₂)
⊢ p'.cons e = p₁.comp (e_uv.toPath.comp (p₂.comp e.toPath))
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: case succ
V : Type u_1
inst✝ : Quiver V
n : ℕ
ih :
  ∀ {a b : V} (p : Path a b) (S : Set V),
    ¬a ∈ S → b ∈ S → p.length = n → ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)
a b : V
p : Path a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = n + 1
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case nil
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v : V
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨φ.obj u, Path.nil⟩

Tactic:
use ⟨u, Path.nil⟩
    simp only [Prefunctor.mapPath_nil]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
p : α → Prop
h : ∀ a ∈ s, ∀ b ∈ t, Disjoint a b → p (a ⊔ b)
a : α
ha : a ∈ s
b : α
hb : b ∈ t
hab : Disjoint a b
⊢ p (a ⊔ b)

Tactic:
exact h _ ha _ hb hab

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ⊆ s
⊢ s ∈ ↑(Finset.nonMemberSubfamily a 𝒜) → t ∈ ↑(Finset.nonMemberSubfamily a 𝒜)

Tactic:
simp_rw [mem_coe, mem_nonMemberSubfamily]
  exact And.imp (h hts) (mt <| @hts _)

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 A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ 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:
← compress_sdiff_sdiff A B

Goal state after:
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
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_3.refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
hℬ : #ℬ = #((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ ℬ ⊆ 𝒜.shatterer

Tactic:
· refine forall_mem_image.2 fun s hs ↦ mem_shatterer.2 fun t ht ↦ ?_
    simp only [mem_inter, mem_shatterer] at hs
    rw [subset_insert_iff] at ht
    by_cases ha : a ∈ t
    · obtain ⟨u, hu, hsu⟩ := hs.1 ht
      rw [mem_memberSubfamily] at hu
      refine ⟨_, hu.1, ?_⟩
      rw [← insert_inter_distrib, hsu, insert_erase ha]
    · obtain ⟨u, hu, hsu⟩ := hs.2 ht
      rw [mem_nonMemberSubfamily] at hu
      refine ⟨_, hu.1, ?_⟩
      rwa [insert_inter_of_notMem hu.2, hsu, erase_eq_self]

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ a ∈ ⋃₀ c

Tactic:
hu

Goal state after:
α : Type u_1
c : Set (Set α)
hu : ⋃₀ c = Set.univ
H : c.PairwiseDisjoint id
a : α
⊢ a ∈ Set.univ
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ #𝒜 = 0

Tactic:
rw [Finset.card_eq_zero, eq_empty_iff_forall_notMem]

Goal state after:
case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

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

Tactic:
simp only [chromaticNumber, Set.mem_ofPred_eq, le_iInf_iff, Nat.cast_le]
    rintro i ⟨C⟩
    contrapose! h
    refine ⟨G.recolorOfCardLE (by simpa using h.le) C, fun hC ↦ ?_⟩
    dsimp at hC
    simpa [h.not_ge] using Fintype.card_le_of_surjective _ hC.of_comp

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

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s

pp: case calc_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s =
    ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s

pp: case calc_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s = ∑ s ∈ 𝒜, f s

Tactic:
· rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]
    · exact sum_congr rfl fun s hs ↦ collapse_eq (notMem_mono (mem_powerset.1 hs) hu) _ _
    · exact (insert_erase_invOn.2.injOn).mono fun s hs ↦ notMem_mono (mem_powerset.1 hs) hu

Goal state after:
case calc_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s =
    ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s

case calc_3
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s = ∑ s ∈ 𝒜, f s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
v w : V
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
hv : v ∈ s
hadj : G.Adj v w
⊢ w ∈ t

Tactic:
by
  apply h.mem_of_adj at hadj
  have nhv : v ∉ t := Set.disjoint_left.mp h.disjoint hv
  simpa [hv, nhv] using hadj

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

Goal state before:
pp: case refine_1
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 β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V ⊕ V
hl : l ∈ left
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1

Tactic:
obtain ⟨r, hr⟩ : right.Nonempty := card_pos.mp <| card_pos.trans_le card_right.ge

Goal state after:
case refine_1
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 β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V ⊕ V
hl : l ∈ left
r : V ⊕ V
hr : r ∈ right
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
⊢ G.Connected

Tactic:
have := (nonempty_prod.1 h.nonempty).1

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ G.Connected
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
⊢ H.Connected

Tactic:
have := (nonempty_prod.1 h.nonempty).1

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
h : (G □ H).Connected
this : Nonempty α
⊢ H.Connected
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤

Tactic:
← not_ne_iff,

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
⊢ ¬(G □ H).edist x y ≠ ⊤ ↔ ¬G.edist x.1 y.1 ≠ ⊤ ∨ ¬H.edist x.2 y.2 ≠ ⊤
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
⊢ u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
hu

Goal state after:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
⊢ v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
Module: Mathlib.Combinatorics.SimpleGraph.Sum

Goal state before:
pp: V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable n

Tactic:
rw [← n.max_self]

Goal state after:
V : Type u_3
W : Type u_5
G : SimpleGraph V
H : SimpleGraph W
n : ℕ
x✝ : G.Colorable n ∧ H.Colorable n
cG : G.Colorable n
cH : H.Colorable n
⊢ (G ⊕g H).Colorable (max n n)
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_1.inl.inr.refine_3
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 β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : i ∈ left.toLeft
j : V
hj : j ∈ ↑right.toRight
⊢ G.Adj i j

Tactic:
mem_toLeft

Goal state after:
case refine_1.inl.inr.refine_3
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 β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inl l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inr r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inr r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inl i ∈ left
j : V
hj : j ∈ ↑right.toRight
⊢ G.Adj i j
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: case succ
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
⊢ ↑(G.finsetWalkLength (n + 1) u v) = {p | p.length = n + 1}

Tactic:
| succ n ih =>

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

Goal state before:
pp: case refine_1.inr.inl.refine_3
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 β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : j ∈ right.toLeft
⊢ G.Adj i j

Tactic:
mem_toLeft

Goal state after:
case refine_1.inr.inl.refine_3
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 β
x✝ :
  ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween ↑left ↑right
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V},
    l' ∈ left → ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V},
    r' ∈ right → ((Sum.inl r).isLeft = true → r'.isLeft = true) ∧ ((Sum.inl r).isRight = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : Sum.inl j ∈ right
⊢ G.Adj i j
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 β
⊢ completeBipartiteGraph α β ⊑ G.bipartiteDoubleCover ↔ completeBipartiteGraph α β ⊑ G

Tactic:
by
  have : Fintype α := .ofFinite α
  have : Fintype β := .ofFinite β
  simp_rw [completeBipartiteGraph_isContained_iff]
  refine ⟨fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_,
    fun ⟨left, right, card_left, card_right, h⟩ ↦ ?_⟩
  · simp_rw [← card_left, ← card_right]
    obtain ⟨l, hl⟩ : left.Nonempty := card_pos.mp <| card_pos.trans_le card_left.ge
    obtain ⟨r, hr⟩ : right.Nonempty := card_pos.mp <| card_pos.trans_le card_right.ge
    have hmem_left {l'} (hl' : l' ∈ left) :
        (l.isLeft → l'.isLeft) ∧ (l.isRight → l'.isRight) := by
      rcases l with l | l <;> rcases r with r | r <;> rcases l' with l' | l'
      all_goals solve | simp | simpa using h hl hr | simpa using h hl' hr
    have hmem_right {r'} (hr' : r' ∈ right) :
        (r.isLeft → r'.isLeft) ∧ (r.isRight → r'.isRight) := by
      rcases l with l | l <;> rcases r with r | r <;> rcases r' with r' | r'
      all_goals solve | simp | simpa using h hl hr | simpa using h hl hr'
    rcases l with l | l <;> rcases r with r | r
    · simpa using h hl hr
    · refine ⟨left.toLeft, right.toRight, ?_, ?_, fun i hi j hj ↦ ?_⟩
      · exact card_bij (fun i _ ↦ .inl i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getLeft <| (hmem_left hi).left Sum.isLeft_inl, by simp [hi]⟩)
      · exact card_bij (fun j hj ↦ .inr j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getRight <| (hmem_right hj).right Sum.isRight_inr, by simp [hj]⟩)
      · rw [mem_coe, mem_toLeft] at hi
        rw [mem_coe, mem_toRight] at hj
        simpa using h hi hj
    · refine ⟨left.toRight, right.toLeft, ?_, ?_, fun i hi j hj ↦ ?_⟩
      · exact card_bij (fun i _ ↦ .inr i) (fun i hi ↦ by simpa using hi) (fun i hi j hj ↦ by simp)
          (fun i hi ↦ ⟨i.getRight <| (hmem_left hi).right Sum.isRight_inr, by simp [hi]⟩)
      · exact card_bij (fun j hj ↦ .inl j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getLeft <| (hmem_right hj).left Sum.isLeft_inl, by simp [hj]⟩)
      · rw [mem_coe, mem_toRight] at hi
        rw [mem_coe, mem_toLeft] at hj
        simpa using h hi hj
    · simpa using h hl hr
  · simp_rw [← card_left, ← card_right]
    refine ⟨left.map .inl, right.map .inr, card_map _, card_map _, fun i hi j hj ↦ ?_⟩
    simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj
    obtain ⟨i', hi', hi⟩ := hi
    obtain ⟨j', hj', hj⟩ := hj
    simpa [← hi, ← hj] using h hi' hj'

Goal state after: