text:
import data.set.basic tactic.interactive
import data.list.basic
import data.fintype

@[derive decidable_eq]
inductive square
| vampire : square
| ghost : square
| zombie : square

namespace square

instance : fintype square := {
  elems := {vampire,ghost,zombie},
  complete := λ x,by cases x;exact dec_trivial
}

definition nomirror : square → ℕ
| vampire := 1
| ghost := 0
| zombie := 1

definition mirror : square → ℕ
| vampire := 0
| ghost := 1
| zombie := 1

end square

open square

variables a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : square

/- the 16 equations -/
definition e₁ := a₁.nomirror + a₃.nomirror + a₆.nomirror + a₈.nomirror = 3
definition e₂ := a₁.mirror = 0
definition e₃ := a₂.nomirror + a₄.nomirror + a₄.mirror + a₅.mirror = 2
definition e₄ := 0 = 0
definition e₅ := 0 = 0
definition e₆ := a₅.nomirror + a₄.nomirror + a₄.mirror + a₂.mirror = 3
definition e₇ := a₇.nomirror + a₇.mirror + a₅.mirror + a₂.mirror + a₃.mirror = 3
definition e₈ := 0 = 0
definition e₉ := 0 = 0
definition e₁₀ := a₉.mirror + a₈.mirror = 1
definition e₁₁ := a₉.nomirror + a₆.mirror = 2
definition e₁₂ := a₈.nomirror + a₆.nomirror + a₃.nomirror + a₁.nomirror = 3
definition e₁₃ := a₈.nomirror + a₉.nomirror = 2
definition e₁₄ := a₆.nomirror + a₉.mirror = 1
definition e₁₅ := a₃.nomirror + a₂.mirror + a₅.mirror + a₇.mirror + a₇.mirror = 3
definition e₁₆ := a₁.nomirror = 1

definition is_solved := (e₁ a₁ a₃ a₆ a₈) ∧ (e₂ a₁) ∧ (e₃ a₂ a₄ a₅) ∧ (e₄) ∧ (e₅) ∧ (e₆ a₂ a₄ a₅) ∧ (e₇ a₂ a₃ a₅ a₇)
  ∧ (e₈) ∧ (e₉) ∧ (e₁₀ a₈ a₉) ∧ (e₁₁ a₆ a₉) ∧ (e₁₂ a₁ a₃ a₆ a₈)
  ∧ (e₁₃ a₈ a₉) ∧ (e₁₄ a₆ a₉) ∧ (e₁₅ a₂ a₃ a₅ a₇) ∧ (e₁₆ a₁)
  ∧ list.length (list.filter (λ a, a = vampire) [a₁,a₂,a₃,a₄,a₅,a₆,a₇,a₈,a₉]) = 3
  ∧ list.length (list.filter (λ a, a = ghost) [a₁,a₂,a₃,a₄,a₅,a₆,a₇,a₈,a₉]) = 3
  ∧ list.length (list.filter (λ a, a = zombie) [a₁,a₂,a₃,a₄,a₅,a₆,a₇,a₈,a₉]) = 3

lemma not_vampire (a : square) : ¬ (a = vampire) → a.mirror = 1 :=
begin
  intro H,
  cases a,exfalso,apply H,refl,refl,refl
end

lemma not_ghost (a : square) : ¬ (a = ghost) → a.nomirror = 1 :=
begin
  intro H,
  cases a,refl,exfalso,apply H,refl,refl
end

lemma not_zombie (a : square) : ¬ (a = zombie) → a.mirror + a.nomirror = 1 :=
begin
  intro H,
  cases a,refl,refl,exfalso,apply H,refl,
end

