mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a : V
p : Path a a
⊢ p.length = 0 ↔ p = nil

Tactic:
cases p <;> tauto

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∈ s
⊢ s ∈ 𝓓 a 𝒜

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ s ∈ 𝓓 a 𝒜

Tactic:
· rwa [insert_eq_of_mem ha] at h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ s ∈ 𝓓 a 𝒜
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
⊢ Surjective ⇑supIrredLowerSet

Tactic:
by
  aesop (add simp Surjective)

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
⊢ Surjective ⇑infIrredUpperSet

Tactic:
by
  aesop (add simp Surjective)

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha✝ : a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }
i : { a // SupIrred a }
hi : i ∈ (↑s).toFinset
ha : ↑a ≤ ↑i
⊢ a ∈ ↑s

Tactic:
exact s.lower ha (Set.mem_toFinset.1 hi)

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case neg
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : Fintype α
inst✝ : DecidablePred SupIrred
h : Nonempty α
this : OrderBot α
⊢ α ↪o Set { a // SupIrred a }

Tactic:
exact OrderIso.lowerSetSupIrred.toOrderEmbedding.trans ⟨⟨_, SetLike.coe_injective⟩, Iff.rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
set m := 𝒜.card with hm

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₂ : univ ∉ 𝒜
m : ℕ := #𝒜
hm : m = #𝒜
⊢ supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∉ u
⊢ a ∈ (t ⊔ u) \ v

Tactic:
rw [sup_eq_union, mem_sdiff, mem_union]
        exact ⟨Or.inl hat, hav⟩

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

Goal state before:
pp: case ind.inr.succ.h𝒜
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
s : Finset α
𝒜 : Finset (Finset α)
hs : s ∉ 𝒜
h𝒜₁ : (insert s 𝒜).Nonempty
h𝒜₂ : univ ∉ insert s 𝒜
h𝒜₃ : (insert s 𝒜).Nontrivial
ih :
  ∀ (𝒜_1 : Finset (Finset α)),
    #𝒜_1 < #𝒜 + 1 → 𝒜_1.Nonempty → univ ∉ 𝒜_1 → supSum 𝒜_1 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
hm : #𝒜 + 1 = #(insert s 𝒜)
h𝒜 : 𝒜.Nonempty
⊢ #(image (fun x ↦ s ⊓ x) 𝒜) < #𝒜 + 1

Tactic:
exact card_image_le.trans_lt (lt_add_one _)

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∑ s ∈ 𝒜, (↑((Fintype.card α).choose #s))⁻¹ =
    ∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, (↑((Fintype.card α).choose r))⁻¹

Tactic:
rw [sum_fiberwise_of_maps_to']

Goal state after:
case h
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ ∀ i ∈ 𝒜, #i ∈ range (Fintype.card α + 1)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∈ 𝒜 ∧ u.erase a ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
· exact ⟨u, hu.1, rfl⟩

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s → x ∈ {x | (mkClasses c H) x y}

Tactic:
intro hx _s' hs' hx'

Goal state after:
case mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ s
_s' : Set α
hs' : _s' ∈ c
hx' : x ∈ _s'
⊢ y ∈ _s'
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: 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
U₁ V₁ : Finset (Fin n)
huseful : UsefulCompression U₁ V₁
hUcard : #U₁ < #U
h : ¬IsCompressed U₁ V₁ 𝒜
⊢ False

Tactic:
exact hUcard.not_ge <| t ⟨U₁, V₁⟩ <| mem_filter.2 ⟨mem_univ _, huseful, h⟩

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

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

Tactic:
by
    rw [Partitions.ext_iff, ← classes_mkClasses C.toSet C.isPartition]
    rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C✝ : G.Coloring α
inst✝² : Nonempty (G.Coloring α)
inst✝¹ : Infinite α
inst✝ : Nonempty V
C : G.Coloring α
v : V
⊢ Infinite (G.Coloring α)

Tactic:
let f c := (Iso.completeGraph <| Equiv.swap (C v) c).toHom.comp C

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C✝ : G.Coloring α
inst✝² : Nonempty (G.Coloring α)
inst✝¹ : Infinite α
inst✝ : Nonempty V
C : G.Coloring α
v : V
f : α → G →g completeGraph α := fun c ↦ (Iso.completeGraph (Equiv.swap (C v) c)).toHom.comp C
⊢ Infinite (G.Coloring α)
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 ↑𝒞
⊢ #(∂^[i] 𝒞) ≤ #(∂^[i] 𝒜)

Tactic:
refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
      · rwa [card_powersetCard, card_attachFin, card_range]
      simp_rw [𝒞, mem_powersetCard]
      rintro A B hA ⟨HB₁, HB₂⟩
      refine ⟨fun t ht ↦ ?_, ‹_›⟩
      rw [mem_attachFin, mem_range]
      have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
        rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
      apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
      simp_rw [mem_image]
      rintro _ ⟨a, ha, hab⟩
      simpa [range'k, hab] using hA.1 ha

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
⊢ #𝒜 ≤ (n - 1).choose (r - 1)

Tactic:
by
  -- Take care of the r=0 case first: it's not very interesting.
  rcases Nat.eq_zero_or_pos r with b | h1r
  · convert! Nat.zero_le _
    rw [Finset.card_eq_zero, eq_empty_iff_forall_notMem]
    refine fun A HA ↦ h𝒜 HA HA ?_
    rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]
    exact h₂ HA
  refine le_of_not_gt fun size ↦ ?_
  -- Consider 𝒜ᶜˢ = {sᶜ | s ∈ 𝒜}
  -- Its iterated shadow (∂^[n-2k] 𝒜ᶜˢ) is disjoint from 𝒜 by intersecting-ness
  have : Disjoint 𝒜 (∂^[n - 2 * r] 𝒜ᶜˢ) := disjoint_right.2 fun A hAbar hA ↦ by
    simp only [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
    obtain ⟨C, hC, hAC, _⟩ := hAbar
    exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)
  have : r ≤ n := h₃.trans (Nat.div_le_self n 2)
  have : 1 ≤ n := ‹1 ≤ r›.trans ‹r ≤ n›
  -- We know the size of 𝒜ᶜˢ since it's the same size as 𝒜
  have z : (n - 1).choose (n - r) < #𝒜ᶜˢ := by
    rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]
  -- and everything in 𝒜ᶜˢ has size n-r.
  have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls
  -- We can use the Lovasz form of Kruskal-Katona to get |∂^[n-2k] 𝒜ᶜˢ| ≥ (n-1) choose r
  have kk := kruskal_katona_lovasz_form (i := n - 2 * r) (by lia)
    ((tsub_le_tsub_iff_left ‹1 ≤ n›).2 h1r) tsub_le_self h𝒜bar z.le
  have : n - r - (n - 2 * r) = r := by lia
  rw [this] at kk
  -- But this gives a contradiction: `n choose r < |𝒜| + |∂^[n-2k] 𝒜ᶜˢ|`
  have := calc
    n.choose r = (n - 1).choose (r - 1) + (n - 1).choose r := by
      convert! Nat.choose_succ_succ _ _ using 3 <;> rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
    _ < #𝒜 + #(∂^[n - 2 * r] 𝒜ᶜˢ) := add_lt_add_of_lt_of_le size kk
    _ = #(𝒜 ∪ ∂^[n - 2 * r] 𝒜ᶜˢ) := by rw [card_union_of_disjoint ‹_›]
  apply this.not_ge
  convert! Set.Sized.card_le _
  · rw [Fintype.card_fin]
  rw [coe_union, Set.sized_union]
  refine ⟨‹_›, ?_⟩
  convert! h𝒜bar.shadow_iterate
  lia

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

Goal state before:
pp: V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
⊢ ∀ {v w : V ⊕ W}, (completeBipartiteGraph V W).Adj v w → v.isRight ≠ w.isRight

Tactic:
intro v w
      cases v <;> cases w <;> simp

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

Goal state before:
pp: V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ G.degree v ≤ #t

Tactic:
rw [← card_neighborFinset_eq_degree]

Goal state after:
V : Type u_1
v : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet v)
h : G.IsBipartiteWith ↑s ↑t
hv : v ∈ s
⊢ #(G.neighborFinset v) ≤ #t
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ G.degree w ≤ #s

Tactic:
rw [← card_neighborFinset_eq_degree]

Goal state after:
V : Type u_1
w : V
G : SimpleGraph V
s t : Finset V
inst✝ : Fintype ↑(G.neighborSet w)
h : G.IsBipartiteWith ↑s ↑t
hw : w ∈ t
⊢ #(G.neighborFinset w) ≤ #s
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ v ∈ s.attach, #(bipartiteAbove G.Adj t ↑v) = ∑ w ∈ t.attach, #(bipartiteBelow G.Adj s ↑w)

Tactic:
sum_attach s fun w ↦ #(bipartiteAbove G.Adj t w),

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
⊢ ∑ x ∈ s, #(bipartiteAbove G.Adj t x) = ∑ w ∈ t.attach, #(bipartiteBelow G.Adj s ↑w)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case refine_2
V : Type u
G : SimpleGraph V
G' : G.Subgraph
x✝ : ∃ C, C.toSubgraph = G'
C : G.ConnectedComponent
h : C.toSubgraph = G'
⊢ Maximal Subgraph.Connected G'

Tactic:
· exact h ▸ maximal_connected_toSubgraph _

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✝¹ : Fintype α
inst✝ : Fintype β
⊢ completeBipartiteGraph α β ⊑ G →
    ∃ left right, #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween ↑left ↑right

Tactic:
refine fun ⟨f⟩ ↦ ⟨univ.map ⟨f ∘ Sum.inl, f.injective.comp Sum.inl_injective⟩,
      univ.map ⟨f ∘ Sum.inr, f.injective.comp Sum.inr_injective⟩, by simp, by simp,
      fun _ hl _ hr ↦ ?_⟩

Goal state after:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
x✝² : completeBipartiteGraph α β ⊑ G
f : (completeBipartiteGraph α β).Copy G
x✝¹ : V
hl : x✝¹ ∈ ↑(map { toFun := ⇑f ∘ Sum.inl, inj' := ⋯ } univ)
x✝ : V
hr : x✝ ∈ ↑(map { toFun := ⇑f ∘ Sum.inr, inj' := ⋯ } univ)
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
⊢ G.edist u w ≤ G.edist u v + G.edist v w

Tactic:
obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw

Goal state after:
case inr.inr
V : Type u_1
G : SimpleGraph V
u v w : V
huv : G.edist u v ≠ ⊤
hvw : G.edist v w ≠ ⊤
p : G.Walk u v
hp : ↑p.length = G.edist u v
q : G.Walk v w
hq : ↑q.length = G.edist v w
⊢ G.edist u w ≤ G.edist u v + G.edist v w
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 β
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
l' : V ⊕ V
hl' : l' ∈ left
⊢ (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)

Tactic:
rcases l with l | l

Goal state after:
case inl
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
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inl l ∈ left
⊢ ((Sum.inl l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inl l).isRight = true → l'.isRight = true)

case inr
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
r : V ⊕ V
hr : r ∈ right
l' : V ⊕ V
hl' : l' ∈ left
l : V
hl : Sum.inr l ∈ left
⊢ ((Sum.inr l).isLeft = true → l'.isLeft = true) ∧ ((Sum.inr l).isRight = true → l'.isRight = true)
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 β
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
hmem_left : ∀ {l' : V ⊕ V}, l' ∈ left → (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)
r' : V ⊕ V
hr' : r' ∈ right
⊢ (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)

Tactic:
rcases l with l | l

Goal state after:
case inl
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
r : V ⊕ V
hr : r ∈ right
r' : V ⊕ V
hr' : r' ∈ 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.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)

case inr
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
r : V ⊕ V
hr : r ∈ right
r' : V ⊕ V
hr' : r' ∈ 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.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
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
r : V ⊕ V
hr : r ∈ right
hmem_left : ∀ {l' : V ⊕ V}, l' ∈ left → (l.isLeft = true → l'.isLeft = true) ∧ (l.isRight = true → l'.isRight = true)
hmem_right : ∀ {r' : V ⊕ V}, r' ∈ right → (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1

Tactic:
rcases l with l | l

Goal state after:
case refine_1.inl
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
r : V ⊕ V
hr : r ∈ right
hmem_right : ∀ {r' : V ⊕ V}, r' ∈ right → (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
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)
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1

case refine_1.inr
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
r : V ⊕ V
hr : r ∈ right
hmem_right : ∀ {r' : V ⊕ V}, r' ∈ right → (r.isLeft = true → r'.isLeft = true) ∧ (r.isRight = true → r'.isRight = true)
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)
⊢ ∃ left_1 right_1, #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween ↑left_1 ↑right_1
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 β
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)
j : V
hj : j ∈ right.toRight
⊢ Sum.inr j ∈ right

Tactic:
simpa using hj

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : ↑G'.verts
hu : u ∈ G''.verts
hfu : f u = u'
⊢ ∀ (v : ↑(Subgraph.map f G'').verts), (Subgraph.map f G'').coe.Reachable ⟨u', ⋯⟩ v

Tactic:
⟨v', v, hv, hfv⟩

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : ↑G'.verts
hu : u ∈ G''.verts
hfu : f u = u'
v' : V
v : ↑G'.verts
hv : v ∈ G''.verts
hfv : f v = v'
⊢ (Subgraph.map f G'').coe.Reachable ⟨u', ⋯⟩ ⟨v', ⋯⟩
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 β
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)
j : V
hj : j ∈ right.toLeft
⊢ Sum.inl j ∈ right

Tactic:
simpa using hj

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

Goal state before:
pp: case mpr
V : Type u_1
G : SimpleGraph V
⊢ (Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath) → G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y

Tactic:
rintro ⟨hV, h⟩

Goal state after:
case mpr
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
⊢ G.Connected ∧ ∀ (u v : V) (x y : G.Path u v), x = y
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case mpr.refine_1
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
⊢ G.Reachable v w

Tactic:
obtain ⟨p, _⟩ := h v w

Goal state after:
case mpr.refine_1
V : Type u_1
G : SimpleGraph V
hV : Nonempty V
h : ∀ (v w : V), ∃! p, p.IsPath
v w : V
p : G.Walk v w
h✝ : (fun p ↦ p.IsPath) p ∧ ∀ (y : G.Walk v w), (fun p ↦ p.IsPath) y → y = p
⊢ G.Reachable v w