awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).stirlingFirst n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₃ : n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₄ : n + 1 + (n + 1).choose 2 = (n + 1).choose 1 + (n + 1).choose (Nat.succ 1)
⊢ (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
have succ₅ : n + 1 + (n + 1).choose 2 = n + 1 + (n + 1).choose (Nat.succ 1)
Tactic: rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
⊢ (n + 1).stirlingFirst n = (n + 1).choose 2
have zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2
Tactic: induction n with
  | zero => simp only [zero_add, stirlingFirst_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2
⊢ (n + 1).stirlingFirst n = (n + 1).choose 2
have succ : ∀ (n : ℕ) (ih : (n + 1).stirlingFirst n = (n + 1).choose 2), (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
Tactic: induction n with
  | zero => simp only [zero_add, stirlingFirst_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
⊢ (n + 1 + 1).stirlingFirst 1 = (n + 1)!
have succ : (n + 1) * n ! + 0 = (n + 1)!
Tactic: rw [stirlingFirst_succ_succ, zero_add, hn, stirlingFirst_succ_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
⊢ (n + 1).stirlingFirst 1 = n !
have zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 1 = 0!
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    rw [stirlingFirst_succ_succ, zero_add, hn, stirlingFirst_succ_zero]
    simp [Nat.factorial_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 1 = 0!
⊢ (n + 1).stirlingFirst 1 = n !
have succ : ∀ (n : ℕ) (hn : (n + 1).stirlingFirst 1 = n !), (n + 1 + 1).stirlingFirst 1 = (n + 1)!
Tactic: induction n with
  | zero => rfl
  | succ n hn =>
    rw [stirlingFirst_succ_succ, zero_add, hn, stirlingFirst_succ_zero]
    simp [Nat.factorial_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hk : k ≠ 0
⊢ (n + 1).stirlingSecond k = k * n.stirlingSecond k + n.stirlingSecond (k - 1)
have obtain : ∀ (l : ℕ) (hk : l + succ 0 ≠ 0),
  (n + 1).stirlingSecond (l + succ 0) = (l + succ 0) * n.stirlingSecond (l + succ 0) + n.stirlingSecond (l + succ 0 - 1)
Tactic: obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hk)
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hn : n ≠ 0
⊢ n.stirlingSecond (k + 1) = (k + 1) * (n - 1).stirlingSecond (k + 1) + (n - 1).stirlingSecond k
have obtain : ∀ (l : ℕ) (hn : l + succ 0 ≠ 0),
  (l + succ 0).stirlingSecond (k + 1) =
    (k + 1) * (l + succ 0 - 1).stirlingSecond (k + 1) + (l + succ 0 - 1).stirlingSecond k
Tactic: obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hn)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
h : 0 < n + 1
⊢ stirlingSecond 0 (n + 1) = 0
have rw : Eq (α := ℕ) 0 0
Tactic: rw [stirlingSecond]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
⊢ n.stirlingSecond n = 1
have zero : stirlingSecond 0 0 = 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
zero : stirlingSecond 0 0 = 1
⊢ n.stirlingSecond n = 1
have succ : ∀ (n : ℕ), n.stirlingSecond n = 1 → (n + 1).stirlingSecond (n + 1) = 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
⊢ (n + 1 + 1).stirlingSecond 1 = 1
have succ : HAdd.hAdd (α := ℕ) 0 1 * (n + 1).stirlingSecond (HAdd.hAdd (α := ℕ) 0 1) + (n + 1).stirlingSecond 0 = 1
Tactic: rw [stirlingSecond, stirlingSecond_succ_zero, ih]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
succ : HAdd.hAdd (α := ℕ) 0 1 * (n + 1).stirlingSecond (HAdd.hAdd (α := ℕ) 0 1) + (n + 1).stirlingSecond 0 = 1
⊢ (n + 1 + 1).stirlingSecond 1 = 1
have succ₁ : HAdd.hAdd (α := ℕ) 0 1 * (n + 1).stirlingSecond (HAdd.hAdd (α := ℕ) 0 1) + 0 = 1
Tactic: rw [stirlingSecond, stirlingSecond_succ_zero, ih]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
succ : HAdd.hAdd (α := ℕ) 0 1 * (n + 1).stirlingSecond (HAdd.hAdd (α := ℕ) 0 1) + (n + 1).stirlingSecond 0 = 1
succ₁ : HAdd.hAdd (α := ℕ) 0 1 * (n + 1).stirlingSecond (HAdd.hAdd (α := ℕ) 0 1) + 0 = 1
⊢ (n + 1 + 1).stirlingSecond 1 = 1
have succ₂ : HAdd.hAdd (α := ℕ) 0 1 * 1 + 0 = 1
Tactic: rw [stirlingSecond, stirlingSecond_succ_zero, ih]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
⊢ (n + 1).stirlingSecond 1 = 1
have zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 1 = 1
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [stirlingSecond, stirlingSecond_succ_zero, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 1 = 1
⊢ (n + 1).stirlingSecond 1 = 1
have succ : ∀ (n : ℕ) (ih : (n + 1).stirlingSecond 1 = 1), (n + 1 + 1).stirlingSecond 1 = 1
Tactic: induction n with
  | zero => rfl
  | succ n ih => rw [stirlingSecond, stirlingSecond_succ_zero, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
have succ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2
Tactic: rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
have succ₁ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
Tactic: rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
have succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
Tactic: rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
have succ₃ : n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
Tactic: rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₃ : n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
have succ₄ : n + 1 + (n + 1).choose 2 = (n + 1).choose 1 + (n + 1).choose (Nat.succ 1)
Tactic: rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₃ : n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₄ : n + 1 + (n + 1).choose 2 = (n + 1).choose 1 + (n + 1).choose (Nat.succ 1)
⊢ (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
have succ₅ : n + 1 + (n + 1).choose 2 = n + 1 + (n + 1).choose (Nat.succ 1)
Tactic: rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
⊢ (n + 1).stirlingSecond n = (n + 1).choose 2
have zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2
Tactic: induction n with
  | zero => simp only [zero_add, stirlingSecond_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2
⊢ (n + 1).stirlingSecond n = (n + 1).choose 2
have succ : ∀ (n : ℕ) (ih : (n + 1).stirlingSecond n = (n + 1).choose 2), (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2
Tactic: induction n with
  | zero => simp only [zero_add, stirlingSecond_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β
have refine : ∀ (n : ℕ),
  (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) →
    ∃ (G : SimpleGraph β) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
Tactic: refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
G : SimpleGraph α
w : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∃ (G_1 : SimpleGraph β) (x : DecidableRel G_1.Adj), #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear
have refine : Finset.card.{u_2} (α := Finset β) (cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) 3) = #(G.cliqueFinset 3)
Tactic: refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
G : SimpleGraph α
w : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ Finset.card.{u_2} (α := Finset β) (cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) 3) = #(G.cliqueFinset 3)
have rw : Ne (α := ℕ) 3 1
Tactic: rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β
have refine : ∀ (n : ℕ),
  (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) →
    ∃ (G : SimpleGraph β) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
Tactic: classical
  refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
  rintro n ⟨G, _, rfl, hG⟩
  refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
  rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
  decide
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
refine :
  ∀ (n : ℕ),
    (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) →
      ∃ (G : SimpleGraph β) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β
have refine₁ : ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear),
  ∃ (G_1 : SimpleGraph β) (x : DecidableRel G_1.Adj), #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear
Tactic: classical
  refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
  rintro n ⟨G, _, rfl, hG⟩
  refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
  rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
  decide
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
refine :
  ∀ (n : ℕ),
    (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) →
      ∃ (G : SimpleGraph β) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
refine₁ :
  ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear),
    ∃ (G_1 : SimpleGraph β) (x : DecidableRel G_1.Adj), #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β
have refine₂ : ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear),
  Finset.card.{u_2} (α := Finset β) (cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) 3) = #(G.cliqueFinset 3)
Tactic: classical
  refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
  rintro n ⟨G, _, rfl, hG⟩
  refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
  rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
  decide
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : Fintype α
inst_3 : Fintype β
f : α ↪ β
refine :
  ∀ (n : ℕ),
    (∃ (G : SimpleGraph α) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear) →
      ∃ (G : SimpleGraph β) (x : DecidableRel G.Adj), #(G.cliqueFinset 3) = n ∧ G.LocallyLinear
refine₁ :
  ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear),
    ∃ (G_1 : SimpleGraph β) (x : DecidableRel G_1.Adj), #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear
refine₂ :
  ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear),
    Finset.card.{u_2} (α := Finset β) (cliqueFinset (SimpleGraph.map (⇑f : (a : α) → β) G) 3) = #(G.cliqueFinset 3)
⊢ ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β
have refine₃ : ∀ (G : SimpleGraph α) (w : DecidableRel G.Adj) (hG : G.LocallyLinear), Ne (α := ℕ) 3 1
Tactic: classical
  refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
  rintro n ⟨G, _, rfl, hG⟩
  refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
  rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
  decide
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ (Fintype.card (Fin n)).choose 3 = n.choose 3
have rw : n.choose 3 = n.choose 3
Tactic: rw [Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s_1 : Finset α
x_1 : α × α × α
s : Finset α
x a y b : α
h :
  Eq.{u_1 + 1} (α := α × α × α) ((fun (xa : α × α) ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)) (x, a))
    ((fun (xa : α × α) ↦ (xa.1, xa.1 + xa.2, xa.1 + 2 * xa.2)) (y, b))
⊢ (x, a) = (y, b)
have h₁ : x = y ∧ x + a = y + b ∧ x + 2 * a = y + 2 * b
Tactic: simp only [Prod.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s_1 : Finset α
x_1 : α × α × α
s : Finset α
x a y b : α
h : x = y ∧ x + a = y + b ∧ x + 2 * a = y + 2 * b
⊢ (x, a) = (y, b)
have obtain : ∀ (h : x = x ∧ x + a = x + b ∧ x + 2 * a = x + 2 * b), (x, a) = (x, b)
Tactic: obtain rfl := h.1
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s_1 : Finset α
x_1 : α × α × α
s : Finset α
x a b : α
h : x = x ∧ x + a = x + b ∧ x + 2 * a = x + 2 * b
⊢ (x, a) = (x, b)
have obtain : ∀ (h : x = x ∧ x + a = x + a ∧ x + 2 * a = x + 2 * a), (x, a) = (x, a)
Tactic: obtain rfl := add_right_injective _ h.2.1
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
⊢ ∀ ⦃a a' b b' c c' : α⦄,
    (a', b, c) ∈ triangleIndices s →
      (a, b', c) ∈ triangleIndices s → (a, b, c') ∈ triangleIndices s → a = a' ∨ b = b' ∨ c = c'
have simp : ∀ ⦃a a' b b' c c' : α⦄ (x x_1 : α),
  x_1 ∈ s →
    x = a' →
      x + x_1 = b →
        x + 2 * x_1 = c →
          ∀ (x x_2 : α),
            x_2 ∈ s →
              x = a →
                x + x_2 = b' →
                  x + 2 * x_2 = c →
                    ∀ (x x_3 : α), x_3 ∈ s → x = a → x + x_3 = b → x + 2 * x_3 = c' → a = a' ∨ b = b' ∨ c = c'
Tactic: simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c
have this : a + c = b + b
Tactic: have : a + c = b + b := by linear_combination h₁.symm - h₂.symm
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
hs : ThreeAPFree (↑s : Set α)
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
this : a + c = b + b
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c
have obtain : ∀ (hb : a ∈ s) (h₁ : d' + 2 * a = d + 2 * a) (this : a + c = a + a), d' = d ∨ d + a = d' + a ∨ d + 2 * a = d' + 2 * c
Tactic: obtain rfl := hs ha hb hc this
Cleared hypotheses: b, hb, h₁, this
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
⊢ ∀ ⦃a b c a' : α⦄, (a, b, c) ∈ triangleIndices s → (a', b, c) ∈ triangleIndices s → a = a'
have simp : ∀ ⦃a b c a' : α⦄ (x x_1 : α),
  x_1 ∈ s →
    x = a → x + x_1 = b → x + 2 * x_1 = c → ∀ (x x_2 : α), x_2 ∈ s → x = a' → x + x_2 = b → x + 2 * x_2 = c → a = a'
Tactic: simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
⊢ ∀ ⦃a b c b' : α⦄, (a, b, c) ∈ triangleIndices s → (a, b', c) ∈ triangleIndices s → b = b'
have simp : ∀ ⦃a b c b' : α⦄ (x x_1 : α),
  x_1 ∈ s →
    x = a → x + x_1 = b → x + 2 * x_1 = c → ∀ (x x_2 : α), x_2 ∈ s → x = a → x + x_2 = b' → x + 2 * x_2 = c → b = b'
Tactic: simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : CommRing α
s : Finset α
x : α × α × α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
⊢ ∀ ⦃a b c c' : α⦄, (a, b, c) ∈ triangleIndices s → (a, b, c') ∈ triangleIndices s → c = c'
have simp : ∀ ⦃a b c c' : α⦄ (x x_1 : α),
  x_1 ∈ s →
    x = a → x + x_1 = b → x + 2 * x_1 = c → ∀ (x x_2 : α), x_2 ∈ s → x = a → x + x_2 = b → x + 2 * x_2 = c' → c = c'
Tactic: simp only [mem_triangleIndices, Prod.mk_inj, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
inst_3 : DecidableEq α
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s
have this : NoAccidental (triangleIndices s)
Tactic: haveI := noAccidental hs
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
inst_3 : DecidableEq α
this : NoAccidental (triangleIndices s)
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s
have rw : 3 * #((graph (triangleIndices s)).cliqueFinset 3) = 3 * Fintype.card α * #s
Tactic: rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
inst_3 : DecidableEq α
this : NoAccidental (triangleIndices s)
rw : 3 * #((graph (triangleIndices s)).cliqueFinset 3) = 3 * Fintype.card α * #s
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s
have rw₁ : 3 * #(triangleIndices s) = 3 * Fintype.card α * #s
Tactic: rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
inst_3 : DecidableEq α
this : NoAccidental (triangleIndices s)
rw : 3 * #((graph (triangleIndices s)).cliqueFinset 3) = 3 * Fintype.card α * #s
rw₁ : 3 * #(triangleIndices s) = 3 * Fintype.card α * #s
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s
have rw₂ : 3 * (Fintype.card α * #s) = 3 * Fintype.card α * #s
Tactic: rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]