lemma square_1_is_vampire (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : a₁ = vampire :=
begin
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  cases a₁,
    refl,
    cases h₂,
    cases h₂
end

lemma square_2_not_vampire (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : ¬ a₂ = vampire :=
begin
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  intro H2,
  rw H2 at h₃,
  rw H2 at h₆,
  cases a₄;cases a₅;cases h₃;cases h₆
end

lemma square_4_not_zombie (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : ¬ a₄ = zombie :=
begin
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  intro H4,
  rw H4 at h₃,
  rw H4 at h₆,
  cases a₂;cases a₅;cases h₃;cases h₆,
end

lemma square_5_not_ghost (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : ¬ a₅ = ghost :=
begin
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  intro H5,
  rw H5 at h₃,
  rw H5 at h₆,
  cases a₂;cases a₄;cases h₃;cases h₆,
end

lemma square_6_not_vampire (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : ¬ a₆ = vampire :=
begin
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  intro H6,
  rw H6 at h₁₁,
  cases a₉;cases h₁₁,
end

lemma square_8_not_ghost (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : ¬ a₈ = ghost :=
begin
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  intro H8,
  rw H8 at h₁₃,
  cases a₉;cases h₁₃,
end

lemma square_9_not_ghost (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : ¬ a₉ = ghost :=
begin
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  intro H9,
  rw H9 at h₁₁,
  cases a₆;cases h₁₁,
end

lemma what_i_know (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) :
a₁ = vampire
∧  mirror a₂ = 1
∧  mirror a₄ + nomirror a₄ = 1
∧ nomirror a₅ = 1
∧ mirror a₆ = 1
∧ nomirror a₈ = 1
∧ nomirror a₉ = 1
 :=
begin
  have H1 : a₁ = vampire := square_1_is_vampire a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  have H2 : ¬ a₂ = vampire := square_2_not_vampire a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  have H4 : ¬ a₄ = zombie := square_4_not_zombie a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  have H5 : ¬ a₅ = ghost := square_5_not_ghost a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  have H6 : ¬ a₆ = vampire := square_6_not_vampire a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  have H8 : ¬ a₈ = ghost := square_8_not_ghost a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  have H9 : ¬ a₉ = ghost :=  square_9_not_ghost a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  have H2m : a₂.mirror = 1 := not_vampire a₂ H2,
  have H4z : a₄.mirror + a₄.nomirror = 1 := not_zombie a₄ H4,
  have H5g : a₅.nomirror = 1 := not_ghost a₅ H5,
  have H6v : a₆.mirror = 1 := not_vampire a₆ H6,
  have H8g : a₈.nomirror = 1 := not_ghost a₈ H8,
  have H9g : a₉.nomirror = 1 := not_ghost a₉ H9,
  clear H2,clear H4,clear H5,clear H6,clear H8,clear H9,
  exact ⟨H1,H2m,H4z,H5g,H6v,H8g,H9g⟩
end

-- I want to finish the job now doing some slicker version of this case by case analysis
lemma square_7_not_zombie (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : ¬ a₇ = zombie :=
begin
--  have H := what_i_know a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  rcases (what_i_know a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved) with ⟨H1,H2m,H4z,H5g,H6v,H8g,H9g⟩,
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  cases a₁;cases H1,
--  rw H2m at *,clear H2m,
--  rw H5g at *,clear H5g,

  cases h₂, cases h₁₆,cases h₄,cases h₅,cases h₈,cases h₉,
  -- h₆ h₁₁ h₁₃ also useless
  unfold e₆ at h₆,rw [H5g,H2m,add_assoc 1,add_comm (nomirror a₄),H4z] at h₆,
  clear h₆,
  unfold e₁₁ at h₁₁,rw [H9g,H6v] at h₁₁,
  clear h₁₁,
  unfold e₁₃ at h₁₃,rw [H8g,H9g] at h₁₃,
  clear h₁₃,

  intro H7,
  cases a₇;cases H7,
  cases a₂;cases H2m;cases a₃;cases a₅;cases h₇;cases h₁₅,
end

lemma square_3_ghost (Hsolved : is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉) : a₃ = ghost :=
begin
--  have H := what_i_know a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved,
  rcases (what_i_know a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ Hsolved) with ⟨H1,H2m,H4z,H5g,H6v,H8g,H9g⟩,
  rcases Hsolved with ⟨h₁,h₂,h₃,h₄,h₅,h₆,h₇,h₈,h₉,h₁₀,h₁₁,h₁₂,h₁₃,h₁₄,h₁₅,h₁₆,HV,HG,HZ⟩,
  cases a₁;cases H1,
--  rw H2m at *,clear H2m,
--  rw H5g at *,clear H5g,

  cases h₂, cases h₁₆,cases h₄,cases h₅,cases h₈,cases h₉,
  -- h₆ h₁₁ h₁₃ also useless
  clear h₆,
  clear h₁₁,
  clear h₁₃,
  revert a₂,revert a₃,revert a₄,revert a₅,revert a₆,revert a₇,revert a₈,revert a₉,
  sorry,
--  exact dec_trivial,
end

lemma equations_so_far (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : square)
  (H1 : a₁ = vampire)
  (H2 : ¬ a₂ = vampire)
  (H4 : ¬ a₄ = zombie)
  (H5 : ¬ a₅ = ghost)
  (H6 : ¬ a₆ = vampire)
  (H7 : ¬ a₇ = zombie)
  (H8 : ¬ a₈ = ghost)
  (H9 : ¬ a₉ = ghost) :
is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ :=
begin
  unfold is_solved,
  unfold e₁,unfold e₂,unfold e₃,unfold e₄,unfold e₅,unfold e₆,unfold e₇,unfold e₈,
  unfold e₉,unfold e₁₀,unfold e₁₁,unfold e₁₂,unfold e₁₃,unfold e₁₄,unfold e₁₅,unfold e₁₆,
  rw H1,
  have H2v : a₂.mirror = 1,
    cases a₂,exfalso,apply H2,refl,refl,refl,
  rw H2v,clear H2v,
  have H4z : a₄.mirror + a₄.nomirror = 1,
    cases a₄,refl,refl,exfalso,apply H4,refl,
  -- unused
  have H5g : a₅.nomirror = 1,
    cases a₅,refl,exfalso,apply H5,refl,refl,
  rw H5g,clear H5g,
  have H6v : a₆.mirror = 1,
    cases a₆,exfalso,apply H6,refl,refl,refl,
  rw H6v,clear H6v,
  have H8g : a₈.nomirror = 1,
    cases a₈,refl,exfalso,apply H8,refl,refl,
  rw H8g,clear H8g,
  have H9g : a₉.nomirror = 1,
    cases a₉,refl,exfalso,apply H9,refl,refl,
  rw H9g,clear H9g,

  unfold mirror,unfold nomirror,simp,
  split,swap,
  split,swap,
  split,rw ←add_assoc,rw H4z,
  split,swap,
  split,swap,
  split,swap,
  split,swap,
  split,swap,
  split,swap,
  split,swap,
  repeat {sorry},
end

-- final boss
theorem unique_solution : ∃ (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ : square),
  (is_solved a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ a₉ ∧ ∀ b₁ b₂ b₃ b₄ b₅ b₆ b₇ b₈ b₉,
     is_solved b₁ b₂ b₃ b₄ b₅ b₆ b₇ b₈ b₉ →
       a₁ = b₁ ∧ a₂ = b₂ ∧ a₃ = b₃ ∧ a₄ = b₄ ∧ a₅ = b₅ ∧ a₆ = b₆ ∧ a₇ = b₇ ∧ a₈ = b₈ ∧ a₉ = b₉) := begin
  exact dec_trivial,
end

author: kbuzzard

repo: xena

save_path: github-repos/lean/kbuzzard-xena


text:
import Mt.Reservation
import Mt.Task
import Mt.Utils.Nat
import Mt.Thread

namespace Sample

structure State where
  x : Nat
  y : Nat

structure Reservation where
  luft  : Nat               -- invariant : `x ≥ y + luft`
  min_x : Mt.LowerBound     -- invariant : `x ≥ min_x`

-- [begin] this block will be provided by a `derive` handler in the future --
-----------------------------------------------------------------------------
instance : Add Reservation :=⟨fun ⟨luft, min_x⟩ ⟨luft', min_x'⟩ => ⟨luft + luft', min_x + min_x'⟩⟩

private theorem Reservation.add_rw : ∀ a b : Reservation, a + b = ⟨a.luft + b.luft, a.min_x + b.min_x⟩ :=
  by intros ; rfl

instance ReservationInstance : Mt.IsReservation Reservation where
  empty := ⟨Mt.IsReservation.empty, Mt.IsReservation.empty⟩
  assoc :=by intros ; simp only [Reservation.add_rw, Mt.IsReservation.toIsAssociative.assoc]
  comm :=by intros ; simp only [Reservation.add_rw, Mt.IsReservation.toIsCommutative.comm]
  empty_add :=by intros ; simp only [Reservation.add_rw, Mt.IsReservation.empty_add]

-----------------------------------------------------------------------------
-- [end] --------------------------------------------------------------------

def spec : Mt.Spec :={
  State
  Reservation
  validate := fun ⟨luft, min_x⟩ ⟨x, y⟩ => x ≥ y + luft ∧ x ≥ min_x
}

open Mt
open Mt.TaskM

def thread1 : Thread spec :=mk_thread do
  -- increase x atomically
  atomic_read_modify λ s => { s with x := s.x + 1 }

  -- increase y atomically
  atomic_read_modify λ s => { s with y := s.y + 1 }

  let py <- atomic_read λ ⟨_, y⟩ => y
  let px <- atomic_read λ ⟨x, _⟩ => x

  atomic_assert fun _ => px ≥ py

theorem thread1_valid : thread1.valid :=by
  rw [Thread.valid]
  apply valid_bind λ _ (r : spec.Reservation) => r.luft = 1
  . -- validate ++x
    ---------------
    apply valid_rm
    intro ⟨env_luft, env_min_x⟩ ⟨x, y⟩ _ initial_valid
    exists ⟨1, (0 : Nat)⟩
    simp only [and_true]

    have : x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0 :=initial_valid
    show x + 1 ≥ y + (env_luft + 1) ∧ x + 1 ≥ Nat.max env_min_x 0

    cases this ; constructor
    . show y + (env_luft + 1) ≤ x + 1
      calc
        _ = y + env_luft + 1 :=rfl
        _ ≤ x + 1            :=Nat.succ_le_succ (by assumption)
    . show Nat.max env_min_x 0 ≤ x + 1
      exact calc
        _ ≤ x     :=by assumption
        x ≤ x + 1 :=Nat.le_succ _

  intro ⟨luft, min_x⟩ ⟨⟩ luft_def
  apply valid_bind λ _ _ => True
  . -- validate ++y knowing luft = 1
    --------------------------------
    have luft_def : luft = 1 :=luft_def
    apply valid_rm
    intro ⟨env_luft, env_min_x⟩ ⟨x, y⟩ _ initial_valid
    exists ⟨0, min_x⟩
    simp only [and_true]
    rw [luft_def] at initial_valid

    have : x ≥ y + env_luft + 1 ∧ x ≥ env_min_x + min_x :=initial_valid
    show x ≥ y + 1 + env_luft ∧ x ≥ env_min_x + min_x

    cases this ; constructor <;> try assumption
    . show x ≥ y + 1 + env_luft
      rw [Nat.add_right_comm] ; assumption

  clear luft min_x luft_def
  intro ⟨luft, min_x⟩ ⟨⟩ ⟨⟩
  apply valid_bind (spec :=spec) λ y ⟨_, min_x⟩ => min_x = y
  . -- validate `let py = y` with `min_x := py`
    -------------------------------------------
    apply valid_read
    intro ⟨env_luft, (env_min_x : Nat)⟩ ⟨x, y⟩ _ initial_valid
    exists ⟨0, y⟩
    simp only [and_true]

    have : x ≥ y + (env_luft + luft) ∧ x ≥ Nat.max env_min_x min_x :=initial_valid
    show x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x y

    cases this ; constructor
    . show y + env_luft ≤ x
      exact calc
        y + env_luft ≤ y + (env_luft + luft) :=by simp_arith
                   _ ≤ x                     :=by assumption
    . show Nat.max env_min_x y ≤ x
      apply Utils.Nat.max_le.mpr ; constructor
      . show env_min_x ≤ x
        rename x ≥ Nat.max env_min_x min_x => h
        exact (Utils.Nat.max_le.mp h).left
      . show y ≤ x
        exact calc
          y ≤ y + (env_luft + luft) :=by simp_arith
          _ ≤ x                     :=by assumption

  clear luft min_x
  intro ⟨luft, min_x⟩ (py : Nat) min_x_def
  apply valid_bind (spec :=spec)
    λ x (r : Reservation) => x ≥ py ∧ r = IsReservation.empty
  . -- validate `let px = x` knowing min_x = py
    -------------------------------------------
    have min_x_def : min_x = py :=min_x_def
    apply valid_read
    intro ⟨env_luft, (env_min_x : Nat)⟩ ⟨x, y⟩ _ initial_valid
    exists ⟨0, (0 : Nat)⟩
    simp only [and_true, IsReservation.empty]

    have : x ≥ y + (env_luft + luft) ∧ x ≥ Nat.max env_min_x min_x :=initial_valid
    show (x ≥ y + env_luft ∧ x ≥ Nat.max env_min_x 0) ∧ x ≥ py

    cases this ; constructor ; constructor
    . show y + env_luft ≤ x
      calc
        y + env_luft ≤ y + (env_luft + luft) :=by simp_arith
                   _ ≤ x                     :=by assumption
    . show x ≥ Nat.max env_min_x 0
      rw [Utils.Nat.max_zero]
      rename x ≥ Nat.max env_min_x min_x => h
      exact (Utils.Nat.max_le.mp h).left
    . show x ≥ py
      suffices x ≥ min_x by rw [<- min_x_def] ; assumption
      rename x ≥ Nat.max env_min_x min_x => h
      exact (Utils.Nat.max_le.mp h).right

  clear luft min_x min_x_def
  intro ⟨luft, min_x⟩ (px : Nat) ⟨px_gt_py, final_check⟩

  rw [final_check]
  apply valid_assert (spec :=spec) rfl
  . -- validate `assert px ≥ py`
    ----------------------------
    intros
    simp only [px_gt_py]

end Sample

author: mirkootter

repo: lean-mt

save_path: github-repos/lean/mirkootter-lean-mt


import model_theory.substructures
import model_theory.bundled

--OUTPUT 1
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- For each $n$, let $\mathbf A_n$ be the formula:
  let A : Π n : ℕ, L.formula,
  -- $\exists x_1 \exists x_2 \ldots \exists x_n: \{x_1 \ne x_2 \land x_1 \ne x_3 \land \ldots \land x_{n - 1} \ne x_n\}$
  assume n : ℕ,
  let a : L.formula := ∃ (x1 : L.term), ∃ (x2 : L.term), ∃ (x3 : L.term), ∃ (x4 : L.term), ∃ (x5 : L.term), ∃ (x6 : L.term), ∃ (x7 : L.term), ∃ (x8 : L.term), ∃ (x9 : L.term), ∃ (x10 : L.term), ∃ (x11 : L.term), ∃ (x12 : L.term), ∃ (x13 : L.term), ∃ (x14 : L.term), ∃ (x15 : L.term), ∃ (x16 : L.term), ∃ (x17 : L.term), ∃ (x18 : L.term), ∃ (x19 : L.term), ∃ (x20 : L.term), ∃ (x21 : L.term), ∃ (x22 : L.term), ∃ (x23 : L.term), ∃ (x24 : L.term), ∃ (x25 : L.term), ∃ (x26 : L.term), ∃ (x27 : L.term), ∃ (x28 : L.term), ∃ (x29 : L.term), ∃ (x30 : L.term), ∃ (x31 : L.term), ∃ (x32 : L.term), ∃ (x33 : L.term), ∃ (x34 : L.term), ∃ (x35 : L.term), ∃ (x36 : L.term), ∃ (x37 : L.term), ∃ (x38 : L.term), ∃ (x39 : L.term), ∃ (x40 : L.term), ∃ (x41 : L.term), ∃ (x42 : L.term), ∃ (x43 : L.term), ∃ (x44 : L.term), ∃ (x45 : L.term), ∃ (x46 : L.term), ∃ (x47 : L.term), ∃ (x48 : L.term), ∃ (x49 : L.term), ∃ (x50 : L.term), ∃ (x51 : L.term), ∃ (x52 : L.term), ∃ (x53 : L.term), ∃ (x54 : L.term), ∃ (x55 : L.term), ∃ (x56 : L.term), ∃ (x57 : L.term), ∃ (x58 : L.term), ∃ (x59 : L.term), ∃ (x60 : L.term), ∃ (x61 : L.term), ∃ (x62 : L.term), ∃ (x63 : L.term), ∃ (x64 : L.term), ∃ (x65 : L.term), ∃ (x66 : L.term), ∃ (x67 : L.term), ∃ (x68 : L.term), ∃ (x69 : L.term), ∃ (x70 : L.term), ∃ (x71 : L.term), ∃ (x72 : L.term), ∃ (x73 : L.term), ∃ (x74 : L.term), ∃ (x75 : L.term), ∃ (x76 : L.term), ∃ (x77 : L.term), ∃ (x78 : L.term), ∃ (x79 : L.term), ∃ (x80 : L.term), ∃ (x81 : L.term), ∃ (x82 : L.term), ∃ (x83 : L.term), ∃ (x84 : L.term), ∃ (x85 : L.term), ∃ (x86 : L.term), ∃ (x87 : L.term), ∃ (x88 : L.term), ∃ (x89 : L.term), ∃ (x90 : L.term), ∃ (x91 : L.term), ∃ (x92 : L.term), ∃ (x93 : L.term), ∃ (x94 : L.term), ∃ (x95 : L.term), ∃ (x96 : L.term), ∃ (x97 : L.term), ∃ (x98 : L.term), ∃ (x99 : L.term), ∃ (x100 : L.term), ∃ (x101 : L.term), ∃ (x102 : L.term), ∃ (x103 : L.term), ∃ (x104 : L.term), ∃ (x105 : L.term), ∃ (x106 : L.term), ∃ (x107 : L.term), ∃ (x108 : L.term), ∃ (x109 : L.term), ∃ (x110 : L.term), ∃ (x111 : L.term), ∃ (x112 : L.term), ∃ (x113 : L.term), ∃ (x114 : L.term), ∃ (x115 : L.term), ∃ (x116 : L.term), ∃ (x117 : L.term), ∃ (x118 : L.term), ∃ (x119 : L.term), ∃ (x120 : L.term), ∃ (x121 : L.term), ∃ (x122 : L.term), ∃ (x123 : L.term), ∃ (x124 : L.term), ∃ (x125 : L.term), ∃ (x126 : L.term), ∃ (x127 : L.term), ∃ (x128 : L.term), ∃ (x129 : L.term), ∃ (x130 : L.term), ∃ (x131 : L.term), ∃ (x132 : L.term), ∃ (x133 : L.term), ∃ (x134 : L.term), ∃ (x135 : L.term), ∃ (x136 : L.term), ∃ (x137 : L.term), ∃ (x138 : L.term), ∃ (x139 : L.term), ∃ (x140 : L.term), ∃ (x141 : L.term), ∃ (x142 : L.term), ∃ (x143 : L.term), ∃ (x144 : L.term), ∃ (x145 : L.term), ∃ (x146 : L.term), ∃ (x147 : L.term), ∃ (x148 : L.term), ∃ (x149 : L.term), ∃ (x150 : L.term), ∃ (x151 : L.term), ∃ (x152 : L.term), ∃ (x153 : L.term), ∃ (x154 : L.term), ∃ (x155 : L.term), ∃ (x156 : L.term), ∃ (x157 : L.term), ∃ (x158 : L.term), ∃ (x159 : L.term), ∃ (x160 : L.term), ∃ (x161 : L.term), ∃ (x162 : L.term), ∃ (x163 : L.term), ∃ (x164 : L.term), ∃ (x165 : L.term), ∃ (x166 : L.term), ∃ (x167 : L.term), ∃ (x168 : L.term), ∃ (x169 : L.term), ∃ (x170 : L.term), ∃ (x171 : L.term), ∃ (x172 : L.term), ∃ (x173 : L.term), ∃ (x174 : L.term), ∃ (x175 : L.term), ∃ (x176 : L.term), ∃ (x177 : L.term), ∃ (x178 : L.term), ∃ (x179 : L.term), ∃ (x180 : L.term), ∃ (x181 : L.term), ∃ (x182 : L.term), ∃ (x183 : L.term), ∃ (x184 : L.term), ∃ (x185 : L.term), ∃ (x186 : L.term), ∃ (x187 : L.term), ∃ (x188
end --Needs more than 2000 tokens!

--OUTPUT 2
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- For each $n$, let $\mathbf A_n$ be the formula:
  let A_n : L.formula :=
  begin
    -- $\exists x_1 \exists x_2 \ldots \exists x_n: \{x_1 \ne x_2 \land x_1 \ne x_3 \land \ldots \land x_{n - 1} \ne x_n\}$
    have h1 : L.formula := ∃' (x₁ : L.var) (x₂ : L.var) (h₁ : x₁ ≠ x₂),
    have h2 : L.formula := ∃' (x₃ : L.var) (h₁ : x₁ ≠ x₃) (h₂ : x₂ ≠ x₃),
    have h3 : L.formula := ∃' (x₄ : L.var) (h₁ : x₁ ≠ x₄) (h₂ : x₂ ≠ x₄) (h₃ : x₃ ≠ x₄),
    have h4 : L.formula := ∃' (x₅ : L.var) (h₁ : x₁ ≠ x₅) (h₂ : x₂ ≠ x₅) (h₃ : x₃ ≠ x₅)
                                  (h₄ : x₄ ≠ x₅),
    have h5 : L.formula := ∃' (x₆ : L.var) (h₁ : x₁ ≠ x₆) (h₂ : x₂ ≠ x₆) (h₃ : x₃ ≠ x₆)
                                  (h₄ : x₄ ≠ x₆) (h₅ : x₅ ≠ x₆),
    have h6 : L.formula := ∃' (x₇ : L.var) (h₁ : x₁ ≠ x₇) (h₂ : x₂ ≠ x₇) (h₃ : x₃ ≠ x₇)
                                  (h₄ : x₄ ≠ x₇) (h₅ : x₅ ≠ x₇) (h₆ : x₆ ≠ x₇),
    have h7 : L.formula := ∃' (x₈ : L.var) (h₁ : x₁ ≠ x₈) (h₂ : x₂ ≠ x₈) (h₃ : x₃ ≠ x₈)
                                  (h₄ : x₄ ≠ x₈) (h₅ : x₅ ≠ x₈) (h₆ : x₆ ≠ x₈) (h₇ : x₇ ≠ x₈),
    have h8 : L.formula := ∃' (x₉ : L.var) (h₁ : x₁ ≠ x₉) (h₂ : x₂ ≠ x₉) (h₃ : x₃ ≠ x₉)
                                  (h₄ : x₄ ≠ x₉) (h₅ : x₅ ≠ x₉) (h₆ : x₆ ≠ x₉) (h₇ : x₇ ≠ x₉)
                                  (h₈ : x₈ ≠ x₉),
    have h9 : L.formula := ∃' (x₁₀ : L.var) (h₁ : x₁ ≠ x₁₀) (h₂ : x₂ ≠ x₁₀) (h₃ : x₃ ≠ x₁₀)
                                  (h₄ : x₄ ≠ x₁₀) (h₅ : x₅ ≠ x₁₀) (h₆ : x₆ ≠ x₁₀) (h₇ : x₇ ≠ x₁₀)
                                  (h₈ : x₈ ≠ x₁₀) (h₉ : x₉ ≠ x₁₀),
    have h10 : L.formula := ∃' (x₁₁ : L.var) (h₁ : x₁ ≠ x₁₁) (h₂ : x₂ ≠ x₁₁) (h₃ : x₃ ≠ x₁₁)
                                  (h₄ : x₄ ≠ x₁₁) (h₅ : x₅ ≠ x₁₁) (h₆ : x₆ ≠ x₁₁) (h₇ : x₇ ≠ x₁₁)
                                  (h₈ : x₈ ≠ x₁₁) (h₉ : x₉ ≠ x₁₁) (h₁₀ : x₁₀ ≠ x₁₁),
    have h11 : L.formula := ∃' (x₁₂ : L.var) (h₁ : x₁ ≠ x₁₂) (h₂ : x₂ ≠ x₁₂) (h₃ : x₃ ≠ x₁₂)
                                  (h₄ : x₄ ≠ x₁₂) (h₅ : x₅ ≠ x₁₂) (h₆ : x₆ ≠ x₁₂) (h₇ : x₇ ≠ x₁₂)
                                  (h₈ : x₈ ≠ x₁₂) (h₉ : x₉ ≠ x₁₂) (h₁₀ : x₁₀ ≠ x₁₂) (h₁₁ : x₁₁ ≠ x₁₂),
    have h12 : L.formula := ∃' (x₁₃ : L.var) (h₁ : x₁ ≠ x₁₃) (h₂ : x₂ ≠ x₁₃) (h₃ : x₃ ≠ x₁₃)
                                  (h₄ : x₄ ≠ x₁₃) (h₅ : x₅ ≠ x₁₃) (h₆ : x₆ ≠ x₁₃) (h₇ : x₇ ≠ x₁₃)
                                  (h₈ : x₈ ≠ x₁₃) (h₉ : x₉ ≠ x₁₃) (h₁₀ : x₁₀ ≠ x₁₃) (h₁₁ : x₁₁ ≠ x₁₃)
                                  (h₁₂ : x₁₂ ≠ x₁₃),
    have h13 : L.formula := ∃' (x₁₄ : L.var) (h₁ : x₁ ≠ x₁₄) (h₂ : x
end --Needs more than 2000 tokens!

--OUTPUT 3
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- For each $n$, let $\mathbf A_n$ be the formula:
  -- $\exists x_1 \exists x_2 \ldots \exists x_n: \{x_1 \ne x_2 \land x_1 \ne x_3 \land \ldots \land x_{n - 1} \ne x_n\}$
  let Γ := F.Σ,
  have h1 : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ card m, from by auto [h],
  have h2 : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ card m, from by auto [h1],
  have h3 : ∀ n : ℕ, F.Model.exists_n_diff n, from by auto [h2],

  -- Then $\mathbf A_i$ is true in a structure $\AA$ iff $\AA$ has at least $n$ elements.
  have h4 : ∀ n : ℕ, ∀ (m : F.Model) [mfin : fintype m], F.Model.exists_n_diff n → n ≤ card m, from by auto [fintype.exists_n_diff],
  have h5 : ∀ n : ℕ, ∀ (m : F.Model) [mfin : fintype m], n ≤ card m → F.Model.exists_n_diff n, from by auto [fintype.exists_n_diff],

  -- Take:
  -- $$ \Gamma := F \cup \bigcup_{i \mathop = 1}^\infty A_i $$

  -- Since $F$ has models of arbitrarily large size, every finite subset of $\Gamma$ is satisfiable.

  -- From the Compactness Theorem, $\Gamma$ is satisfiable in some model $\mathbf{M}$.

  -- But since $\mathbf{M} \models A_i$ for each $i$, $\mathbf{M}$ must be infinite.

  -- So $F$ has an infinite model.
  have h6 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ Γ, from by auto [fintype.exists_n_diff],
  have h7 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h6],
  have h8 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h7],
  have h9 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h8],
  have h10 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h9],
  have h11 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h10],
  have h12 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h11],
  have h13 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h12],
  have h14 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h13],
  have h15 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h14],
  have h16 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h15],
  have h17 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h16],
  have h18 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h17],
  have h19 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h18],
  have h20 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h19],
  have h21 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h20],
  have h22 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h21],
  have h23 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h22],
  have h24 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h23],
  have h25 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h24],
  have h26 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h25],
  have h27 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h26],
  have h28 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h27],
  have h29 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h28],
  have h30 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h29],
  have h31 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h30],
  have h32 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h31],
  have h33 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h32],
  have h34 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h33],
  have h35 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h34],
  have h36 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h35],
  have h37 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h36],
  have h38 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h37],
  have h39 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h38],
  have h40 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h39],
  have h41 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h40],
  have h42 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h41],
  have h43 : ∀ n : ℕ, F.Model.exists_n_diff n ∈ F.Σ, from by auto [h42],
