awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
p : SimpleGraph V → Prop
hG : G.IsExtremal p
H : SimpleGraph V
hH : p H
⊢ G ≤ H ↔ G = H

Tactic:
⟨fun hGH ↦ edgeFinset_inj.1 <|
    eq_of_subset_of_card_le (edgeFinset_subset_edgeFinset.2 hGH) (hG.2 hH), le_of_eq⟩

Premises used: Iff.mpr, SimpleGraph.edgeFinset_inj, And.right, Iff.intro, Iff.mp, SimpleGraph.edgeFinset_subset_edgeFinset, Finset.eq_of_subset_of_card_le, le_of_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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
rw :
  LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
      (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset) ∧
    LE.le (α := ℕ) (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)
      (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
⊢ extremalNumber n H = sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset

Tactic:
rw [extremalNumber, le_antisymm_iff]

Premises used: SimpleGraph.extremalNumber, le_antisymm_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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
refine_1 :
  LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
    (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)
refine_2 :
  LE.le (α := ℕ) (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)
    (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
⊢ LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
      (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset) ∧
    LE.le (α := ℕ) (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)
      (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)

Tactic:
and_intros
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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
refine_1 :
  ∀ (e : Fin n ≃ V),
    LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
      (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)
⊢ LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
    (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)

Tactic:
replace e := e.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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
refine_1 :
  ∀ (e : Fin n ≃ V),
    LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
      (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)
⊢ LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
    (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)

Tactic:
on_goal 1 =>
    replace e := e.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n : ℕ
V : Type u_1
W : Type u_2
H : SimpleGraph W
inst : Fintype V
hc : Fintype.card V = n
e : Fin n ≃ V
refine_1 :
  ∀ (b : SimpleGraph (Fin n)),
    Membership.mem (γ := Finset (SimpleGraph (Fin n))) {G : SimpleGraph (Fin n) | H.Free G} b →
      #b.edgeFinset ≤ sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset
⊢ LE.le (α := ℕ) (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)
    (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)

Tactic:
rw [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {G : SimpleGraph (Fin n) | H.Free G} G
G' : SimpleGraph V := SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G
rw : Membership.mem (γ := Finset (SimpleGraph V)) univ G' ∧ H.Free G
⊢ Membership.mem (γ := Finset (SimpleGraph V)) {x : SimpleGraph V | H.Free x} G'

Tactic:
rw [mem_filter, ← free_congr .refl (.map e G)]

Premises used: SimpleGraph.Iso.refl, SimpleGraph.Iso.map, SimpleGraph.free_congr, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {G : SimpleGraph (Fin n) | H.Free G} G
G' : SimpleGraph V := SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G
⊢ Membership.mem (γ := Finset (SimpleGraph V)) univ G' ∧ H.Free G

Tactic:
simpa using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {G : SimpleGraph (Fin n) | H.Free G} G
G' : SimpleGraph V := SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G
⊢ Membership.mem (γ := Finset (SimpleGraph V)) {x : SimpleGraph V | H.Free x} G'

Tactic:
replace h' : G' ∈ univ.filter (H.Free ·) := by
    rw [mem_filter, ← free_congr .refl (.map e G)]
    simpa using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {G : SimpleGraph (Fin n) | H.Free G} G
G' : SimpleGraph V := SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G
h' : Membership.mem (γ := Finset (SimpleGraph V)) {x : SimpleGraph V | H.Free x} G'
refine_1 :
  Finset.card (α := Sym2 V) (edgeFinset (SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G)) ≤
    sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset
⊢ #G.edgeFinset ≤ sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset

Tactic:
rw [Iso.card_edgeFinset_eq (.map e G)]

Premises used: SimpleGraph.Iso.map, SimpleGraph.Iso.card_edgeFinset_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {G : SimpleGraph (Fin n) | H.Free G} G
G' : SimpleGraph V := SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G
h' : Membership.mem (γ := Finset (SimpleGraph V)) {x : SimpleGraph V | H.Free x} G'
⊢ LE.le (α := ℕ) ((fun (x : SimpleGraph V) ↦ #x.edgeFinset) G')
    (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)

Tactic:
@le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G' h'

Premises used: Finset.le_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {G : SimpleGraph (Fin n) | H.Free G} G
G' : SimpleGraph V := SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G
h' : Membership.mem (γ := Finset (SimpleGraph V)) {x : SimpleGraph V | H.Free x} G'
⊢ Finset.card (α := Sym2 V) (edgeFinset (SimpleGraph.map (⇑e.toEmbedding : (a : Fin n) → V) G)) ≤
    sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset

Tactic:
convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G' h'

Premises used: Finset.le_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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
refine_2 :
  ∀ (b : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} b →
      #b.edgeFinset ≤ sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset
⊢ LE.le (α := ℕ) (sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset)
    (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)

Tactic:
rw [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} G
G' : SimpleGraph (Fin n) := SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G
rw : Membership.mem (γ := Finset (SimpleGraph (Fin n))) univ G' ∧ H.Free G
⊢ Membership.mem (γ := Finset (SimpleGraph (Fin n))) {x : SimpleGraph (Fin n) | H.Free x} G'

Tactic:
rw [mem_filter, ← free_congr .refl (.map e G)]

Premises used: SimpleGraph.Iso.refl, SimpleGraph.Iso.map, SimpleGraph.free_congr, Finset.mem_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} G
G' : SimpleGraph (Fin n) := SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G
⊢ Membership.mem (γ := Finset (SimpleGraph (Fin n))) univ G' ∧ H.Free G

Tactic:
simpa using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} G
G' : SimpleGraph (Fin n) := SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G
⊢ Membership.mem (γ := Finset (SimpleGraph (Fin n))) {x : SimpleGraph (Fin n) | H.Free x} G'

Tactic:
replace h' : G' ∈ univ.filter (H.Free ·) := by
    rw [mem_filter, ← free_congr .refl (.map e G)]
    simpa using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} G
G' : SimpleGraph (Fin n) := SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G
h' : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {x : SimpleGraph (Fin n) | H.Free x} G'
refine_2 :
  Finset.card (α := Sym2 (Fin n)) (edgeFinset (SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G)) ≤
    sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset
⊢ #G.edgeFinset ≤ sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset

Tactic:
rw [Iso.card_edgeFinset_eq (.map e G)]

Premises used: SimpleGraph.Iso.map, SimpleGraph.Iso.card_edgeFinset_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} G
G' : SimpleGraph (Fin n) := SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G
h' : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {x : SimpleGraph (Fin n) | H.Free x} G'
⊢ LE.le (α := ℕ) ((fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset) G')
    (sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset)

Tactic:
@le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G' h'

Premises used: Finset.le_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
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 : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} G
G' : SimpleGraph (Fin n) := SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G
h' : Membership.mem (γ := Finset (SimpleGraph (Fin n))) {x : SimpleGraph (Fin n) | H.Free x} G'
⊢ Finset.card (α := Sym2 (Fin n)) (edgeFinset (SimpleGraph.map (⇑e.toEmbedding : (a : V) → Fin n) G)) ≤
    sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset

Tactic:
convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G' h'

Premises used: Finset.le_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : H.Free G
rw : #G.edgeFinset ≤ sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H

Tactic:
rw [extremalNumber_of_fintypeCard_eq rfl]

Premises used: SimpleGraph.extremalNumber_of_fintypeCard_eq, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : H.Free G
⊢ Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | H.Free G} G

