mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: case refine_2
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.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
i : V ⊕ V
hi : i ∈ ↑(map Function.Embedding.inl left)
j : V ⊕ V
hj : j ∈ ↑(map Function.Embedding.inr right)
⊢ G.bipartiteDoubleCover.Adj i j

Tactic:
simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj

Goal state after:
case refine_2
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.IsCompleteBetween ↑left ↑right
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
i j : V ⊕ V
hi : ∃ a ∈ left, Sum.inl a = i
hj : ∃ a ∈ right, Sum.inr a = j
⊢ G.bipartiteDoubleCover.Adj i j
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e
v : V
c : G.Walk v v
hc : c.IsCycle
⊢ c.edges ≠ []

Tactic:
simp [hc.not_nil]

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

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
y : V
hy : y ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨y, hy⟩
px : G.Walk x v
left✝ : px ∈ G.finsetWalkLength n x v
py : G.Walk y v
hpy : py ∈ G.finsetWalkLength n y v
hp : { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } py = { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } px
⊢ { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } px ∈ ⊥

Tactic:
cases hp

Goal state after:
case succ.refl
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v x : V
hx : x ∈ G.neighborSet u
px : G.Walk x v
left✝ : px ∈ G.finsetWalkLength n x v
hy : x ∈ G.neighborSet u
hxy : ⟨x, hx⟩ ≠ ⟨x, hy⟩
hpy : px ∈ G.finsetWalkLength n x v
⊢ { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } px ∈ ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case h
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this✝ : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
x✝ y✝ : V
heH : s(x✝, y✝) ∈ H.edgeSet
heF : s(x✝, y✝) ∉ F.edgeSet
h_bridge : (F ⊔ fromEdgeSet {s(x✝, y✝)}).IsBridge s(x✝, y✝)
this : (F ⊔ fromEdgeSet {s(x✝, y✝)}).deleteEdges {s(x✝, y✝)} = F
⊢ False

Tactic:
isBridge_iff,

Goal state after:
case h
V : Type u_1
G F : SimpleGraph V
hle : F ≤ G
hF : F.IsAcyclic
h : F.Reachable = G.Reachable
this✝ : ¬Maximal (fun F ↦ F ≤ G ∧ F.IsAcyclic) F
H : SimpleGraph V
hFH : F < H
hHG : H ≤ G
hH : H.IsAcyclic
x✝ y✝ : V
heH : s(x✝, y✝) ∈ H.edgeSet
heF : s(x✝, y✝) ∉ F.edgeSet
h_bridge : ¬((F ⊔ fromEdgeSet {s(x✝, y✝)}).deleteEdges {s(x✝, y✝)}).Reachable x✝ y✝
this : (F ⊔ fromEdgeSet {s(x✝, y✝)}).deleteEdges {s(x✝, y✝)} = F
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, x ∈ univ → ¬G.IsNClique r x