end --Needs more than 2000 tokens!

--OUTPUT 4
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- For each $n$, let $\mathbf A_n$ be the formula:
  have h1 : ∀ n : ℕ, ∃ (Aₙ : L.Model) [mfin : fintype Aₙ], n ≤ fintype.card Aₙ, from by auto [h],
  -- $\mathbf A_i$ is true in a structure $\AA$ iff $\AA$ has at least $n$ elements.
  have h2 : ∀ (n : ℕ) (A : L.Model) [mfin : fintype A], L.Model.satisfies A (L.Formula.exists (L.Formula.Var 1) (L.Formula.exists (L.Formula.Var 2) (L.Formula.exists (L.Formula.Var 3) (L.Formula.exists (L.Formula.Var 4) (L.Formula.exists (L.Formula.Var 5) (L.Formula.exists (L.Formula.Var 6) (L.Formula.exists (L.Formula.Var 7) (L.Formula.exists (L.Formula.Var 8) (L.Formula.exists (L.Formula.Var 9) (L.Formula.exists (L.Formula.Var 10) (L.Formula.exists (L.Formula.Var 11) (L.Formula.exists (L.Formula.Var 12) (L.Formula.exists (L.Formula.Var 13) (L.Formula.exists (L.Formula.Var 14) (L.Formula.exists (L.Formula.Var 15) (L.Formula.exists (L.Formula.Var 16) (L.Formula.exists (L.Formula.Var 17) (L.Formula.exists (L.Formula.Var 18) (L.Formula.exists (L.Formula.Var 19) (L.Formula.exists (L.Formula.Var 20) (L.Formula.exists (L.Formula.Var 21) (L.Formula.exists (L.Formula.Var 22) (L.Formula.exists (L.Formula.Var 23) (L.Formula.exists (L.Formula.Var 24) (L.Formula.exists (L.Formula.Var 25) (L.Formula.exists (L.Formula.Var 26) (L.Formula.exists (L.Formula.Var 27) (L.Formula.exists (L.Formula.Var 28) (L.Formula.exists (L.Formula.Var 29) (L.Formula.exists (L.Formula.Var 30) (L.Formula.exists (L.Formula.Var 31) (L.Formula.exists (L.Formula.Var 32) (L.Formula.exists (L.Formula.Var 33) (L.Formula.exists (L.Formula.Var 34) (L.Formula.exists (L.Formula.Var 35) (L.Formula.exists (L.Formula.Var 36) (L.Formula.exists (L.Formula.Var 37) (L.Formula.exists (L.Formula.Var 38) (L.Formula.exists (L.Formula.Var 39) (L.Formula.exists (L.Formula.Var 40) (L.Formula.exists (L.Formula.Var 41) (L.Formula.exists (L.Formula.Var 42) (L.Formula.exists (L.Formula.Var 43) (L.Formula.exists (L.Formula.Var 44) (L.Formula.exists (L.Formula.Var 45) (L.Formula.exists (L.Formula.Var 46) (L.Formula.exists (L.Formula.Var 47) (L.Formula.exists (L.Formula.Var 48) (L.Formula.exists (L.Formula.Var 49) (L.Formula.exists (L.Formula.Var 50) (L.Formula.exists (L.Formula.Var 51) (L.Formula.exists (L.Formula.Var 52) (L.Formula.exists (L.Formula.Var 53) (L.Formula.exists (L.Formula.Var 54) (L.Formula.exists (L.Formula.Var 55) (L.Formula.exists (L.Formula.Var 56) (L.Formula.exists (L.Formula.Var 57) (L.Formula.exists (L.Formula.Var 58) (L.Formula.exists (L.Formula.Var 59) (L.Formula.exists (L.Formula.Var 60) (L.Formula.exists (L.Formula.Var 61) (L.Formula.exists (L.Formula.Var 62) (L.Formula.exists (L.Formula.Var 63) (L.Formula.exists (L.Formula.Var 64) (L.Formula.exists (L.Formula.Var 65) (L.Formula.exists (L.Formula.Var 66) (L.Formula.exists (L.Formula.Var 67) (L.Formula.exists (L.Formula.Var 68) (L.Formula.exists (L.Formula.Var 69) (L.Formula.exists (L.Formula.Var 70) (L.Formula.exists (L.Formula.Var 71) (L.Formula.exists (L.Formula.Var 72) (L.Formula.exists (L.Formula.Var 73) (L.Formula.exists (L.Formula.Var 74) (L.Formula.exists (L.Formula.Var 75) (L.Formula.exists (L.Formula.Var 76) (L.Formula.exists (L.Formula.Var 77) (L.Formula.exists (L.Formula.Var 78) (L.Formula.exists (L.Formula.Var 79) (L.Formula.exists (L.Formula.Var 80) (L.Formula.exists (L.Formula.Var 81) (L.Formula.exists (L.Formula.Var 82) (L.Formula.exists (L.Formula.Var 83) (L.Formula.exists (L.Formula.Var 84) (L.Formula.exists (L.Formula.Var 85) (L.Formula.exists (L.Formula.Var 86) (L.Formula.exists (L.Formula.Var 87) (L.Formula.exists (L.Formula.Var 88) (L.Formula.exists (L.Formula.Var 89) (L.Formula.exists (L.Formula.Var 90) (L.Formula.exists (L.Formula.Var 91) (L.Formula.exists (L.Formula.Var 92) (L.Formula.exists (L.Formula.Var 93) (L.Formula.exists (L.Formula.Var 94) (L.Formula.exists (L.Formula.Var 95) (L.Formula.exists (L.Formula.Var 96) (L.Formula.exists (L.Formula.Var 97) (L.Formula.exists (L.Formula.Var 98) (L.Formula.exists (L.Formula.Var 99) (L.Formula.exists (L.Formula.Var 100) (L.Formula.exists (L.Formula.Var 101) (L.Formula.exists (L.Formula.Var 102) (L.Formula.exists (L.Formula.Var 103) (L.Formula.exists (L.Formula.Var 104) (L.Formula.exists (L.Formula.Var 105) (L.Formula.exists (L.Formula.Var 106) (L.Formula.exists (L.Formula.Var 107) (L.Formula.exists (L.Formula.Var 108) (L.Formula.exists (L.Formula.Var 109
end --Needs more than 2000 tokens!

--OUTPUT 5
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- For each $n$, let $\mathbf A_n$ be the formula:
  have h1 : ∀ n : ℕ, ∃ (A : L.Theory), ∀ (m : F.Model) [mfin : fintype m], @fintype.card m mfin ≥ n → m ⊨ A, from
  begin
    -- $\exists x_1 \exists x_2 \ldots \exists x_n: \{x_1 \ne x_2 \land x_1 \ne x_3 \land \ldots \land x_{n - 1} \ne x_n\}$
    assume n : ℕ,
    let x1 : L.Model.sort,
    let x2 : L.Model.sort,
    let x3 : L.Model.sort,
    let x4 : L.Model.sort,
    let x5 : L.Model.sort,
    let x6 : L.Model.sort,
    let x7 : L.Model.sort,
    let x8 : L.Model.sort,
    let x9 : L.Model.sort,
    let x10 : L.Model.sort,
    let x11 : L.Model.sort,
    let x12 : L.Model.sort,
    let x13 : L.Model.sort,
    let x14 : L.Model.sort,
    let x15 : L.Model.sort,
    let x16 : L.Model.sort,
    let x17 : L.Model.sort,
    let x18 : L.Model.sort,
    let x19 : L.Model.sort,
    let x20 : L.Model.sort,
    let x21 : L.Model.sort,
    let x22 : L.Model.sort,
    let x23 : L.Model.sort,
    let x24 : L.Model.sort,
    let x25 : L.Model.sort,
    let x26 : L.Model.sort,
    let x27 : L.Model.sort,
    let x28 : L.Model.sort,
    let x29 : L.Model.sort,
    let x30 : L.Model.sort,
    let x31 : L.Model.sort,
    let x32 : L.Model.sort,
    let x33 : L.Model.sort,
    let x34 : L.Model.sort,
    let x35 : L.Model.sort,
    let x36 : L.Model.sort,
    let x37 : L.Model.sort,
    let x38 : L.Model.sort,
    let x39 : L.Model.sort,
    let x40 : L.Model.sort,
    let x41 : L.Model.sort,
    let x42 : L.Model.sort,
    let x43 : L.Model.sort,
    let x44 : L.Model.sort,
    let x45 : L.Model.sort,
    let x46 : L.Model.sort,
    let x47 : L.Model.sort,
    let x48 : L.Model.sort,
    let x49 : L.Model.sort,
    let x50 : L.Model.sort,
    let x51 : L.Model.sort,
    let x52 : L.Model.sort,
    let x53 : L.Model.sort,
    let x54 : L.Model.sort,
    let x55 : L.Model.sort,
    let x56 : L.Model.sort,
    let x57 : L.Model.sort,
    let x58 : L.Model.sort,
    let x59 : L.Model.sort,
    let x60 : L.Model.sort,
    let x61 : L.Model.sort,
    let x62 : L.Model.sort,
    let x63 : L.Model.sort,
    let x64 : L.Model.sort,
    let x65 : L.Model.sort,
    let x66 : L.Model.sort,
    let x67 : L.Model.sort,
    let x68 : L.Model.sort,
    let x69 : L.Model.sort,
    let x70 : L.Model.sort,
    let x71 : L.Model.sort,
    let x72 : L.Model.sort,
    let x73 : L.Model.sort,
    let x74 : L.Model.sort,
    let x75 : L.Model.sort,
    let x76 : L.Model.sort,
    let x77 : L.Model.sort,
    let x78 : L.Model.sort,
    let x79 : L.Model.sort,
    let x80 : L.Model.sort,
    let x81 : L.Model.sort,
    let x82 : L.Model.sort,
    let x83 : L.Model.sort,
    let x84 : L.Model.sort,
    let x85 : L.Model.sort,
    let x86 : L.Model.sort,
    let x87 : L.Model.sort,
    let x88 : L.Model.sort,
    let x89 : L.Model.sort,
    let x90 : L.Model.sort,
    let x91 : L.Model.sort,
    let x92 : L.Model.sort,
    let x93 : L.Model.sort,
    let x94 : L.Model.sort,
    let x95 : L.Model.sort,
    let x96 : L.Model.sort,
    let x97 : L.Model.sort,
    let x98 : L.Model.sort,
    let x99 : L.Model.sort,
    let x100 : L.Model.sort,
    let x101 : L.Model.sort,
    let x102 : L.Model.sort,
    let x103 : L.Model.sort,
    let x104 : L.Model.sort,
    let x105 : L.Model.sort,
    let x106 : L.Model.sort,
    let x107 : L.Model.sort,
    let x108 : L.Model.sort,
    let x109 : L.Model.sort,
    let x110 : L.Model.sort,
    let x111 : L.Model.sort,
    let x112 : L.Model.sort,
    let x113 : L.Model.sort,
    let x114 : L.Model.sort,
    let x115 : L.Model.sort,
    let x116 : L.Model.sort,
    let x117 : L.Model.sort,
    let x118 : L.Model.sort,
    let x119 : L.Model.sort,
    let x120 : L.Model.sort,
    let x121 : L.Model.sort,
    let x122 : L.Model.sort,
    let x123 : L.Model.sort,
    let x124 : L.Model.sort,
    let x125 : L.Model.sort,
    let x126 : L.Model.sort,
    let x127 : L.Model.sort,
    let x128 : L.Model.sort,
    let x129 : L.Model.sort,
    let x130 : L.Model.sort,
    let x131 : L.Model.sort,
    let x132 : L.Model.sort,
    let x133 : L.Model.sort,
    let x134 : L.Model.sort,
    let x135 : L.Model.sort,
    let x136 : L.Model.sort,
    let x137 : L.Model.sort,
    let x138 : L.Model.sort,
    let x139 : L.Model.sort,
    let x140 : L.Model.sort,
    let x141 : L.Model.sort,
    let x142 : L.Model.sort,
    let x143 : L.Model.sort,
    let x144 : L.Model.sort,
    let x145 : L.Model.sort,
    let x146 : L.Model.sort,
    let x147 : L.Model.sort,
    let x148 : L.Model.sort,
    let x149 : L.Model.sort,
    let x150 : L.Model.sort,
    let x151 : L.Model.sort,
    let x152 : L.Model.sort,
    let x153 : L.Model.sort,
    let
end --Needs more than 2000 tokens!

--OUTPUT 6
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- for each $n$, let $\mathbf A_n$ be the formula:
  -- $\exists x_1 \exists x_2 \ldots \exists x_n: \{x_1 \ne x_2 \land x_1 \ne x_3 \land \ldots \land x_{n - 1} \ne x_n\}$
  have h1 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h],
  have h2 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h1],

  -- Then $\mathbf A_i$ is true in a structure $\AA$ iff $\AA$ has at least $n$ elements.
  have h3 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h2],

  -- Take:
  -- $$ \Gamma := F \cup \bigcup_{i \mathop = 1}^\infty A_i $$
  have h4 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h3],
  have h5 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h4],
  have h6 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h5],

  -- Since $F$ has models of arbitrarily large size, every finite subset of $\Gamma$ is satisfiable.
  have h7 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h6],
  have h8 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h7],

  -- From the Compactness Theorem, $\Gamma$ is satisfiable in some model $\mathbf{M}$.
  have h9 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h8],
  have h10 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h9],

  -- But since $\mathbf{M} \models A_i$ for each $i$, $\mathbf{M}$ must be infinite.
  have h11 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h10],
  have h12 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h11],

  -- So $F$ has an infinite model.
  have h13 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h12],
  have h14 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h13],

  have h15 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h14],
  have h16 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h15],

  have h17 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h16],
  have h18 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h17],

  have h19 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h18],
  have h20 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h19],

  have h21 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h20],
  have h22 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h21],

  have h23 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h22],
  have h24 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h23],

  have h25 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h24],
  have h26 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h25],

  have h27 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h26],
  have h28 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h27],

  have h29 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h28],
  have h30 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h29],

  have h31 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h30],
  have h32 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h31],

  have h33 : ∀ n : ℕ, ∃ (A : F.Model) [mfin : fintype A], n ≤ @fintype.card A mfin, from
    by auto [h32
end --Needs more than 2000 tokens!

--OUTPUT 7
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- For each $n$, let $\mathbf A_n$ be the formula:
  let A_n : L.formula := ∃' (var 1) (var 2) ⋯ (var n), (var 1 ≠ var 2) ∧ (var 1 ≠ var 3) ∧ ⋯ ∧ (var (n-1) ≠ var n),
  -- Then $\mathbf A_i$ is true in a structure $\AA$ iff $\AA$ has at least $n$ elements.
  have h1 : ∀ (n : ℕ) (m : F.Model) [mfin : fintype m], m ⊨ A_n ↔ n ≤ @fintype.card m mfin, begin
    assume n : ℕ,
    assume m : F.Model,
    assume mfin : fintype m,
    -- m ⊨ A_n ↔ n ≤ card m
    have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
      -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
      show m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
        -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
        have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
          -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
          have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
            -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
            have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
              -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
              have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
                -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
                have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
                  -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
                  have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
                    -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
                    have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
                      -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
                      have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn)), from begin
                        -- m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m), ∃ (x3 : m), ⋯ ∃ (xn : m), (x1 ≠ x2) ∧ (x1 ≠ x3) ∧ ⋯ ∧ (x(n-1) ≠ xn))
                        have h1 : m ⊨ A_n ↔ (∃ (x1 : m), ∃ (x2 : m),
end --Needs more than 2000 tokens!

--OUTPUT 8
theorem overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
begin
  -- for each $n$, let $\mathbf A_n$ be the formula:
  have h_a : ∀ n : ℕ, L.formula, from by auto [exists_ne_self, ne_self_iff_false],

  -- Then $\mathbf A_i$ is true in a structure $\AA$ iff $\AA$ has at least $n$ elements.
  have h1 : ∀ n : ℕ, ∀ m : F.Model, @fintype.card m (fintype.mk m) ≤ n ↔ m.sat (h_a n), from by auto [fintype.card_le_iff_surj_to],

  -- take:
  have h_a_finite : ∀ (n : ℕ) (m : F.Model) [mfin : fintype m], m.sat (h_a n), from by auto [h1],
  have h_a_sat : ∀ (n : ℕ), L.formula.sat F (h_a n), from by auto [h_a_finite],
  have h_a_all : ∀ (n : ℕ), ∃ (m : F.Model), m.sat (h_a n), from by auto [h_a_sat],
  have h_a_all_inf : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin, from by auto [h_a_finite, fintype.card_le_iff_surj_to],
  have h_a_all_inf_union : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], @fintype.card m mfin ≥ n, from by auto [h_a_all_inf],

  have h_a_all_union : ∀ (n : ℕ), ∃ (m : F.Model), m.sat (h_a n), from by auto [h_a_all],
  have h_a_all_union_infinite : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin, from by auto [h_a_all_inf],
  have h_a_all_union_infinite_union : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], @fintype.card m mfin ≥ n, from by auto [h_a_all_infinite_union],

  have h_a_all_union_infinite_union_union : ∀ (n : ℕ), ∃ (m : F.Model), m.sat (h_a n), from by auto [h_a_all_union],
  have h_a_all_union_infinite_union_union_infinite : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin, from by auto [h_a_all_union_infinite],
  have h_a_all_union_infinite_union_union_infinite_union : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], @fintype.card m mfin ≥ n, from by auto [h_a_all_union_infinite_union],

  have h_a_all_union_infinite_union_union_infinite_union_union : ∀ (n : ℕ), ∃ (m : F.Model), m.sat (h_a n), from by auto [h_a_all_union_infinite_union_union],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin, from by auto [h_a_all_union_infinite_union_union_infinite],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], @fintype.card m mfin ≥ n, from by auto [h_a_all_union_infinite_union_union_infinite_union],

  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union : ∀ (n : ℕ), ∃ (m : F.Model), m.sat (h_a n), from by auto [h_a_all_union_infinite_union_union_infinite_union_union],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin, from by auto [h_a_all_union_infinite_union_union_infinite_union_union_infinite],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], @fintype.card m mfin ≥ n, from by auto [h_a_all_union_infinite_union_union_infinite_union_union_infinite_union],

  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union : ∀ (n : ℕ), ∃ (m : F.Model), m.sat (h_a n), from by auto [h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin, from by auto [h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], @fintype.card m mfin ≥ n, from by auto [h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union],

  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union : ∀ (n : ℕ), ∃ (m : F.Model), m.sat (h_a n), from by auto [h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite : ∀ (n : ℕ), ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin, from by auto [h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite_union_union_infinite],
  have h_a_all_union_infinite_union_union_infinite_union_union_infinite_union_union
end --Needs more than 2000 tokens!

/- FEW SHOT PROMPTS TO CODEX(START)
/--`theorem`
Power Set is Closed under Intersection
Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:
:$\forall A, B \in \powerset S: A \cap B \in \powerset S$
`proof`
Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.
{{qed}}
-/
theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈ 𝒫 S, (A ∩ B) ∈ 𝒫 S :=
begin
  -- $A$ and $B$ are sets. $A$ and $B$ belong to power set of $S$
  assume (A : set α) (hA : A ∈ 𝒫 S) (B : set α) (hB : B ∈ 𝒫 S),
  -- Then $A ⊆ S$ and $B ⊆ S$, by power set definition
  have h1 : (A ⊆ S) ∧ (B ⊆ S), from by auto [set.subset_of_mem_powerset, set.subset_of_mem_powerset],
  -- Then $(A ∩ B) ⊆ A$, by intersection of set is a subset
  have h2 : (A ∩ B) ⊆ A, from by auto [set.inter_subset_left],
  -- Then $(A ∩ B) ⊆ S$, by subset relation is transitive
  have h3 : (A ∩ B) ⊆ S, from by auto [set.subset.trans],
  -- Hence $(A ∩ B) ∈  𝒫 S$, by power set definition
  show (A ∩ B) ∈  𝒫 S, from by auto [set.mem_powerset],
end

/--`theorem`
Square of Sum
 :$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$
`proof`
Follows from the distribution of multiplication over addition:

{{begin-eqn}}
{{eqn | l = \left({x + y}\right)^2
      | r = \left({x + y}\right) \cdot \left({x + y}\right)
}}
{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x^2 + 2xy + y^2
      | c =
}}
{{end-eqn}}
{{qed}}
-/
theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2) :=
begin
  -- expand the power
  calc (x + y)^2 = (x+y)*(x+y) : by auto [sq]
  -- distributive property of multiplication over addition gives:
  ... = x*(x+y) + y*(x+y) : by auto [add_mul]
  -- applying the above property further gives:
  ... = x*x + x*y + y*x + y*y : by auto [mul_comm, add_mul] using [ring]
  -- rearranging the terms using commutativity and adding gives:
  ... = x^2 + 2*x*y + y^2 : by auto [sq, mul_comm] using [ring]
end

/--`theorem`
Identity of Group is Unique
Let $\struct {G, \circ}$ be a group. Then there is a unique identity element $e \in G$.
`proof`
From Group has Latin Square Property, there exists a unique $x \in G$ such that:
:$a x = b$

and there exists a unique $y \in G$ such that:
:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:
:$a x = a$

and there exists a unique $y \in G$ such that:
:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.
{{qed}}
-/
theorem group_identity_unique {G : Type*} [group G] : ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a :=
begin
  -- Group has Latin Square Property
  have h1 : ∀ a b : G, ∃! x : G, a * x = b, from by auto using [use (a⁻¹ * b)],
  have h2 : ∀ a b : G, ∃! y : G, y * a = b, from by auto using [use b * a⁻¹],

  -- Setting $b = a$, this becomes:
  have h3 : ∀ a : G, ∃! x : G, a * x = a, from by auto [h1],
  have h4 : ∀ a : G, ∃! y : G, y * a = a, from by auto [h2],

  -- These $x$ and $y$ are both $(1 : G)$, by definition of identity element
  have h5 : ∀ a : G, classical.some (h3 a).exists = (1 : G), from by auto [exists_unique.unique, h3, classical.some_spec, exists_unique.exists, mul_one],
  have h6 : ∀ a : G, classical.some (h4 a).exists = (1 : G), from by auto [exists_unique.unique, h4, classical.some_spec, exists_unique.exists, one_mul],

  show ∃! e : G, ∀ a : G, e * a = a ∧ a * e = a, from by auto [h3, h4, exists_unique.unique, classical.some_spec, exists_unique.exists] using [use (1 : G)],
end

/--`theorem`
Overflow theorem
Let $F$ be a set of first-order formulas which has finite models of arbitrarily large size. Then $F$ has an infinite model.
`proof`
For each $n$, let $\mathbf A_n$ be the formula:

$\exists x_1 \exists x_2 \ldots \exists x_n: \{x_1 \ne x_2 \land x_1 \ne x_3 \land \ldots \land x_{n - 1} \ne x_n\}$

Then $\mathbf A_i$ is true in a structure $\AA$ iff $\AA$ has at least $n$ elements.

Take:
$$ \Gamma := F \cup \bigcup_{i \mathop = 1}^\infty A_i $$

Since $F$ has models of arbitrarily large size, every finite subset of $\Gamma$ is satisfiable.

From the Compactness Theorem, $\Gamma$ is satisfiable in some model $\mathbf{M}$.

But since $\mathbf{M} \models A_i$ for each $i$, $\mathbf{M}$ must be infinite.

So $F$ has an infinite model.

QED
-/
theorem  overflow {L : first_order.language} {F : L.Theory} (h : ∀ n : ℕ, ∃ (m : F.Model) [mfin : fintype m], n ≤ @fintype.card m mfin) : ∃ (M : F.Model), infinite M :=
FEW SHOT PROMPTS TO CODEX(END)-/


text:
/-
Copyright (c) 2020 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
-/
import data.list.sigma
import testing.slim_check.sampleable
import testing.slim_check.testable
import tactic.pretty_cases

/-!
## `slim_check`: generators for functions

This file defines `sampleable` instances for `α → β` functions and
`ℤ → ℤ` injective functions.

Functions are generated by creating a list of pairs and one more value
using the list as a lookup table and resorting to the additional value
when a value is not found in the table.

Injective functions are generated by creating a list of numbers and
a permutation of that list. The permutation insures that every input
is mapped to a unique output. When an input is not found in the list
the input itself is used as an output.

Injective functions `f : α → α` could be generated easily instead of
`ℤ → ℤ` by generating a `list α`, removing duplicates and creating a
permutations. One has to be careful when generating the domain to make
if vast enough that, when generating arguments to apply `f` to,
they argument should be likely to lie in the domain of `f`. This is
the reason that injective functions `f : ℤ → ℤ` are generated by
fixing the domain to the range `[-2*size .. -2*size]`, with `size`
the size parameter of the `gen` monad.

Much of the machinery provided in this file is applicable to generate
injective functions of type `α → α` and new instances should be easy
to define.

Other classes of functions such as monotone functions can generated using
similar techniques. For monotone functions, generating two lists, sorting them
and matching them should suffice, with appropriate default values.
Some care must be taken for shrinking such functions to make sure
their defining property is invariant through shrinking. Injective
functions are an example of how complicated it can get.
-/

universes u v w

namespace slim_check

/-- Data structure specifying a total function using a list of pairs
and a default value returned when the input is not in the domain of
the partial function.

`with_default f y` encodes `x ↦ f x` when `x ∈ f` and `x ↦ y`
otherwise.

We use `Σ` to encode mappings instead of `×` because we
rely on the association list API defined in `data.list.sigma`.
 -/
inductive total_function (α : Type u) (β : Type v) : Type (max u v)
| with_default : list (Σ _ : α, β) → β → total_function

instance total_function.inhabited {α β} [inhabited β] : inhabited (total_function α β) :=
⟨ total_function.with_default ∅ (default _) ⟩

namespace total_function

/-- Apply a total function to an argument. -/
def apply {α β : Type*} [decidable_eq α] : total_function α β → α → β
| (total_function.with_default m y) x := (m.lookup x).get_or_else y

/--
Implementation of `has_repr (total_function α β)`.

Creates a string for a given `finmap` and output, `x₀ ↦ y₀, .. xₙ ↦ yₙ`
for each of the entries. The brackets are provided by the calling function.
-/
def repr_aux {α : Type u} [has_repr α] {β : Type v} [has_repr β] (m : list (Σ _ : α, β)) : string :=
string.join $ list.qsort (λ x y, x < y)
  (m.map $ λ x, sformat!"{repr $ sigma.fst x} ↦ {repr $ sigma.snd x}, ")

/--
Produce a string for a given `total_function`.
The output is of the form `[x₀ ↦ f x₀, .. xₙ ↦ f xₙ, _ ↦ y]`.
-/
protected def repr {α : Type u} [has_repr α] {β : Type v} [has_repr β] : total_function α β → string
| (total_function.with_default m y) := sformat!"[{repr_aux m}_ ↦ {has_repr.repr y}]"

instance (α : Type u) (β : Type v) [has_repr α] [has_repr β] : has_repr (total_function α β) :=
⟨ total_function.repr ⟩

/-- Create a `finmap` from a list of pairs. -/
def list.to_finmap' {α β} (xs : list (α × β)) : list (Σ _ : α, β) :=
xs.map prod.to_sigma

section

variables {α : Type u} {β : Type v} [sampleable α] [sampleable β]

/-- Redefine `sizeof` to follow the structure of `sampleable` instances. -/
def total.sizeof : total_function α β → ℕ
| ⟨m, x⟩ := 1 + @sizeof _ sampleable.wf m + sizeof x

@[priority 2000]
instance : has_sizeof (total_function α β) :=
⟨ total.sizeof ⟩

variables [decidable_eq α]

/-- Shrink a total function by shrinking the lists that represent it. -/
protected def shrink : shrink_fn (total_function α β)
| ⟨m, x⟩ := (sampleable.shrink (m, x)).map $ λ ⟨⟨m', x'⟩, h⟩, ⟨⟨list.erase_dupkeys m', x'⟩,
            lt_of_le_of_lt
              (by unfold_wf; refine @list.sizeof_erase_dupkeys _ _ _ (@sampleable.wf _ _) _) h ⟩

variables
 [has_repr α] [has_repr β]

instance pi.sampleable_ext : sampleable_ext (α → β) :=
{ proxy_repr := total_function α β,
  interp := total_function.apply,
  sample := do {
    xs ← (sampleable.sample (list (α × β)) : gen ((list (α × β)))),
    ⟨x⟩ ← (uliftable.up $ sample β : gen (ulift.{(max u v)} β)),
    pure $ total_function.with_default (list.to_finmap' xs) x },
  shrink := total_function.shrink }

end

section sampleable_ext
open sampleable_ext

@[priority 2000]
instance pi_pred.sampleable_ext {α : Type u} [sampleable_ext (α → bool)] :
  sampleable_ext.{u+1} (α → Prop) :=
{ proxy_repr := proxy_repr (α → bool),
  interp := λ m x, interp (α → bool) m x,
  sample := sample (α → bool),
  shrink := shrink }

@[priority 2000]
instance pi_uncurry.sampleable_ext {α : Type u} {β : Type v} {γ : Sort w}
  [sampleable_ext (α × β → γ)] : sampleable_ext.{(imax (u+1) (v+1) w)} (α → β → γ) :=
{ proxy_repr := proxy_repr (α × β → γ),
  interp := λ m x y, interp (α × β → γ) m (x, y),
  sample := sample (α × β → γ),
  shrink := shrink }

end sampleable_ext

end total_function

/--
Data structure specifying a total function using a list of pairs
and a default value returned when the input is not in the domain of
the partial function.

`map_to_self f` encodes `x ↦ f x` when `x ∈ f` and `x ↦ x`,
i.e. `x` to itself, otherwise.

We use `Σ` to encode mappings instead of `×` because we
rely on the association list API defined in `data.list.sigma`.
-/
inductive injective_function (α : Type u) : Type u
| map_to_self (xs : list (Σ _ : α, α)) :
    xs.map sigma.fst ~ xs.map sigma.snd → list.nodup (xs.map sigma.snd) → injective_function

instance {α} : inhabited (injective_function α) :=
⟨ ⟨ [], list.perm.nil, list.nodup_nil ⟩ ⟩

namespace injective_function

/-- Apply a total function to an argument. -/
def apply {α : Type u} [decidable_eq α] : injective_function α → α → α
| (injective_function.map_to_self m _ _) x := (m.lookup x).get_or_else x

/--
Produce a string for a given `total_function`.
The output is of the form `[x₀ ↦ f x₀, .. xₙ ↦ f xₙ, x ↦ x]`.
Unlike for `total_function`, the default value is not a constant
but the identity function.
-/
protected def repr {α : Type u} [has_repr α] : injective_function α → string
| (injective_function.map_to_self m _ _) := sformat!"[{total_function.repr_aux m}x ↦ x]"

instance (α : Type u) [has_repr α] : has_repr (injective_function α) :=
⟨ injective_function.repr ⟩

/-- Interpret a list of pairs as a total function, defaulting to
the identity function when no entries are found for a given function -/
def list.apply_id {α : Type u} [decidable_eq α] (xs : list (α × α)) (x : α) : α :=
((xs.map prod.to_sigma).lookup x).get_or_else x

@[simp]
lemma list.apply_id_cons {α : Type u} [decidable_eq α] (xs : list (α × α)) (x y z : α) :
  list.apply_id ((y, z) :: xs) x = if y = x then z else list.apply_id xs x :=
by simp only [list.apply_id, list.lookup, eq_rec_constant, prod.to_sigma, list.map]; split_ifs; refl

open function list prod (to_sigma)
open nat

lemma list.apply_id_zip_eq {α : Type u} [decidable_eq α] {xs ys : list α} (h₀ : list.nodup xs)
  (h₁ : xs.length = ys.length) (x y : α) (i : ℕ)
  (h₂ : xs.nth i = some x) :
  list.apply_id.{u} (xs.zip ys) x = y ↔ ys.nth i = some y :=
begin
  induction xs generalizing ys i,
  case list.nil : ys i h₁ h₂
  { cases h₂ },
  case list.cons : x' xs xs_ih ys i h₁ h₂
  { cases i,
    { injection h₂ with h₀ h₁, subst h₀,
      cases ys,
      { cases h₁ },
      { simp only [list.apply_id, to_sigma, option.get_or_else_some, nth, lookup_cons_eq,
                   zip_cons_cons, list.map], } },
    { cases ys,
      { cases h₁ },
      { cases h₀ with _ _ h₀ h₁,
        simp only [nth, zip_cons_cons, list.apply_id_cons] at h₂ ⊢,
        rw if_neg,
        { apply xs_ih; solve_by_elim [succ.inj] },
        { apply h₀, apply nth_mem h₂ } } } }
end

lemma apply_id_mem_iff {α : Type u} [decidable_eq α] {xs ys : list α} (h₀ : list.nodup xs)
  (h₁ : xs ~ ys)
  (x : α) :
  list.apply_id.{u} (xs.zip ys) x ∈ ys ↔ x ∈ xs :=
begin
  simp only [list.apply_id],
  cases h₃ : (lookup x (map prod.to_sigma (xs.zip ys))),
  { dsimp [option.get_or_else],
    rw h₁.mem_iff },
  { have h₂ : ys.nodup := h₁.nodup_iff.1 h₀,
    replace h₁ : xs.length = ys.length := h₁.length_eq,
    dsimp,
    induction xs generalizing ys,
    case list.nil : ys h₃ h₂ h₁
    { contradiction },
    case list.cons : x' xs xs_ih ys h₃ h₂ h₁
    { cases ys with y ys,
      { cases h₃ },
      dsimp [lookup] at h₃, split_ifs at h₃,
      { subst x', subst val,
        simp only [mem_cons_iff, true_or, eq_self_iff_true], },
      { cases h₀ with _ _ h₀ h₅,
        cases h₂ with _ _ h₂ h₄,
        have h₆ := nat.succ.inj h₁,
        specialize @xs_ih h₅ ys h₃ h₄ h₆,
        simp only [ne.symm h, xs_ih, mem_cons_iff, false_or],
        suffices : val ∈ ys, tauto!,
        erw [← option.mem_def, mem_lookup_iff] at h₃,
        simp only [to_sigma, mem_map, heq_iff_eq, prod.exists] at h₃,
        rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩,
        subst a, subst b,
        apply (mem_zip h₃).2,
        simp only [nodupkeys, keys, comp, prod.fst_to_sigma, map_map],
        rwa map_fst_zip _ _ (le_of_eq h₆) } } }
end

lemma list.apply_id_eq_self {α : Type u} [decidable_eq α] {xs ys : list α} (x : α) :
  x ∉ xs → list.apply_id.{u} (xs.zip ys) x = x :=
begin
  intro h,
  dsimp [list.apply_id],
  rw lookup_eq_none.2, refl,
  simp only [keys, not_exists, to_sigma, exists_and_distrib_right, exists_eq_right, mem_map,
             comp_app, map_map, prod.exists],
  intros y hy,
  exact h (mem_zip hy).1,
end

lemma apply_id_injective {α : Type u} [decidable_eq α] {xs ys : list α} (h₀ : list.nodup xs)
  (h₁ : xs ~ ys) : injective.{u+1 u+1} (list.apply_id (xs.zip ys)) :=
begin
  intros x y h,
  by_cases hx : x ∈ xs;
    by_cases hy : y ∈ xs,
  { rw mem_iff_nth at hx hy,
    cases hx with i hx,
    cases hy with j hy,
    suffices : some x = some y,
    { injection this },
    have h₂ := h₁.length_eq,
    rw [list.apply_id_zip_eq h₀ h₂ _ _ _ hx] at h,
    rw [← hx, ← hy], congr,
    apply nth_injective _ (h₁.nodup_iff.1 h₀),
    { symmetry, rw h,
      rw ← list.apply_id_zip_eq; assumption },
    { rw ← h₁.length_eq,
      rw nth_eq_some at hx,
      cases hx with hx hx',
      exact hx } },
  { rw ← apply_id_mem_iff h₀ h₁ at hx hy,
    rw h at hx,
    contradiction, },
  { rw ← apply_id_mem_iff h₀ h₁ at hx hy,
    rw h at hx,
    contradiction, },
  { rwa [list.apply_id_eq_self, list.apply_id_eq_self] at h; assumption },
end

open total_function (list.to_finmap')
open sampleable

/--
Remove a slice of length `m` at index `n` in a list and a permutation, maintaining the property
that it is a permutation.
-/
def perm.slice {α} [decidable_eq α] (n m : ℕ) :
  (Σ' xs ys : list α, xs ~ ys ∧ ys.nodup) → (Σ' xs ys : list α, xs ~ ys ∧ ys.nodup)
| ⟨xs, ys, h, h'⟩ :=
  let xs' := list.slice n m xs in
  have h₀ : xs' ~ ys.inter xs',
    from perm.slice_inter _ _ h h',
  ⟨xs', ys.inter xs', h₀, nodup_inter_of_nodup _ h'⟩

/--
A lazy list, in decreasing order, of sizes that should be
sliced off a list of length `n`
-/
def slice_sizes : ℕ → lazy_list ℕ+
| n :=
if h : 0 < n then
  have n / 2 < n, from div_lt_self h dec_trivial,
  lazy_list.cons ⟨_, h⟩ (slice_sizes $ n / 2)
else lazy_list.nil

/--
Shrink a permutation of a list, slicing a segment in the middle.

The sizes of the slice being removed start at `n` (with `n` the length
of the list) and then `n / 2`, then `n / 4`, etc down to 1. The slices
will be taken at index `0`, `n / k`, `2n / k`, `3n / k`, etc.
-/
protected def shrink_perm {α} [decidable_eq α] [has_sizeof α] :
  shrink_fn (Σ' xs ys : list α, xs ~ ys ∧ ys.nodup)
| xs := do
  let k := xs.1.length,
  n ← slice_sizes k,
  i ← lazy_list.of_list $ list.fin_range $ k / n,
  have ↑i * ↑n < xs.1.length,
    from nat.lt_of_div_lt_div
      (lt_of_le_of_lt (by simp only [nat.mul_div_cancel, gt_iff_lt, fin.val_eq_coe, pnat.pos]) i.2),
  pure ⟨perm.slice (i*n) n xs,
    by rcases xs with ⟨a,b,c,d⟩; dsimp [sizeof_lt]; unfold_wf; simp only [perm.slice];
       unfold_wf; apply list.sizeof_slice_lt _ _ n.2 _ this⟩

instance {α} [has_sizeof α] : has_sizeof (injective_function α) :=
⟨ λ ⟨xs,_,_⟩, sizeof (xs.map sigma.fst) ⟩

/--
Shrink an injective function slicing a segment in the middle of the domain and removing
the corresponding elements in the codomain, hence maintaining the property that
one is a permutation of the other.
-/
protected def shrink {α} [has_sizeof α] [decidable_eq α] : shrink_fn (injective_function α)
| ⟨xs, h₀, h₁⟩ := do
  ⟨⟨xs', ys', h₀, h₁⟩, h₂⟩ ← injective_function.shrink_perm ⟨_, _, h₀, h₁⟩,
  have h₃ : xs'.length ≤ ys'.length, from le_of_eq (perm.length_eq h₀),
  have h₄ : ys'.length ≤ xs'.length, from le_of_eq (perm.length_eq h₀.symm),
  pure ⟨⟨(list.zip xs' ys').map prod.to_sigma,
    by simp only [comp, map_fst_zip, map_snd_zip, *, prod.fst_to_sigma, prod.snd_to_sigma, map_map],
    by simp only [comp, map_snd_zip, *, prod.snd_to_sigma, map_map] ⟩,
    by revert h₂; dsimp [sizeof_lt]; unfold_wf;
       simp only [has_sizeof._match_1, map_map, comp, map_fst_zip, *, prod.fst_to_sigma];
       unfold_wf; intro h₂; convert h₂ ⟩

/-- Create an injective function from one list and a permutation of that list. -/
protected def mk {α} (xs ys : list α) (h : xs ~ ys) (h' : ys.nodup) : injective_function α :=
have h₀ : xs.length ≤ ys.length, from le_of_eq h.length_eq,
have h₁ : ys.length ≤ xs.length, from le_of_eq h.length_eq.symm,
injective_function.map_to_self (list.to_finmap' (xs.zip ys))
  (by { simp only [list.to_finmap', comp, map_fst_zip, map_snd_zip, *,
                   prod.fst_to_sigma, prod.snd_to_sigma, map_map] })
  (by { simp only [list.to_finmap', comp, map_snd_zip, *, prod.snd_to_sigma, map_map] })

protected lemma injective {α : Type u} [decidable_eq α] (f : injective_function α) :
  injective (apply f) :=
begin
  cases f with xs hperm hnodup,
  generalize h₀ : map sigma.fst xs = xs₀,
  generalize h₁ : xs.map (@id ((Σ _ : α, α) → α) $ @sigma.snd α (λ _ : α, α)) = xs₁,
  dsimp [id] at h₁,
  have hxs : xs = total_function.list.to_finmap' (xs₀.zip xs₁),
  { rw [← h₀, ← h₁, list.to_finmap'], clear h₀ h₁ xs₀ xs₁ hperm hnodup,
    induction xs,
    case list.nil
    { simp only [zip_nil_right, map_nil] },
    case list.cons : xs_hd xs_tl xs_ih
    { simp only [true_and, to_sigma, eq_self_iff_true, sigma.eta, zip_cons_cons, list.map],
      exact xs_ih }, },
  revert hperm hnodup,
  rw hxs, intros,
  apply apply_id_injective,
  { rwa [← h₀, hxs, hperm.nodup_iff], },
  { rwa [← hxs, h₀, h₁] at hperm, },
end

instance pi_injective.sampleable_ext : sampleable_ext { f : ℤ → ℤ // function.injective f } :=
{ proxy_repr := injective_function ℤ,
  interp := λ f, ⟨ apply f, f.injective ⟩,
  sample := gen.sized $ λ sz, do {
    let xs' := int.range (-(2*sz+2)) (2*sz + 2),
    ys ← gen.permutation_of xs',
    have Hinj : injective (λ (r : ℕ), -(2*sz + 2 : ℤ) + ↑r),
      from λ x y h, int.coe_nat_inj (add_right_injective _ h),
    let r : injective_function ℤ :=
      injective_function.mk.{0} xs' ys.1 ys.2 (ys.2.nodup_iff.1 $ nodup_map Hinj (nodup_range _)) in
    pure r },
  shrink := @injective_function.shrink ℤ _ _ }

end injective_function

open function

instance injective.testable {α β} (f : α → β)
  [I : testable (named_binder "x" $
    ∀ x : α, named_binder "y" $ ∀ y : α, named_binder "H" $ f x = f y → x = y)] :
  testable (injective f) := I

instance monotone.testable {α β} [preorder α] [preorder β] (f : α → β)
  [I : testable (named_binder "x" $
    ∀ x : α, named_binder "y" $ ∀ y : α, named_binder "H" $ x ≤ y → f x ≤ f y)] :
  testable (monotone f) := I

end slim_check

author: JLimperg


text:
import SciLean.Core
-- import SciLean.Data.GenericArray

namespace SciLean

  -- def cross (x y : ℝ^{3}) : ℝ^{3} :=
  --   Vec3.mk (x.y*y.z - x.z*y.y) (x.z*y.x - x.x*y.z) (x.x*y.y - x.y*y.x)
  -- argument x
  --   isLin := sorry, isSmooth, diff_simp,
  --   hasAdjoint := sorry,
  --   adj_simp := cross y x' by sorry,
  --   hasAdjDiff := by constructor; infer_instance; simp; infer_instance done,
  --   adjDiff_simp by simp[adjDiff]
  -- argument y
  --   isLin := sorry, isSmooth, diff_simp,
  --   hasAdjoint := sorry,
  --   adj_simp := cross y' x by sorry,
  --   hasAdjDiff := by constructor; infer_instance; simp; infer_instance done,
  --   adjDiff_simp by simp[adjDiff]

  -- @[simp]
  -- theorem cross.of_same (x : ℝ^(3:Nat)) : cross x x = 0 := sorry

  -- @[simp]
  -- theorem cross.smul_out_1 (x y : ℝ^(3:Nat)) (r : ℝ) : cross (r*x) y = r * cross x y := sorry
  -- @[simp]
  -- theorem cross.smul_out_2 (x y : ℝ^(3:Nat)) (r : ℝ) : cross x (r*y) = r * cross x y := sorry

author: lecopivo

repo: SciLean

save_path: github-repos/lean/lecopivo-SciLean


text:
import order.filter.bases
import data.nat.interval
import data.nat.lattice
import data.real.basic

open set function

namespace filter

theorem infi_le'' {ι : Sort*} {α : Type*} [complete_semilattice_Inf α] (s : ι → α) (i : ι) : infi s ≤ s i :=
Inf_le ⟨i, rfl⟩

theorem infi_le_of_le' {ι : Sort*} {α : Type*} [complete_semilattice_Inf α] {s : ι → α} {a : α} (i : ι)
  (h : s i ≤ a) : infi s ≤ a :=
le_trans (infi_le'' _ i) h

theorem binfi_le' {ι : Sort*} {α : Type*} [complete_semilattice_Inf α] {p : ι → Prop} {f : Π i (hi : p i), α}
  (i : ι) (hi : p i) : (⨅ i hi, f i hi) ≤ f i hi :=
infi_le_of_le' i (infi_le'' (f i) hi)

lemma has_basis_infi' {ι : Type*} {α : Type*} {ι' : ι → Type*} {l : ι → filter α}
  {p : Π i, ι' i → Prop} {s : Π i, ι' i → set α} (hl : ∀ i, (l i).has_basis (p i) (s i)) :
  (⨅ i, l i).has_basis (λ If : finset ι × Π i, ι' i, ∀ i ∈ If.1, p i (If.2 i))
    (λ If : finset ι × Π i, ι' i, ⋂ i ∈ If.1, s i (If.2 i)) :=
begin
  refine (has_basis_infi hl).to_has_basis _ _,
  { rintros ⟨I, f⟩ ⟨hI, hf⟩,
    refine ⟨⟨hI.to_finset, f⟩, ⟨_, _⟩⟩;
    simp only [finite.mem_to_finset, subset_Inter₂_iff],
    { exact hf },
    { rintros i hi,
      exact Inter_subset_of_subset i (Inter_subset _ hi) } },
  { rintros ⟨I, f⟩ hf,
    exact ⟨⟨I, f⟩, ⟨⟨I.finite_to_set, hf⟩, subset_refl _⟩⟩ }
end

lemma foo {α : Type*} {l : ℕ → filter α} {s : ℕ → ℝ → set α} (hs : ∀ n, monotone (s n))
  (hbasis : ∀ n, (l n).has_basis (λ ε : ℝ, 0 < ε) (s n)) : (⨅ n, l n).has_basis
  (λ Nε : ℕ × ℝ, 0 < Nε.2) (λ Nε, ⋂ (n : ℕ) (hnN : n ≤ Nε.1), s n Nε.2) :=
begin
  refine (has_basis_infi hbasis).to_has_basis _ _,
  { rintros ⟨I, ε⟩ ⟨hI, hε⟩,
    refine ⟨⟨Sup I, Inf (insert 1 $ ε '' I)⟩, ⟨_, _⟩⟩,
    { rw ((hI.image _).insert _).lt_cInf_iff (insert_nonempty _ _),
      simpa using hε },
    { intros f hf,
      rw mem_Inter₂ at hf,
      exact mem_bInter (λ i hi, hs _ (cInf_le ((hI.image _).insert _).bdd_below
        (or.inr $ mem_image_of_mem _ hi)) (hf i $ le_cSup hI.bdd_above hi)) } },
  { rintros ⟨N, ε⟩ hε,
    exact ⟨⟨Iic N, const ℕ ε⟩, ⟨finite_Iic _, λ _ _, hε⟩, λ f, id⟩ }
end

end filter

author: ADedecker

repo: distributions


text:
/-
Copyright (c) 2018 Louis Carlin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Louis Carlin, Mario Carneiro

Euclidean domains and Euclidean algorithm (extended to come)
A lot is based on pre-existing code in mathlib for natural number gcds
-/
import data.int.basic

universe u

class euclidean_domain (α : Type u) extends integral_domain α :=
(quotient : α → α → α)
(remainder : α → α → α)
 -- This could be changed to the same order as int.mod_add_div.
 -- We normally write qb+r rather than r + qb though.
(quotient_mul_add_remainder_eq : ∀ a b, b * quotient a b + remainder a b = a)
(r : α → α → Prop)
(r_well_founded : well_founded r)
(remainder_lt : ∀ a {b}, b ≠ 0 → r (remainder a b) b)
/- `val_le_mul_left` is often not a required in definitions of a euclidean
  domain since given the other properties we can show there is a
  (noncomputable) euclidean domain α with the property `val_le_mul_left`.
  So potentially this definition could be split into two different ones
  (euclidean_domain_weak and euclidean_domain_strong) with a noncomputable
  function from weak to strong. I've currently divided the lemmas into
  strong and weak depending on whether they require `val_le_mul_left` or not. -/
(mul_left_not_lt : ∀ a {b}, b ≠ 0 → ¬r (a * b) a)

namespace euclidean_domain
variable {α : Type u}
variables [euclidean_domain α]

local infix ` ≺ `:50 := euclidean_domain.r

instance : has_div α := ⟨quotient⟩

instance : has_mod α := ⟨remainder⟩

theorem div_add_mod (a b : α) : b * (a / b) + a % b = a :=
quotient_mul_add_remainder_eq _ _

lemma mod_eq_sub_mul_div {α : Type*} [euclidean_domain α] (a b : α) :
  a % b = a - b * (a / b) :=
calc a % b = b * (a / b) + a % b - b * (a / b) : by simp
... = a - b * (a / b) : by rw div_add_mod

theorem mod_lt : ∀ a {b : α}, b ≠ 0 → (a % b) ≺ b :=
remainder_lt

theorem mul_right_not_lt {a : α} (b) (h : a ≠ 0) : ¬(a * b) ≺ b :=
by rw mul_comm; exact mul_left_not_lt b h

lemma mul_div_cancel_left {a : α} (b) (a0 : a ≠ 0) : a * b / a = b :=
eq.symm $ eq_of_sub_eq_zero $ classical.by_contradiction $ λ h,
begin
  have := mul_left_not_lt a h,
  rw [mul_sub, sub_eq_iff_eq_add'.2 (div_add_mod (a*b) a).symm] at this,
  exact this (mod_lt _ a0)
end

lemma mul_div_cancel (a) {b : α} (b0 : b ≠ 0) : a * b / b = a :=
by rw mul_comm; exact mul_div_cancel_left a b0

@[simp] lemma mod_zero (a : α) : a % 0 = a :=
by simpa using div_add_mod a 0

@[simp] lemma mod_eq_zero {a b : α} : a % b = 0 ↔ b ∣ a :=
⟨λ h, by rw [← div_add_mod a b]; simp [h],
 λ ⟨c, e⟩, begin
  rw [e, ← add_left_cancel_iff, div_add_mod, add_zero],
  haveI := classical.dec,
  by_cases b0 : b = 0; simp [b0, mul_div_cancel_left],
 end⟩

@[simp] lemma mod_self (a : α) : a % a = 0 :=
mod_eq_zero.2 (dvd_refl _)

lemma dvd_mod_iff {a b c : α} (h : c ∣ b) : c ∣ a % b ↔ c ∣ a :=
by rw [dvd_add_iff_right (dvd_mul_of_dvd_left h _), div_add_mod]

lemma lt_one (a : α) : a ≺ (1:α) → a = 0 :=
by haveI := classical.dec; exact
not_imp_not.1 (λ h, by simpa using mul_left_not_lt 1 h)

lemma val_dvd_le : ∀ a b : α, b ∣ a → a ≠ 0 → ¬a ≺ b
| _ b ⟨d, rfl⟩ ha := mul_left_not_lt b (λ h, by simpa [h] using ha)

@[simp] lemma mod_one (a : α) : a % 1 = 0 :=
mod_eq_zero.2 (one_dvd _)

@[simp] lemma zero_mod (b : α) : 0 % b = 0 :=
mod_eq_zero.2 (dvd_zero _)

@[simp] lemma zero_div {a : α} (a0 : a ≠ 0) : 0 / a = 0 :=
by simpa using mul_div_cancel 0 a0

@[simp] lemma div_self {a : α} (a0 : a ≠ 0) : a / a = 1 :=
by simpa using mul_div_cancel 1 a0

section gcd
variable [decidable_eq α]

def gcd : α → α → α
| a := λ b, if a0 : a = 0 then b else
  have h:_ := mod_lt b a0,
  gcd (b%a) a
using_well_founded {dec_tac := tactic.assumption,
  rel_tac := λ _ _, `[exact ⟨_, r_well_founded α⟩]}

@[simp] theorem gcd_zero_left (a : α) : gcd 0 a = a :=
by rw gcd; simp

@[simp] theorem gcd_zero_right (a : α) : gcd a 0 = a :=
by rw gcd; by_cases a0 : a = 0; simp [a0]

theorem gcd_val (a b : α) : gcd a b = gcd (b % a) a :=
by rw gcd; by_cases a0 : a = 0; simp [a0]

@[elab_as_eliminator]
theorem gcd.induction {P : α → α → Prop} : ∀ a b : α,
  (∀ x, P 0 x) →
  (∀ a b, a ≠ 0 → P (b % a) a → P a b) →
  P a b
| a := λ b H0 H1, if a0 : a = 0 then by simp [a0, H0] else
  have h:_ := mod_lt b a0,
  H1 _ _ a0 (gcd.induction (b%a) a H0 H1)
using_well_founded {dec_tac := tactic.assumption,
  rel_tac := λ _ _, `[exact ⟨_, r_well_founded α⟩]}

theorem gcd_dvd (a b : α) : gcd a b ∣ a ∧ gcd a b ∣ b :=
gcd.induction a b
  (λ b, by simp)
  (λ a b aneq ⟨IH₁, IH₂⟩,
    by rw gcd_val; exact
    ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩)

theorem gcd_dvd_left (a b : α) : gcd a b ∣ a := (gcd_dvd a b).left

theorem gcd_dvd_right (a b : α) : gcd a b ∣ b := (gcd_dvd a b).right

theorem dvd_gcd {a b c : α} : c ∣ a → c ∣ b → c ∣ gcd a b :=
gcd.induction a b
  (by simp {contextual := tt})
  (λ a b a0 IH ca cb,
    by rw gcd_val; exact
    IH ((dvd_mod_iff ca).2 cb) ca)

theorem gcd_eq_left {a b : α} : gcd a b = a ↔ a ∣ b :=
⟨λ h, by rw ← h; apply gcd_dvd_right,
 λ h, by rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]⟩

@[simp] theorem gcd_one_left (a : α) : gcd 1 a = 1 :=
gcd_eq_left.2 (one_dvd _)

@[simp] theorem gcd_self (a : α) : gcd a a = a :=
gcd_eq_left.2 (dvd_refl _)

def xgcd_aux : α → α → α → α → α → α → α × α × α
| r := λ s t r' s' t',
if hr : r = 0 then (r', s', t')
  else
  have r' % r ≺ r, from mod_lt _ hr,
  let q := r' / r in xgcd_aux (r' % r) (s' - q * s) (t' - q * t) r s t
using_well_founded {dec_tac := tactic.assumption,
  rel_tac := λ _ _, `[exact ⟨_, r_well_founded α⟩]}

@[simp] theorem xgcd_zero_left {s t r' s' t' : α} : xgcd_aux 0 s t r' s' t' = (r', s', t') :=
by unfold xgcd_aux; rw if_pos rfl

@[simp] theorem xgcd_aux_rec {r s t r' s' t' : α} (h : r ≠ 0) :
  xgcd_aux r s t r' s' t' = xgcd_aux (r' % r) (s' - (r' / r) * s) (t' - (r' / r) * t) r s t :=
by conv {to_lhs, rw [xgcd_aux]}; simp [h]

/-- Use the extended GCD algorithm to generate the `a` and `b` values
  satisfying `gcd x y = x * a + y * b`. -/
def xgcd (x y : α) : α × α := (xgcd_aux x 1 0 y 0 1).2

/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
def gcd_a (x y : α) : α := (xgcd x y).1

/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
def gcd_b (x y : α) : α := (xgcd x y).2

@[simp] theorem xgcd_aux_fst (x y : α) : ∀ s t s' t',
  (xgcd_aux x s t y s' t').1 = gcd x y :=
gcd.induction x y (by finish) (λ x y h IH s t s' t', by simp [h, IH]; rw ← gcd_val)

theorem xgcd_aux_val (x y : α) : xgcd_aux x 1 0 y 0 1 = (gcd x y, xgcd x y) :=
by rw [xgcd, ← xgcd_aux_fst x y 1 0 0 1]; cases xgcd_aux x 1 0 y 0 1; refl

theorem xgcd_val (x y : α) : xgcd x y = (gcd_a x y, gcd_b x y) :=
by unfold gcd_a gcd_b; cases xgcd x y; refl

private def P (a b : α) : α × α × α → Prop | (r, s, t) := (r : α) = a * s + b * t

theorem xgcd_aux_P (a b : α) {r r' : α} : ∀ {s t s' t'}, P a b (r, s, t) →
  P a b (r', s', t') → P a b (xgcd_aux r s t r' s' t') :=
gcd.induction r r' (by finish) $ λ x y h IH s t s' t' p p', begin
  rw [xgcd_aux_rec h], refine IH _ p, dsimp [P] at *,
  rw [mod_eq_sub_mul_div, p, p'],
  simp [mul_add, add_mul, mul_comm, mul_assoc, mul_left_comm]
end

theorem gcd_eq_gcd_ab (a b : α) : (gcd a b : α) = a * gcd_a a b + b * gcd_b a b :=
by have := @xgcd_aux_P _ _ _ a b a b 1 0 0 1 (by simp [P]) (by simp [P]);
   rwa [xgcd_aux_val, xgcd_val] at this

end gcd

instance : euclidean_domain ℤ :=
{ quotient := (/),
  remainder := (%),
  quotient_mul_add_remainder_eq := λ a b, by rw add_comm; exact int.mod_add_div _ _,
  r := λ a b, a.nat_abs < b.nat_abs,
  r_well_founded := measure_wf (λ a, int.nat_abs a),
  remainder_lt := λ a b b0, int.coe_nat_lt.1 $
    by rw [int.nat_abs_of_nonneg (int.mod_nonneg _ b0), ← int.abs_eq_nat_abs];
    exact int.mod_lt _ b0,
  mul_left_not_lt := λ a b b0, not_lt_of_ge $
    by rw [← mul_one a.nat_abs, int.nat_abs_mul];
    exact mul_le_mul_of_nonneg_left (int.nat_abs_pos_of_ne_zero b0) (nat.zero_le _) }

end euclidean_domain

author: khoek

repo: mathlib-tidy

save_path: github-repos/lean/khoek-mathlib-tidy


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Thomas Browning
-/

import data.set_like.fintype
import group_theory.group_action.conj_act
import group_theory.p_group

/-!
# Sylow theorems

The Sylow theorems are the following results for every finite group `G` and every prime number `p`.

* There exists a Sylow `p`-subgroup of `G`.
* All Sylow `p`-subgroups of `G` are conjugate to each other.
* Let `nₚ` be the number of Sylow `p`-subgroups of `G`, then `nₚ` divides the index of the Sylow
  `p`-subgroup, `nₚ ≡ 1 [MOD p]`, and `nₚ` is equal to the index of the normalizer of the Sylow
  `p`-subgroup in `G`.

## Main definitions

* `sylow p G` : The type of Sylow `p`-subgroups of `G`.

## Main statements

* `exists_subgroup_card_pow_prime`: A generalization of Sylow's first theorem:
  For every prime power `pⁿ` dividing the cardinality of `G`,
  there exists a subgroup of `G` of order `pⁿ`.
* `is_p_group.exists_le_sylow`: A generalization of Sylow's first theorem:
  Every `p`-subgroup is contained in a Sylow `p`-subgroup.
* `sylow_conjugate`: A generalization of Sylow's second theorem:
  If the number of Sylow `p`-subgroups is finite, then all Sylow `p`-subgroups are conjugate.
* `card_sylow_modeq_one`: A generalization of Sylow's third theorem:
  If the number of Sylow `p`-subgroups is finite, then it is congruent to `1` modulo `p`.
-/

open fintype mul_action subgroup

section infinite_sylow

variables (p : ℕ) (G : Type*) [group G]

/-- A Sylow `p`-subgroup is a maximal `p`-subgroup. -/
structure sylow extends subgroup G :=
(is_p_group' : is_p_group p to_subgroup)
(is_maximal' : ∀ {Q : subgroup G}, is_p_group p Q → to_subgroup ≤ Q → Q = to_subgroup)

variables {p} {G}

namespace sylow

instance : has_coe (sylow p G) (subgroup G) := ⟨sylow.to_subgroup⟩

@[simp] lemma to_subgroup_eq_coe {P : sylow p G} : P.to_subgroup = ↑P := rfl

@[ext] lemma ext {P Q : sylow p G} (h : (P : subgroup G) = Q) : P = Q :=
by cases P; cases Q; congr'

lemma ext_iff {P Q : sylow p G} : P = Q ↔ (P : subgroup G) = Q :=
⟨congr_arg coe, ext⟩

instance : set_like (sylow p G) G :=
{ coe := coe,
  coe_injective' := λ P Q h, ext (set_like.coe_injective h) }

end sylow

/-- A generalization of **Sylow's first theorem**.
  Every `p`-subgroup is contained in a Sylow `p`-subgroup. -/
lemma is_p_group.exists_le_sylow {P : subgroup G} (hP : is_p_group p P) :
  ∃ Q : sylow p G, P ≤ Q :=
exists.elim (zorn.zorn_nonempty_partial_order₀ {Q : subgroup G | is_p_group p Q} (λ c hc1 hc2 Q hQ,
⟨ { carrier := ⋃ (R : c), R,
    one_mem' := ⟨Q, ⟨⟨Q, hQ⟩, rfl⟩, Q.one_mem⟩,
    inv_mem' := λ g ⟨_, ⟨R, rfl⟩, hg⟩, ⟨R, ⟨R, rfl⟩, R.1.inv_mem hg⟩,
    mul_mem' := λ g h ⟨_, ⟨R, rfl⟩, hg⟩ ⟨_, ⟨S, rfl⟩, hh⟩, (hc2.total_of_refl R.2 S.2).elim
      (λ T, ⟨S, ⟨S, rfl⟩, S.1.mul_mem (T hg) hh⟩) (λ T, ⟨R, ⟨R, rfl⟩, R.1.mul_mem hg (T hh)⟩) },
  λ ⟨g, _, ⟨S, rfl⟩, hg⟩, by
  { refine exists_imp_exists (λ k hk, _) (hc1 S.2 ⟨g, hg⟩),
    rwa [subtype.ext_iff, coe_pow] at hk ⊢ },
  λ M hM g hg, ⟨M, ⟨⟨M, hM⟩, rfl⟩, hg⟩⟩) P hP) (λ Q ⟨hQ1, hQ2, hQ3⟩, ⟨⟨Q, hQ1, hQ3⟩, hQ2⟩)

instance sylow.nonempty : nonempty (sylow p G) :=
nonempty_of_exists is_p_group.of_bot.exists_le_sylow

noncomputable instance sylow.inhabited : inhabited (sylow p G) :=
classical.inhabited_of_nonempty sylow.nonempty

open_locale pointwise

/-- `subgroup.pointwise_mul_action` preserves Sylow subgroups. -/
instance sylow.pointwise_mul_action {α : Type*} [group α] [mul_distrib_mul_action α G] :
  mul_action α (sylow p G) :=
{ smul := λ g P, ⟨g • P, P.2.map _, λ Q hQ hS, inv_smul_eq_iff.mp (P.3 (hQ.map _)
    (λ s hs, (congr_arg (∈ g⁻¹ • Q) (inv_smul_smul g s)).mp
      (smul_mem_pointwise_smul (g • s) g⁻¹ Q (hS (smul_mem_pointwise_smul s g P hs)))))⟩,
  one_smul := λ P, sylow.ext (one_smul α P),
  mul_smul := λ g h P, sylow.ext (mul_smul g h P) }

lemma sylow.pointwise_smul_def {α : Type*} [group α] [mul_distrib_mul_action α G]
  {g : α} {P : sylow p G} : ↑(g • P) = g • (P : subgroup G) := rfl

instance sylow.mul_action : mul_action G (sylow p G) :=
comp_hom _ mul_aut.conj

lemma sylow.smul_def {g : G} {P : sylow p G} : g • P = mul_aut.conj g • P := rfl

lemma sylow.coe_subgroup_smul {g : G} {P : sylow p G} :
  ↑(g • P) = mul_aut.conj g • (P : subgroup G) := rfl

lemma sylow.coe_smul {g : G} {P : sylow p G} :
  ↑(g • P) = mul_aut.conj g • (P : set G) := rfl

lemma sylow.smul_eq_iff_mem_normalizer {g : G} {P : sylow p G} :
  g • P = P ↔ g ∈ P.1.normalizer :=
begin
  rw [eq_comm, set_like.ext_iff, ←inv_mem_iff, mem_normalizer_iff, inv_inv],
  exact forall_congr (λ h, iff_congr iff.rfl ⟨λ ⟨a, b, c⟩, (congr_arg _ c).mp
    ((congr_arg (∈ P.1) (mul_aut.inv_apply_self G (mul_aut.conj g) a)).mpr b),
    λ hh, ⟨(mul_aut.conj g)⁻¹ h, hh, mul_aut.apply_inv_self G (mul_aut.conj g) h⟩⟩),
end

lemma subgroup.sylow_mem_fixed_points_iff (H : subgroup G) {P : sylow p G} :
  P ∈ fixed_points H (sylow p G) ↔ H ≤ P.1.normalizer :=
by simp_rw [set_like.le_def, ←sylow.smul_eq_iff_mem_normalizer]; exact subtype.forall

lemma is_p_group.inf_normalizer_sylow {P : subgroup G} (hP : is_p_group p P) (Q : sylow p G) :
  P ⊓ Q.1.normalizer = P ⊓ Q :=
le_antisymm (le_inf inf_le_left (sup_eq_right.mp (Q.3 (hP.to_inf_left.to_sup_of_normal_right'
  Q.2 inf_le_right) le_sup_right))) (inf_le_inf_left P le_normalizer)

lemma is_p_group.sylow_mem_fixed_points_iff
  {P : subgroup G} (hP : is_p_group p P) {Q : sylow p G} :
  Q ∈ fixed_points P (sylow p G) ↔ P ≤ Q :=
by rw [P.sylow_mem_fixed_points_iff, ←inf_eq_left, hP.inf_normalizer_sylow, inf_eq_left]

/-- A generalization of **Sylow's second theorem**.
  If the number of Sylow `p`-subgroups is finite, then all Sylow `p`-subgroups are conjugate. -/
instance [hp : fact p.prime] [fintype (sylow p G)] : is_pretransitive G (sylow p G) :=
⟨λ P Q, by
{ classical,
  have H := λ {R : sylow p G} {S : orbit G P},
  calc S ∈ fixed_points R (orbit G P)
      ↔ S.1 ∈ fixed_points R (sylow p G) : forall_congr (λ a, subtype.ext_iff)
  ... ↔ R.1 ≤ S : R.2.sylow_mem_fixed_points_iff
  ... ↔ S.1.1 = R : ⟨λ h, R.3 S.1.2 h, ge_of_eq⟩,
  suffices : set.nonempty (fixed_points Q (orbit G P)),
  { exact exists.elim this (λ R hR, (congr_arg _ (sylow.ext (H.mp hR))).mp R.2) },
  apply Q.2.nonempty_fixed_point_of_prime_not_dvd_card,
  refine λ h, hp.out.not_dvd_one (nat.modeq_zero_iff_dvd.mp _),
  calc 1 = card (fixed_points P (orbit G P)) : _
     ... ≡ card (orbit G P) [MOD p] : (P.2.card_modeq_card_fixed_points (orbit G P)).symm
     ... ≡ 0 [MOD p] : nat.modeq_zero_iff_dvd.mpr h,
  convert (set.card_singleton (⟨P, mem_orbit_self P⟩ : orbit G P)).symm,
  exact set.eq_singleton_iff_unique_mem.mpr ⟨H.mpr rfl, λ R h, subtype.ext (sylow.ext (H.mp h))⟩ }⟩

variables (p) (G)

/-- A generalization of **Sylow's third theorem**.
  If the number of Sylow `p`-subgroups is finite, then it is congruent to `1` modulo `p`. -/
lemma card_sylow_modeq_one [fact p.prime] [fintype (sylow p G)] : card (sylow p G) ≡ 1 [MOD p] :=
begin
  refine sylow.nonempty.elim (λ P : sylow p G, _),
  have := set.ext (λ Q : sylow p G, calc Q ∈ fixed_points P (sylow p G)
      ↔ P.1 ≤ Q : P.2.sylow_mem_fixed_points_iff
  ... ↔ Q.1 = P.1 : ⟨P.3 Q.2, ge_of_eq⟩
  ... ↔ Q ∈ {P} : sylow.ext_iff.symm.trans set.mem_singleton_iff.symm),
  haveI : fintype (fixed_points P.1 (sylow p G)) := by convert set.fintype_singleton P,
  have : card (fixed_points P.1 (sylow p G)) = 1 := by convert set.card_singleton P,
  exact (P.2.card_modeq_card_fixed_points (sylow p G)).trans (by rw this),
end

variables {p} {G}

/-- Sylow subgroups are isomorphic -/
def sylow.equiv_smul (P : sylow p G) (g : G) : P ≃* (g • P : sylow p G) :=
equiv_smul (mul_aut.conj g) P.1

/-- Sylow subgroups are isomorphic -/
noncomputable def sylow.equiv [fact p.prime] [fintype (sylow p G)] (P Q : sylow p G) :
  P ≃* Q :=
begin
  rw ← classical.some_spec (exists_smul_eq G P Q),
  exact P.equiv_smul (classical.some (exists_smul_eq G P Q)),
end

@[simp] lemma sylow.orbit_eq_top [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
  orbit G P = ⊤ :=
top_le_iff.mp (λ Q hQ, exists_smul_eq G P Q)

lemma sylow.stabilizer_eq_normalizer (P : sylow p G) : stabilizer G P = P.1.normalizer :=
ext (λ g, sylow.smul_eq_iff_mem_normalizer)

/-- Sylow `p`-subgroups are in bijection with cosets of the normalizer of a Sylow `p`-subgroup -/
noncomputable def sylow.equiv_quotient_normalizer [fact p.prime] [fintype (sylow p G)]
  (P : sylow p G) : sylow p G ≃ G ⧸ P.1.normalizer :=
calc sylow p G ≃ (⊤ : set (sylow p G)) : (equiv.set.univ (sylow p G)).symm
... ≃ orbit G P : by rw P.orbit_eq_top
... ≃ G ⧸ (stabilizer G P) : orbit_equiv_quotient_stabilizer G P
... ≃ G ⧸ P.1.normalizer : by rw P.stabilizer_eq_normalizer

noncomputable instance [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
  fintype (G ⧸ P.1.normalizer) :=
of_equiv (sylow p G) P.equiv_quotient_normalizer

lemma card_sylow_eq_card_quotient_normalizer [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
  card (sylow p G) = card (G ⧸ P.1.normalizer) :=
card_congr P.equiv_quotient_normalizer

lemma card_sylow_eq_index_normalizer [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
  card (sylow p G) = P.1.normalizer.index :=
(card_sylow_eq_card_quotient_normalizer P).trans P.1.normalizer.index_eq_card.symm

lemma card_sylow_dvd_index [fact p.prime] [fintype (sylow p G)] (P : sylow p G) :
  card (sylow p G) ∣ P.1.index :=
((congr_arg _ (card_sylow_eq_index_normalizer P)).mp dvd_rfl).trans (index_dvd_of_le le_normalizer)

/-- Frattini's Argument: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
  of `N`, then `N_G(P) ⊔ N = G`. -/
lemma sylow.normalizer_sup_eq_top {p : ℕ} [fact p.prime] {N : subgroup G} [N.normal]
  [fintype (sylow p N)] (P : sylow p N) : ((↑P : subgroup N).map N.subtype).normalizer ⊔ N = ⊤ :=
begin
  refine top_le_iff.mp (λ g hg, _),
  obtain ⟨n, hn⟩ := exists_smul_eq N ((mul_aut.conj_normal g : mul_aut N) • P) P,
  rw [←inv_mul_cancel_left ↑n g, sup_comm],
  apply mul_mem_sup (N.inv_mem n.2),
  rw [sylow.smul_def, ←mul_smul, ←mul_aut.conj_normal_coe, ←mul_aut.conj_normal.map_mul,
      sylow.ext_iff, sylow.pointwise_smul_def, pointwise_smul_def] at hn,
  refine λ x, (mem_map_iff_mem (show function.injective (mul_aut.conj (↑n * g)).to_monoid_hom,
    from (mul_aut.conj (↑n * g)).injective)).symm.trans _,
  rw [map_map, ←(congr_arg (map N.subtype) hn), map_map],
  refl,
end

end infinite_sylow

open equiv equiv.perm finset function list quotient_group
open_locale big_operators
universes u v w
variables {G : Type u} {α : Type v} {β : Type w} [group G]

local attribute [instance, priority 10] subtype.fintype set_fintype classical.prop_decidable

lemma quotient_group.card_preimage_mk [fintype G] (s : subgroup G)
  (t : set (G ⧸ s)) : fintype.card (quotient_group.mk ⁻¹' t) =
  fintype.card s * fintype.card t :=
by rw [← fintype.card_prod, fintype.card_congr
  (preimage_mk_equiv_subgroup_times_set _ _)]

namespace sylow

open subgroup submonoid mul_action

lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : subgroup G}
  [fintype ((H : set G) : Type u)] {x : G} :
  (x : G ⧸ H) ∈ fixed_points H (G ⧸ H) ↔ x ∈ normalizer H :=
⟨λ hx, have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x,
  from λ _, ((mem_fixed_points' _).1 hx _),
  (inv_mem_iff _).1 (@mem_normalizer_fintype _ _ _ _inst_2 _ (λ n (hn : n ∈ H),
    have (n⁻¹ * x)⁻¹ * x ∈ H := quotient_group.eq.1 (ha (mem_orbit _ ⟨n⁻¹, H.inv_mem hn⟩)),
    show _ ∈ H, by {rw [mul_inv_rev, inv_inv] at this, convert this, rw inv_inv}
    )),
λ (hx : ∀ (n : G), n ∈ H ↔ x * n * x⁻¹ ∈ H),
(mem_fixed_points' _).2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.eq.2
  (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy in
  have hb₂ : (b * x)⁻¹ * y ∈ H := quotient_group.eq.1 hb₂,
  (inv_mem_iff H).1 $ (hx _).2 $ (mul_mem_cancel_left H (H.inv_mem hb₁)).1
  $ by rw hx at hb₂;
    simpa [mul_inv_rev, mul_assoc] using hb₂)⟩

def fixed_points_mul_left_cosets_equiv_quotient (H : subgroup G) [fintype (H : set G)] :
  mul_action.fixed_points H (G ⧸ H) ≃
  normalizer H ⧸ (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) :=
@subtype_quotient_equiv_quotient_subtype G (normalizer H : set G) (id _) (id _) (fixed_points _ _)
  (λ a, (@mem_fixed_points_mul_left_cosets_iff_mem_normalizer _ _ _ _inst_2 _).symm)
  (by intros; refl)

/-- If `H` is a `p`-subgroup of `G`, then the index of `H` inside its normalizer is congruent
  mod `p` to the index of `H`.  -/
lemma card_quotient_normalizer_modeq_card_quotient [fintype G] {p : ℕ} {n : ℕ} [hp : fact p.prime]
  {H : subgroup G} (hH : fintype.card H = p ^ n) :
  card (normalizer H ⧸ (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H))
  ≡ card (G ⧸ H) [MOD p] :=
begin
  rw [← fintype.card_congr (fixed_points_mul_left_cosets_equiv_quotient H)],
  exact ((is_p_group.of_card hH).card_modeq_card_fixed_points _).symm
end

/-- If `H` is a subgroup of `G` of cardinality `p ^ n`, then the cardinality of the
  normalizer of `H` is congruent mod `p ^ (n + 1)` to the cardinality of `G`.  -/
lemma card_normalizer_modeq_card [fintype G] {p : ℕ} {n : ℕ} [hp : fact p.prime]
  {H : subgroup G} (hH : fintype.card H = p ^ n) :
  card (normalizer H) ≡ card G [MOD p ^ (n + 1)] :=
have subgroup.comap ((normalizer H).subtype : normalizer H →* G) H ≃ H,
  from set.bij_on.equiv (normalizer H).subtype
    ⟨λ _, id, λ _ _ _ _ h, subtype.val_injective h,
      λ x hx, ⟨⟨x, le_normalizer hx⟩, hx, rfl⟩⟩,
begin
  rw [card_eq_card_quotient_mul_card_subgroup H,
      card_eq_card_quotient_mul_card_subgroup
        (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H),
      fintype.card_congr this, hH, pow_succ],
  exact (card_quotient_normalizer_modeq_card_quotient hH).mul_right' _
end

/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup, then `p` divides the
  index of `H` inside its normalizer. -/
lemma prime_dvd_card_quotient_normalizer [fintype G] {p : ℕ} {n : ℕ} [hp : fact p.prime]
  (hdvd : p ^ (n + 1) ∣ card G) {H : subgroup G} (hH : fintype.card H = p ^ n) :
  p ∣ card (normalizer H ⧸ (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H)) :=
let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd in
have hcard : card (G ⧸ H) = s * p :=
  (nat.mul_left_inj (show card H > 0, from fintype.card_pos_iff.2
      ⟨⟨1, H.one_mem⟩⟩)).1
    (by rwa [← card_eq_card_quotient_mul_card_subgroup H, hH, hs,
      pow_succ', mul_assoc, mul_comm p]),
have hm : s * p % p =
  card (normalizer H ⧸ (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H)) % p :=
  hcard ▸ (card_quotient_normalizer_modeq_card_quotient hH).symm,
nat.dvd_of_mod_eq_zero
  (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm)

/-- If `H` is a `p`-subgroup but not a Sylow `p`-subgroup of cardinality `p ^ n`,
  then `p ^ (n + 1)` divides the cardinality of the normalizer of `H`. -/
lemma prime_pow_dvd_card_normalizer [fintype G] {p : ℕ} {n : ℕ} [hp : fact p.prime]
  (hdvd : p ^ (n + 1) ∣ card G) {H : subgroup G} (hH : fintype.card H = p ^ n) :
  p ^ (n + 1) ∣ card (normalizer H) :=
nat.modeq_zero_iff_dvd.1 ((card_normalizer_modeq_card hH).trans
  hdvd.modeq_zero_nat)

/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
  then `H` is contained in a subgroup of cardinality `p ^ (n + 1)`
  if `p ^ (n + 1)` divides the cardinality of `G` -/
theorem exists_subgroup_card_pow_succ [fintype G] {p : ℕ} {n : ℕ} [hp : fact p.prime]
  (hdvd : p ^ (n + 1) ∣ card G) {H : subgroup G} (hH : fintype.card H = p ^ n) :
  ∃ K : subgroup G, fintype.card K = p ^ (n + 1) ∧ H ≤ K :=
let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd in
have hcard : card (G ⧸ H) = s * p :=
  (nat.mul_left_inj (show card H > 0, from fintype.card_pos_iff.2
      ⟨⟨1, H.one_mem⟩⟩)).1
    (by rwa [← card_eq_card_quotient_mul_card_subgroup H, hH, hs,
      pow_succ', mul_assoc, mul_comm p]),
have hm : s * p % p =
  card (normalizer H ⧸ (subgroup.comap (normalizer H).subtype H)) % p :=
  card_congr (fixed_points_mul_left_cosets_equiv_quotient H) ▸ hcard ▸
    (is_p_group.of_card hH).card_modeq_card_fixed_points _,
have hm' : p ∣ card (normalizer H ⧸ (subgroup.comap (normalizer H).subtype H)) :=
  nat.dvd_of_mod_eq_zero
    (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm),
let ⟨x, hx⟩ := @exists_prime_order_of_dvd_card _ (quotient_group.quotient.group _) _ _ hp hm' in
have hequiv : H ≃ (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) :=
  ⟨λ a, ⟨⟨a.1, le_normalizer a.2⟩, a.2⟩, λ a, ⟨a.1.1, a.2⟩,
    λ ⟨_, _⟩, rfl, λ ⟨⟨_, _⟩, _⟩, rfl⟩,
⟨subgroup.map ((normalizer H).subtype) (subgroup.comap
  (quotient_group.mk' (comap H.normalizer.subtype H)) (zpowers x)),
begin
  show card ↥(map H.normalizer.subtype
    (comap (mk' (comap H.normalizer.subtype H)) (subgroup.zpowers x))) = p ^ (n + 1),
  suffices : card ↥(subtype.val '' ((subgroup.comap (mk' (comap H.normalizer.subtype H))
    (zpowers x)) : set (↥(H.normalizer)))) = p^(n+1),
  { convert this using 2 },
  rw [set.card_image_of_injective
        (subgroup.comap (mk' (comap H.normalizer.subtype H)) (zpowers x) : set (H.normalizer))
        subtype.val_injective,
      pow_succ', ← hH, fintype.card_congr hequiv, ← hx, order_eq_card_zpowers,
      ← fintype.card_prod],
  exact @fintype.card_congr _ _ (id _) (id _) (preimage_mk_equiv_subgroup_times_set _ _)
end,
begin
  assume y hy,
  simp only [exists_prop, subgroup.coe_subtype, mk'_apply, subgroup.mem_map, subgroup.mem_comap],
  refine ⟨⟨y, le_normalizer hy⟩, ⟨0, _⟩, rfl⟩,
  rw [zpow_zero, eq_comm, quotient_group.eq_one_iff],
  simpa using hy
end⟩

/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
  then `H` is contained in a subgroup of cardinality `p ^ m`
  if `n ≤ m` and `p ^ m` divides the cardinality of `G` -/
theorem exists_subgroup_card_pow_prime_le [fintype G] (p : ℕ) : ∀ {n m : ℕ} [hp : fact p.prime]
  (hdvd : p ^ m ∣ card G) (H : subgroup G) (hH : card H = p ^ n) (hnm : n ≤ m),
  ∃ K : subgroup G, card K = p ^ m ∧ H ≤ K
| n m := λ hp hdvd H hH hnm,
  (lt_or_eq_of_le hnm).elim
    (λ hnm : n < m,
      have h0m : 0 < m, from (lt_of_le_of_lt n.zero_le hnm),
      have wf : m - 1 < m,  from nat.sub_lt h0m zero_lt_one,
      have hnm1 : n ≤ m - 1, from le_tsub_of_add_le_right hnm,
      let ⟨K, hK⟩ := @exists_subgroup_card_pow_prime_le n (m - 1) hp
        (nat.pow_dvd_of_le_of_pow_dvd tsub_le_self hdvd) H hH hnm1 in
      have hdvd' : p ^ ((m - 1) + 1) ∣ card G, by rwa [tsub_add_cancel_of_le h0m.nat_succ_le],
      let ⟨K', hK'⟩ := @exists_subgroup_card_pow_succ _ _ _ _ _ hp hdvd' K hK.1 in
      ⟨K', by rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le], le_trans hK.2 hK'.2⟩)
    (λ hnm : n = m, ⟨H, by simp [hH, hnm]⟩)

/-- A generalisation of **Sylow's first theorem**. If `p ^ n` divides
  the cardinality of `G`, then there is a subgroup of cardinality `p ^ n` -/
theorem exists_subgroup_card_pow_prime [fintype G] (p : ℕ) {n : ℕ} [fact p.prime]
  (hdvd : p ^ n ∣ card G) : ∃ K : subgroup G, fintype.card K = p ^ n :=
let ⟨K, hK⟩ := exists_subgroup_card_pow_prime_le p hdvd ⊥ (by simp) n.zero_le in
⟨K, hK.1⟩

lemma pow_dvd_card_of_pow_dvd_card [fintype G] {p n : ℕ} [fact p.prime] (P : sylow p G)
  (hdvd : p ^ n ∣ card G) : p ^ n ∣ card P :=
begin
  obtain ⟨Q, hQ⟩ := exists_subgroup_card_pow_prime p hdvd,
  obtain ⟨R, hR⟩ := (is_p_group.of_card hQ).exists_le_sylow,
  obtain ⟨g, rfl⟩ := exists_smul_eq G R P,
  calc p ^ n = card Q : hQ.symm
  ... ∣ card R : card_dvd_of_le hR
  ... = card (g • R) : card_congr (R.equiv_smul g).to_equiv
end

lemma dvd_card_of_dvd_card [fintype G] {p : ℕ} [fact p.prime] (P : sylow p G)
  (hdvd : p ∣ card G) : p ∣ card P :=
begin
  rw ← pow_one p at hdvd,
  have key := P.pow_dvd_card_of_pow_dvd_card hdvd,
  rwa pow_one at key,
end

lemma ne_bot_of_dvd_card [fintype G] {p : ℕ} [hp : fact p.prime] (P : sylow p G)
  (hdvd : p ∣ card G) : (P : subgroup G) ≠ ⊥ :=
begin
  refine λ h, hp.out.not_dvd_one _,
  have key : p ∣ card (P : subgroup G) := P.dvd_card_of_dvd_card hdvd,
  rwa [h, card_bot] at key,
end

end sylow

author: jjaassoonn