awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
this :
  ¬G.Adj (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V)
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)
⊢ (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b ⋯)) :
          ℕ) %
        r ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        min (Fintype.card V) r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        min (Fintype.card V) r
have map_rel_iff' : ∀ (c : r ≤ Fintype.card V),
  (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a sorry)) :
          ℕ) %
        r =
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b sorry)) :
          ℕ) %
        r ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a sorry)) :
          ℕ) %
        min (Fintype.card V) r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b sorry)) :
          ℕ) %
        min (Fintype.card V) r
Tactic: rcases le_or_gt r (card V) with c | c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
this :
  ¬G.Adj (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V)
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)
c : r ≤ Fintype.card V
⊢ (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b ⋯)) :
          ℕ) %
        r ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        min (Fintype.card V) r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        min (Fintype.card V) r
have map_rel_iff' : (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
            (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a sorry)) :
        ℕ) %
      r =
    (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
            (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b sorry)) :
        ℕ) %
      r ↔
  (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a sorry)) : ℕ) %
      r =
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b sorry)) :
        ℕ) %
      r
Tactic: rw [min_eq_right c]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (hypothesis)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
this :
  ¬G.Adj (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V)
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)
c : Fintype.card V < r
⊢ (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b ⋯)) :
          ℕ) %
        r ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        min (Fintype.card V) r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        min (Fintype.card V) r
have lc : ∀ (x : V),
  (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) x sorry)) : ℕ) <
    Fintype.card V
Tactic: have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ)
zp :
  ∀ (a b : ↥univ),
    Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
      (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
        (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)
a b : V
this :
  ¬G.Adj (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯) : V)
        (↑(Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯) : V) ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition) =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        #(Finpartition.parts h.finpartition)
c : Fintype.card V < r
lc :
  ∀ (x : V),
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) x ⋯)) :
        ℕ) <
      Fintype.card V
⊢ (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a ⋯)) :
          ℕ) %
        r =
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b ⋯)) :
          ℕ) %
        r ↔
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a ⋯)) :
          ℕ) %
        min (Fintype.card V) r =
      (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b ⋯)) :
          ℕ) %
        min (Fintype.card V) r
have map_rel_iff' : (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
            (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a sorry)) :
        ℕ) %
      r =
    (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
            (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b sorry)) :
        ℕ) %
      r ↔
  (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) a sorry)) : ℕ) %
      r =
    (↑((zm : (a : ↥univ) → Fin #univ) (Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Finset V) univ x) b sorry)) :
        ℕ) %
      r
Tactic: rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
have obtain : ∀ (zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ))
  (zp :
    ∀ (a b : ↥univ),
      Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
        (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
          (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)),
  Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
Tactic: classical
  obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
  use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
  intro a b
  simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
  have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
  rw [← h.not_adj_iff_part_eq] at this
  rw [← not_iff_not, not_ne_iff, this, card_parts]
  rcases le_or_gt r (card V) with c | c
  · rw [min_eq_right c]; rfl
  · have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
obtain :
  ∀ (zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ))
    (zp :
      ∀ (a b : ↥univ),
        Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
          (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
            (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)),
    Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
have map_rel_iff' : ∀ (zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ))
  (zp :
    ∀ (a b : ↥univ),
      Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
        (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
          (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition))
  {a b : V},
  Adj (V := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)
      ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) sorry)) zm :
          (a : V) → Fin (Fintype.card V))
        a)
      ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) sorry)) zm :
          (a : V) → Fin (Fintype.card V))
        b) ↔
    G.Adj a b
Tactic: classical
  obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
  use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
  intro a b
  simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
  have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
  rw [← h.not_adj_iff_part_eq] at this
  rw [← not_iff_not, not_ne_iff, this, card_parts]
  rcases le_or_gt r (card V) with c | c
  · rw [min_eq_right c]; rfl
  · have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
obtain :
  ∀ (zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ))
    (zp :
      ∀ (a b : ↥univ),
        Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
          (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
            (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition)),
    Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
map_rel_iff' map_rel_iff'₁ :
  ∀ (zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ))
    (zp :
      ∀ (a b : ↥univ),
        Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
          (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
            (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition))
    {a b : V},
    Adj (V := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)
        ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) ⋯)) zm :
            (a : V) → Fin (Fintype.card V))
          a)
        ((Equiv.trans (Equiv.symm (Equiv.subtypeUnivEquiv (p := Membership.mem (γ := Finset V) univ) ⋯)) zm :
            (a : V) → Fin (Fintype.card V))
          b) ↔
      G.Adj a b