Tactic:
simpa using h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset

Tactic:
convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G (by simpa using h)
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : extremalNumber (Fintype.card V) H < #G.edgeFinset
contrapose : ∀ (h : ¬H ⊑ G), ¬extremalNumber (Fintype.card V) H < #G.edgeFinset
⊢ H ⊑ G

Tactic:
contrapose h
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : ¬H ⊑ G
push : #G.edgeFinset ≤ extremalNumber (Fintype.card V) H
⊢ ¬extremalNumber (Fintype.card V) H < #G.edgeFinset

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : ¬H ⊑ G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H

Tactic:
card_edgeFinset_le_extremalNumber h

Premises used: SimpleGraph.card_edgeFinset_le_extremalNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : DecidableRel G.Adj
h : ¬H ⊑ G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card V) H

Tactic:
exact card_edgeFinset_le_extremalNumber h

Premises used: SimpleGraph.card_edgeFinset_le_extremalNumber
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
simp_rw :
  (∀ (b : SimpleGraph V), H.Free b → #b.edgeFinset ≤ m) ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_1 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m
⊢ extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_1 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m

Tactic:
simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.sup_le_iff, mem_filter_univ]

Premises used: Finset.mem_filter_univ, SimpleGraph.extremalNumber_of_fintypeCard_eq, Finset.sup_le_iff, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
h : ∀ (b : SimpleGraph V), H.Free b → #b.edgeFinset ≤ m
x : SimpleGraph V
x_1 : DecidableRel x.Adj
h' : H.Free x
⊢ #x.edgeFinset ≤ m

Tactic:
h _ h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
h : ∀ (b : SimpleGraph V), H.Free b → #b.edgeFinset ≤ m
x : SimpleGraph V
x_1 : DecidableRel x.Adj
h' : H.Free x
⊢ #x.edgeFinset ≤ m

