awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
inl : Finite.{u + 1} (G.ComponentCompl (↑∅ : Set V))
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
have inr : ∀ (h : K.Nonempty), Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
Tactic: classical
  rcases K.eq_empty_or_nonempty with rfl | h
  -- If K is empty, then removing K doesn't change the graph, which is connected, hence has a
  -- single connected component
  · dsimp [ComponentCompl]
    rw [Finset.coe_empty, Set.compl_empty]
    have := Gpc.out.subsingleton_connectedComponent
    exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
  -- Otherwise, we consider the function `touch` mapping a connected component to one of its
  -- vertices adjacent to `K`.
  · let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
      let p := C.exists_adj_boundary_pair Gpc.out h
      ⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩
    -- `touch` is injective
    have touch_inj : touch.Injective := fun C D h' => ComponentCompl.pairwise_disjoint.eq
      (Set.not_disjoint_iff.mpr ⟨touch C, (C.exists_adj_boundary_pair Gpc.out h).choose_spec.1,
                                 h'.symm ▸ (D.exists_adj_boundary_pair Gpc.out h).choose_spec.1⟩)
    -- `touch` has finite range
    have : Finite (Set.range touch) := by
      refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
      apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
      simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
    -- hence `touch` has a finite domain
    apply Finite.of_injective_finite_range touch_inj
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
x : (Finset V)ᵒᵖ
⊢ ↾ComponentCompl.hom (K := (↑(Opposite.unop x) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯ =
    𝟙 (G.ComponentCompl (↑(Opposite.unop x) : Set V))
have h : ∀ (x_1 : G.ComponentCompl (↑(Opposite.unop x) : Set V)) (x_2 : V),
  x_2 ∈
      (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾ComponentCompl.hom (K := (↑(Opposite.unop x) : Set V)) (L := (↑(Opposite.unop x) : Set V)) sorry))
            x_1).supp
        (K := (↑(Opposite.unop x) : Set V)) ↔
    x_2 ∈
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (G.ComponentCompl (↑(Opposite.unop x) : Set V)))).toFun x_1).supp
        (K := (↑(Opposite.unop x) : Set V))
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
x Y Z : (Finset V)ᵒᵖ
h : x ⟶ Y
h' : Y ⟶ Z
⊢ Eq (α := G.ComponentCompl (↑(Opposite.unop x) : Set V) ⟶ G.ComponentCompl (↑(Opposite.unop Z) : Set V))
    (↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯)
    (↾ComponentCompl.hom (K := (↑(Opposite.unop Y) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯ ≫
      ↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop Y) : Set V)) ⋯)
have h₁ : ∀ (C : G.ComponentCompl (↑(Opposite.unop x) : Set V)) (x_1 : V),
  x_1 ∈
      (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop x) : Set V)) sorry))
            C).supp
        (K := (↑(Opposite.unop Z) : Set V)) ↔
    x_1 ∈
      (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾ComponentCompl.hom (K := (↑(Opposite.unop Y) : Set V)) (L := (↑(Opposite.unop x) : Set V)) sorry ≫
                ↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop Y) : Set V)) sorry))
            C).supp
        (K := (↑(Opposite.unop Z) : Set V))
Tactic: ext C
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk (K := (↑(Opposite.unop L) : Set V)) vnL
⊢ s K = G.componentComplMk (K := (↑(Opposite.unop K) : Set V)) ⋯
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (G.componentComplFunctor.map h) :
      (a : (fun (X : Type u) ↦ X) (G.componentComplFunctor.obj L)) →
        (fun (X : Type u) ↦ X) (G.componentComplFunctor.obj K))
    (G.componentComplMk (K := (↑(Opposite.unop L) : Set V)) vnL) =
  G.componentComplMk (K := (↑(Opposite.unop K) : Set V)) sorry