⊢ Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r))
have map_rel_iff'₂ : ∀ (zm : ↥univ ≃ Fin (Finset.card.{u_1} (α := V) univ))
  (zp :
    ∀ (a b : ↥univ),
      Finpartition.part h.finpartition (↑a : V) = Finpartition.part h.finpartition (↑b : V) ↔
        (↑((zm : (a : ↥univ) → Fin #univ) a) : ℕ) % #(Finpartition.parts h.finpartition) =
          (↑((zm : (a : ↥univ) → Fin #univ) b) : ℕ) % #(Finpartition.parts h.finpartition))
  {a b : V},
  (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) a sorry)) :
          ℕ) %
        r ≠
      (↑((zm : (a : Subtype (Membership.mem univ)) → Fin (Fintype.card V))
              (Subtype.mk (p := Membership.mem (γ := Finset V) univ) b sorry)) :
          ℕ) %
        r ↔
    G.Adj a b
Tactic: classical
  obtain ⟨zm, zp⟩ := h.isEquipartition.exists_partPreservingEquiv
  use (Equiv.subtypeUnivEquiv mem_univ).symm.trans zm
  intro a b
  simp_rw [turanGraph_adj, Equiv.trans_apply, Equiv.subtypeUnivEquiv_symm_apply]
  have := zp ⟨a, mem_univ a⟩ ⟨b, mem_univ b⟩
  rw [← h.not_adj_iff_part_eq] at this
  rw [← not_iff_not, not_ne_iff, this, card_parts]
  rcases le_or_gt r (card V) with c | c
  · rw [min_eq_right c]; rfl
  · have lc : ∀ x, zm ⟨x, _⟩ < card V := fun x ↦ (zm ⟨x, mem_univ x⟩).2
    rw [min_eq_left c.le, Nat.mod_eq_of_lt (lc a), Nat.mod_eq_of_lt (lc b),
      ← Nat.mod_eq_of_lt ((lc a).trans c), ← Nat.mod_eq_of_lt ((lc b).trans c)]; rfl
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
⊢ G.IsTuranMaximal r
have obtain : ∀ (J : SimpleGraph V) (w : DecidableRel J.Adj) (j : J.IsTuranMaximal r), G.IsTuranMaximal r
Tactic: obtain ⟨J, _, j⟩ := exists_isTuranMaximal (V := V) hr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w : DecidableRel J.Adj
j : J.IsTuranMaximal r
⊢ G.IsTuranMaximal r
have obtain : ∀ (g : J.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)), G.IsTuranMaximal r
Tactic: obtain ⟨g⟩ := j.nonempty_iso_turanGraph
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) r)
⊢ G.IsTuranMaximal r
have rw : ∀ (g : J ≃g turanGraph n r), G.IsTuranMaximal r
Tactic: rw [f.card_eq, Fintype.card_fin] at g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph n r
⊢ G.IsTuranMaximal r
have left : (fun (x : SimpleGraph V) ↦ x.CliqueFree (r + 1)) G
Tactic: use (turanGraph_cliqueFree (n := n) hr).comap f.isContained,
    fun H _ cf ↦ (f.symm.comp g).card_edgeFinset_eq ▸ j.2 cf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
n r : ℕ
f : G ≃g turanGraph n r
hr : 0 < r
J : SimpleGraph V
w : DecidableRel J.Adj
j : J.IsTuranMaximal r
g : J ≃g turanGraph n r
left : (fun (x : SimpleGraph V) ↦ x.CliqueFree (r + 1)) G
⊢ G.IsTuranMaximal r
have right : ∀ ⦃G' : SimpleGraph V⦄ [inst_2 : DecidableRel G'.Adj],
  (fun (x : SimpleGraph V) ↦ x.CliqueFree (r + 1)) G' → #G'.edgeFinset ≤ #G.edgeFinset
Tactic: use (turanGraph_cliqueFree (n := n) hr).comap f.isContained,
    fun H _ cf ↦ (f.symm.comp g).card_edgeFinset_eq ▸ j.2 cf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