Tactic:
convert! h _ h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
h : ∀ ⦃G : SimpleGraph V⦄ [inst_1 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m
x : SimpleGraph V
h' : H.Free x
⊢ #x.edgeFinset ≤ m

Tactic:
h h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
h : ∀ ⦃G : SimpleGraph V⦄ [inst_1 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m
x : SimpleGraph V
h' : H.Free x
⊢ #x.edgeFinset ≤ m

Tactic:
convert! h h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
⊢ (∀ (b : SimpleGraph V), H.Free b → #b.edgeFinset ≤ m) ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_1 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m

Tactic:
exact ⟨fun h _ _ h' ↦ by convert! h _ h', fun h _ h' ↦ by convert! h h'⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
simp_rw :
  (∃ (b : SimpleGraph V), H.Free b ∧ m < #b.edgeFinset) ↔
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < #G.edgeFinset
⊢ m < extremalNumber (Fintype.card V) H ↔ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < #G.edgeFinset

Tactic:
simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.lt_sup_iff, mem_filter_univ]

Premises used: Finset.mem_filter_univ, SimpleGraph.extremalNumber_of_fintypeCard_eq, Finset.lt_sup_iff, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
h_1 : ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < #G.edgeFinset
w : SimpleGraph V
w_1 : DecidableRel w.Adj
h : H.Free w
h' : m < #w.edgeFinset
⊢ m < #w.edgeFinset

Tactic:
h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
h_1 : ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < #G.edgeFinset
w : SimpleGraph V
w_1 : DecidableRel w.Adj
h : H.Free w
h' : m < #w.edgeFinset
⊢ m < #w.edgeFinset

Tactic:
convert!
    h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
⊢ (∃ (b : SimpleGraph V), H.Free b ∧ m < #b.edgeFinset) ↔
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < #G.edgeFinset

Tactic:
exact ⟨fun ⟨_, h, h'⟩ ↦ ⟨_, _, h, h'⟩, fun ⟨_, _, h, h'⟩ ↦ ⟨_, h, by convert!
    h'⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
R : Type u_3
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
simp_rw :
  extremalNumber (Fintype.card V) H ≤ ⌊m⌋₊ ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_4 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ ⌊m⌋₊
⊢ (↑(extremalNumber (Fintype.card V) H) : R) ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_4 : DecidableRel G.Adj], H.Free G → (↑(#G.edgeFinset) : R) ≤ m

Tactic:
simp_rw [← Nat.le_floor_iff h]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
R : Type u_3
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ extremalNumber (Fintype.card V) H ≤ ⌊m⌋₊ ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_4 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ ⌊m⌋₊

Tactic:
extremalNumber_le_iff H ⌊m⌋₊

Premises used: SimpleGraph.extremalNumber_le_iff, Nat.floor
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
R : Type u_3
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ extremalNumber (Fintype.card V) H ≤ ⌊m⌋₊ ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_4 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ ⌊m⌋₊

Tactic:
exact extremalNumber_le_iff H ⌊m⌋₊

Premises used: SimpleGraph.extremalNumber_le_iff, Nat.floor
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
R : Type u_3
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
simp_rw :
  ⌊m⌋₊ < extremalNumber (Fintype.card V) H ↔
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ ⌊m⌋₊ < #G.edgeFinset
⊢ m < (↑(extremalNumber (Fintype.card V) H) : R) ↔
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < (↑(#G.edgeFinset) : R)

Tactic:
simp_rw [← Nat.floor_lt h]

Premises used: Nat.floor_lt
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
R : Type u_3
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ ⌊m⌋₊ < extremalNumber (Fintype.card V) H ↔
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ ⌊m⌋₊ < #G.edgeFinset

Tactic:
lt_extremalNumber_iff H ⌊m⌋₊

Premises used: SimpleGraph.lt_extremalNumber_iff, Nat.floor
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
R : Type u_3
inst_1 : Semiring R
inst_2 : LinearOrder R
inst_3 : FloorSemiring R
H : SimpleGraph W
m : R
h : 0 ≤ m
⊢ ⌊m⌋₊ < extremalNumber (Fintype.card V) H ↔
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ ⌊m⌋₊ < #G.edgeFinset

Tactic:
exact lt_extremalNumber_iff H ⌊m⌋₊

Premises used: SimpleGraph.lt_extremalNumber_iff, Nat.floor
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
rw :
  ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
    H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
⊢ extremalNumber n H' ≤ extremalNumber n H

Tactic:
rw [← Fintype.card_fin n, extremalNumber_le_iff]

Premises used: Fintype.card_fin, SimpleGraph.extremalNumber_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G : SimpleGraph (Fin n)
_ : ∀ [inst : DecidableRel G.Adj], H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
⊢ ∀ [inst : DecidableRel G.Adj], H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G : SimpleGraph (Fin n)
inst : DecidableRel G.Adj
h' : H'.Free G
contrapose! : ∀ (h' : extremalNumber (Fintype.card (Fin n)) H < #G.edgeFinset), H' ⊑ G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H

Tactic:
contrapose! h'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G : SimpleGraph (Fin n)
inst : DecidableRel G.Adj
h' : extremalNumber (Fintype.card (Fin n)) H < #G.edgeFinset
⊢ H' ⊑ G

Tactic:
h.trans (IsContained.of_extremalNumber_lt_card_edgeFinset h')

Premises used: SimpleGraph.IsContained.of_extremalNumber_lt_card_edgeFinset, SimpleGraph.IsContained.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
G : SimpleGraph (Fin n)
inst : DecidableRel G.Adj
h' : extremalNumber (Fintype.card (Fin n)) H < #G.edgeFinset
⊢ H' ⊑ G

Tactic:
exact h.trans (IsContained.of_extremalNumber_lt_card_edgeFinset h')

Premises used: SimpleGraph.IsContained.of_extremalNumber_lt_card_edgeFinset, SimpleGraph.IsContained.trans