Tactic:
mem_univ,

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
⊢ ∀ ⦃x : Finset V⦄, True → ¬G.IsNClique r x
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ (c ∈ univ ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (c ∈ univ ∧ c.supp ⊆ c'.supp) ∧ Odd {x | x ∈ univ ∧ G.connectedComponentMk x = c}.ncard

Tactic:
mem_univ,

Goal state after:
case intro
V : Type u
G : SimpleGraph V
inst✝ : Finite V
G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
val✝ : Fintype V
c : G.ConnectedComponent
⊢ (True ∧ Odd c.supp.ncard) ∧ c.supp ⊆ c'.supp ↔
    (True ∧ c.supp ⊆ c'.supp) ∧ Odd {x | True ∧ G.connectedComponentMk x = c}.ncard
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
ht : ¬t = 0
this : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
p : ↥K.parts
⊢ t ≤ #↑p

Tactic:
K.card_mem_parts p.prop

Goal state after:
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
p : ↥K.parts
⊢ t ≤ t
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_4
α : 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
p✝ : Finset V
h : ∃ a ∈ univ, { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } a = p✝
⊢ #p✝ = t

Tactic:
mem_univ,

Goal state after:
case neg.refine_4
α : 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
p✝ : Finset V
h : ∃ a, True ∧ { toFun := fun i ↦ map { toFun := fun j ↦ f (i, j), inj' := ⋯ } univ, inj' := ⋯ } a = p✝
⊢ #p✝ = t
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ ⊥.eccent u = ⊥.radius

Tactic:
eccent_bot,

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ ⊤ = ⊥.radius
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ (∃ x ∈ ↑C, x ∈ ↑D) → hom h C = D

Tactic:
· refine C.ind fun x xnL => ?_
    rintro ⟨x, ⟨_, e₁⟩, _, rfl⟩
    rw [← e₁]
    rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ n ^ 2 * (r - 1) + 2 * r * (n % r).choose 2 ≤ (r - 1) * n ^ 2 + (n % r) ^ 2 * (r - 1)

Tactic:
mul_comm,

Goal state after:
n r : ℕ
⊢ (r - 1) * n ^ 2 + 2 * r * (n % r).choose 2 ≤ (r - 1) * n ^ 2 + (n % r) ^ 2 * (r - 1)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑(#G.edgeFinset) ≤ ↑(extremalNumber n H) / ↑(n.choose 2) * ↑((n + 1).choose 2)

Tactic:
mul_comm,

Goal state after:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ↑(#G.edgeFinset) ≤ ↑((n + 1).choose 2) * (↑(extremalNumber n H) / ↑(n.choose 2))
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ∈ univ ∧ b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
mem_univ,

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    True ∧ b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEquiv) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ ∧ v ∉ K.vertsᶜ ∨ v ∈ K.vertsᶜ ∧ ¬∀ p ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).degree v < #K.verts - t' + t

Tactic:
and_not_self_iff,

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : False ∨ v ∈ K.vertsᶜ ∧ ¬∀ p ∈ K.parts, ∃ s ∈ powersetCard t p, ∀ w ∈ s, G.Adj v w
⊢ (between (↑K.verts) (↑K.verts)ᶜ G).degree v < #K.verts - t' + t
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ ∀ (b : SimpleGraph (V ⊕ W)),
    b ∈ univ ∧ b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
          #x.edgeFinset

Tactic:
mem_univ,

Goal state after:
case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ ∀ (b : SimpleGraph (V ⊕ W)),
    True ∧ b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b →
      #b.edgeFinset ≤
        {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
          #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ K.Free (SimpleGraph.map (⇑e₁.toEquiv) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ (H.turanDensity + ε) * ↑(n.choose 2) ≤ ↑(extremalNumber n H)

Tactic:
conv =>
      enter [2, 1, 1]
      rw [← Fintype.card_fin n]

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
x : ℝ
x✝ : x ∈ {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
m : ℕ
hm : m ∈ Set.Ici 2
hx : ↑(extremalNumber m H) / ↑(m.choose 2) = x
n : ℕ
hn : m ≤ n
G : SimpleGraph (Fin n)
w✝ : DecidableRel G.Adj
hcard_edges : ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(n.choose 2)
h_free : H.Free G
⊢ (H.turanDensity + ε) * ↑(n.choose 2) ≤ ↑(extremalNumber (Fintype.card (Fin n)) H)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: case h₂
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
v : Fin n
ht'_pos : 0 < t'
hv : v ∈ K.vertsᶜ
p : Finset (Fin n)
hp : p ∈ K.parts
hs✝ : t ≤ #({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
s : Finset (Fin n)
hs : s ∈ powersetCard t ({v_1 ∈ id p | (between (↑K.verts) (↑K.verts)ᶜ G).Adj v_1 v})
hs' : s ∈ powersetCard t p
w : Fin n
hw : w ∈ s
left✝ : w ∈ id p
hadj : G.Adj w v
right✝ : w ∈ ↑K.verts ∧ v ∈ (↑K.verts)ᶜ ∨ w ∈ (↑K.verts)ᶜ ∧ v ∈ ↑K.verts
⊢ G.Adj v w

Tactic:
exact hadj.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
⊢ (∀ (b : SimpleGraph (V ⊕ W)),
      b ∈ univ ∧ b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b → #b.edgeFinset ≤ x) ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x

Tactic:
mem_univ,

Goal state after:
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
⊢ (∀ (b : SimpleGraph (V ⊕ W)),
      True ∧ b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b → #b.edgeFinset ≤ x) ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
⊢ (∃ b, (b ∈ univ ∧ b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b) ∧ x < #b.edgeFinset) ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < #G.edgeFinset

Tactic:
mem_univ,

Goal state after:
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : ℕ
⊢ (∃ b, (True ∧ b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b) ∧ x < #b.edgeFinset) ↔
    ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < #G.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : Fintype V
inst✝⁵ : Fintype W
inst✝⁴ : Fintype α
inst✝³ : Fintype β
R : Type u_5
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
x : R
h : 0 ≤ x
⊢ zarankiewicz m n s t ≤ ⌊x⌋₊ ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ ⌊x⌋₊

Tactic:
exact zarankiewicz_le_iff hm hn hs ht ⌊x⌋₊

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    b ∈ univ ∧ b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
mem_univ,

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ∀ (b : SimpleGraph (Fin m ⊕ Fin n)),
    True ∧ b ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free b →
      #b.edgeFinset ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = ∑ᶠ (i : ι) (_ : i ∈ univ), (s i).ncard

Tactic:
← finite_univ.ncard_biUnion (by simpa) (fun _ _ _ _ hab ↦ h hab)

Goal state after:
α : Type u_1
ι : Type u_2
inst✝ : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ (⋃ i, s i).ncard = (⋃ i ∈ univ, s i).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case hb
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ G.bipartiteDoubleCover ∈ univ ∧
    G.bipartiteDoubleCover ≤ completeBipartiteGraph (Fin n) (Fin n) ∧
      (completeBipartiteGraph (Fin s) (Fin t)).Free G.bipartiteDoubleCover

Tactic:
mem_univ,

Goal state after:
case hb
n s t : ℕ
α : Type u_3
β : Type u_4
inst✝⁴ : Fintype α
inst✝³ : Fintype β
inst✝² : Nonempty α
inst✝¹ : Nonempty β
hs : Fintype.card α = s
ht : Fintype.card β = t
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
h : (completeBipartiteGraph α β).Free G
⊢ True ∧
    G.bipartiteDoubleCover ≤ completeBipartiteGraph (Fin n) (Fin n) ∧
      (completeBipartiteGraph (Fin s) (Fin t)).Free G.bipartiteDoubleCover