⊢ G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔ G.IsTuranMaximal (Fintype.card α - 1)
have simp_rw : G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔ G.IsExtremal fun (x : SimpleGraph V) ↦ x.CliqueFree (Fintype.card α - 1 + 1)
Tactic: simp_rw [IsTuranMaximal, IsExtremal,
    Nat.sub_one_add_one Fintype.card_ne_zero, cliqueFree_iff_top_free]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
simp_rw :
  G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔
    G.IsExtremal fun (x : SimpleGraph V) ↦ x.CliqueFree (Fintype.card α - 1 + 1)
⊢ G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔ G.IsTuranMaximal (Fintype.card α - 1)
have simp_rw₁ : (Free.{u_2, u_1} (α := α) ⊤ G ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
      Free.{u_2, u_1} (α := α) ⊤ G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
  G.CliqueFree (Fintype.card α - 1 + 1) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
      G'.CliqueFree (Fintype.card α - 1 + 1) → #G'.edgeFinset ≤ #G.edgeFinset
Tactic: simp_rw [IsTuranMaximal, IsExtremal,
    Nat.sub_one_add_one Fintype.card_ne_zero, cliqueFree_iff_top_free]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
simp_rw :
  G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔
    G.IsExtremal fun (x : SimpleGraph V) ↦ x.CliqueFree (Fintype.card α - 1 + 1)
simp_rw₁ :
  (Free.{u_2, u_1} (α := α) ⊤ G ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
        Free.{u_2, u_1} (α := α) ⊤ G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
    G.CliqueFree (Fintype.card α - 1 + 1) ∧
      ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
        G'.CliqueFree (Fintype.card α - 1 + 1) → #G'.edgeFinset ≤ #G.edgeFinset
⊢ G.IsExtremal (Free.{u_2, u_1} (α := α) ⊤) ↔ G.IsTuranMaximal (Fintype.card α - 1)
have simp_rw₂ : (Free.{u_2, u_1} (α := α) ⊤ G ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
      Free.{u_2, u_1} (α := α) ⊤ G' → #G'.edgeFinset ≤ #G.edgeFinset) ↔
  G.CliqueFree (Fintype.card α) ∧
    ∀ ⦃G' : SimpleGraph V⦄ [inst_4 : DecidableRel G'.Adj],
      G'.CliqueFree (Fintype.card α) → #G'.edgeFinset ≤ #G.edgeFinset
Tactic: simp_rw [IsTuranMaximal, IsExtremal,
    Nat.sub_one_add_one Fintype.card_ne_zero, cliqueFree_iff_top_free]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
⊢ (turanGraph n (Fintype.card α - 1)).IsExtremal (Free.{u_2, 0} (α := α) ⊤)
have rw : (turanGraph n (Fintype.card α - 1)).IsTuranMaximal (Fintype.card α - 1)
Tactic: rw [isExtremal_top_free_iff_isTuranMaximal]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
| extremalNumber.{u_2} n (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset
have enter : n
Tactic: enter [1, 1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
| n
have rw : Fintype.card (Fin n)
Tactic: rw [← Fintype.card_fin n]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
| extremalNumber.{u_2} n (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset
have enter : Fintype.card (Fin n)
Tactic: enter [1, 1]
    rw [← Fintype.card_fin n]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
n : ℕ
α : Type u_2
inst : Fintype α
inst_1 : Nontrivial α
⊢ extremalNumber.{u_2} n (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset
have conv : extremalNumber.{u_2} (Fintype.card (Fin n)) (W := α) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset
Tactic: conv =>
    enter [1, 1]
    rw [← Fintype.card_fin n]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.Turan (goal)
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
α : Type u_2
inst_2 : Fintype α
inst_3 : Nontrivial α
⊢ Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
    Nonempty.{max 1 (u_1 + 1)} (G.Iso (W := Fin (Fintype.card V)) (turanGraph (Fintype.card V) (Fintype.card α - 1)))
have rw : Free.{u_2, u_1} (α := α) ⊤ G ∧ #G.edgeFinset = extremalNumber.{u_2} (Fintype.card V) (W := α) ⊤ ↔
  G.IsTuranMaximal (Fintype.card α - 1)
Tactic: rw [← isTuranMaximal_iff_nonempty_iso_turanGraph (Nat.sub_pos_iff_lt.mpr one_lt_card),
    ← isExtremal_top_free_iff_isTuranMaximal, isExtremal_free_iff]