Tactic: rw [← sec h, hs]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (ComponentCompl.supp (K := (↑(Opposite.unop K) : Set V)) C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K
have simp : (∀ (L : Finset V) (h : Opposite.unop K ⊆ L),
    ∃ (D : G.ComponentCompl (↑L : Set V)),
      ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D = C) ↔
  ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K),
    ∃ (y : G.componentComplFunctor.obj i),
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑(Opposite.unop i) : Set V)) sorry) :
            (a : G.componentComplFunctor.obj i) → G.componentComplFunctor.obj K)
          y =
        C
Tactic: simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter,
    Set.mem_range, componentComplFunctor_map]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Properties (goal)
Goal:
V : Type
G : SimpleGraph V
inst : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property : s ∈ G.end
⊢ False
have intro : ∀ (val : Fintype V), False
Tactic: cases nonempty_fintype V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Properties (goal)
Goal:
V : Type
G : SimpleGraph V
inst : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property : s ∈ G.end
val : Fintype V
⊢ False
have intro : ∀ (v : V) (h : v ∈ (↑(s (Opposite.op Finset.univ)) : Set V)), False
Tactic: obtain ⟨v, h⟩ := (s <| Opposite.op Finset.univ).nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Properties (goal)
Goal:
V : Type
G : SimpleGraph V
e : (↑G.end : Type)
K : (Finset V)ᵒᵖ
⊢ (ComponentCompl.supp (K := (↑(Opposite.unop K) : Set V))
      ((↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K)).Infinite
have refine : ∀ (L : Finset V) (h : Opposite.unop K ⊆ L),
  ∃ (D : G.ComponentCompl (↑L : Set V)),
    ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D =
      (↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K
Tactic: refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Properties (hypothesis)
Goal:
V : Type
G : SimpleGraph V
e : (↑G.end : Type)
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ L
⊢ ∃ (D : G.ComponentCompl (↑L : Set V)),
    ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D =
      (↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K
have h₁ : Opposite.unop K ⊆ Opposite.unop (Opposite.op L)
Tactic: change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
⊢ (∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p) ↔ ∃ (G : SimpleGraph V), p G
have refine : (∃ (G : SimpleGraph V), p G) →
  ∀ (G : SimpleGraph V) (hp : p G), ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p
Tactic: refine ⟨fun ⟨_, _, h⟩ ↦ ⟨_, h.1⟩, fun ⟨G, hp⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
⊢ ∃ (x : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x ∧
      ∀ (x' : SimpleGraph V),
        Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #x.edgeFinset
have apply : Finset.Nonempty.{u_1} (α := SimpleGraph V) {G : SimpleGraph V | p G}
Tactic: apply exists_max_image { G | p G } (#·.edgeFinset)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
w : SimpleGraph V
⊢ Finset.Nonempty.{u_1} (α := SimpleGraph V) {G : SimpleGraph V | p G}
have h : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G
Tactic: use G, by simpa using hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
⊢ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p
have obtain : ∀ (G' : SimpleGraph V) (hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G')
  (h :
    ∀ (x' : SimpleGraph V),
      Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset),
  ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p
Tactic: obtain ⟨G', hp', h⟩ := by
    apply exists_max_image { G | p G } (#·.edgeFinset)
    use G, by simpa using hp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h_1 : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
G' : SimpleGraph V
hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G'
h :
  ∀ (x' : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset
⊢ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p
have h₁ : G'.IsExtremal p
Tactic: use G', inferInstanceAs (DecidableRel G'.Adj)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ extremalNumber n H = sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset
have 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)
Tactic: rw [extremalNumber, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ 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)
have 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)
Tactic: and_intros
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: and_intros
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ 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)
have 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)
Tactic: replace e := e.symm
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ 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)
have 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)
Tactic: on_goal 1 =>
    replace e := e.symm
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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'
have rw : Membership.mem (γ := Finset (SimpleGraph V)) univ G' ∧ H.Free G
Tactic: rw [mem_filter, ← free_congr .refl (.map e G)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (hypothesis)
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
⊢ #G.edgeFinset ≤ sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset
have h' : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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'
⊢ #G.edgeFinset ≤ sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset
have 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
Tactic: rw [Iso.card_edgeFinset_eq (.map e G)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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'
have rw : Membership.mem (γ := Finset (SimpleGraph (Fin n))) univ G' ∧ H.Free G
Tactic: rw [mem_filter, ← free_congr .refl (.map e G)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (hypothesis)
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
⊢ #G.edgeFinset ≤ sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset
have h' : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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'
⊢ #G.edgeFinset ≤ sup {G : SimpleGraph (Fin n) | H.Free G} fun (x : SimpleGraph (Fin n)) ↦ #x.edgeFinset
have 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
Tactic: rw [Iso.card_edgeFinset_eq (.map e G)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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 ≤ extremalNumber (Fintype.card V) H
have rw : #G.edgeFinset ≤ sup {G : SimpleGraph V | H.Free G} fun (x : SimpleGraph V) ↦ #x.edgeFinset
Tactic: rw [extremalNumber_of_fintypeCard_eq rfl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ H ⊑ G
have contrapose : ∀ (h : ¬H ⊑ G), ¬extremalNumber (Fintype.card V) H < #G.edgeFinset
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ ¬extremalNumber (Fintype.card V) H < #G.edgeFinset
have push : #G.edgeFinset ≤ extremalNumber (Fintype.card V) H
Tactic: push Not
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
⊢ extremalNumber (Fintype.card V) H ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_1 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ m
have 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
Tactic: simp_rw [extremalNumber_of_fintypeCard_eq rfl, Finset.sup_le_iff, mem_filter_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
V : Type u_1
W : Type u_2
inst : Fintype V
H : SimpleGraph W
m : ℕ
⊢ m < extremalNumber (Fintype.card V) H ↔ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < #G.edgeFinset
have simp_rw : (∃ (b : SimpleGraph V), H.Free b ∧ m < #b.edgeFinset) ↔
  ∃ (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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) : R) ≤ m ↔
    ∀ ⦃G : SimpleGraph V⦄ [inst_4 : DecidableRel G.Adj], H.Free G → (↑(#G.edgeFinset) : R) ≤ m
have simp_rw : extremalNumber (Fintype.card V) H ≤ ⌊m⌋₊ ↔
  ∀ ⦃G : SimpleGraph V⦄ [inst_4 : DecidableRel G.Adj], H.Free G → #G.edgeFinset ≤ ⌊m⌋₊
Tactic: simp_rw [← Nat.le_floor_iff h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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) : R) ↔
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ m < (↑(#G.edgeFinset) : R)
have simp_rw : ⌊m⌋₊ < extremalNumber (Fintype.card V) H ↔
  ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), H.Free G ∧ ⌊m⌋₊ < #G.edgeFinset
Tactic: simp_rw [← Nat.floor_lt h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
n : ℕ
W : Type u_2
H : SimpleGraph W
W' : Type u_4
H' : SimpleGraph W'
h : H' ⊑ H
⊢ extremalNumber n H' ≤ extremalNumber n H
have rw : ∀ ⦃G : SimpleGraph (Fin n)⦄ [inst : DecidableRel G.Adj],
  H'.Free G → #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
Tactic: rw [← Fintype.card_fin n, extremalNumber_le_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
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
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n)) H
have contrapose! : ∀ (h' : extremalNumber (Fintype.card (Fin n)) H < #G.edgeFinset), H' ⊑ G
Tactic: contrapose! h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Basic (goal)
Goal:
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h : n₁ = n₂
e : H₁ ≃g H₂
⊢ extremalNumber n₁ H₁ = extremalNumber n₂ H₂
have rw : extremalNumber n₂ H₁ ≤ extremalNumber n₂ H₂ ∧ extremalNumber n₂ H₂ ≤ extremalNumber n₂ H₁
Tactic: rw [h, le_antisymm_iff]