awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet) (pp : p_1.IsPath), (p_1.transfer H hp).IsPath
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
pp : (cons h p_1).IsPath
⊢ ((cons h p_1).transfer H hp).IsPath
have cons : ∀ (pp : p_1.IsPath ∧ u_1 ∉ p_1.support), (p_1.transfer H sorry).IsPath ∧ u_1 ∉ p_1.support
Tactic: simp only [Walk.transfer, cons_isPath_iff, support_transfer _] at pp ⊢
Cleared hypotheses: pp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
pp : p.IsPath
⊢ (p.transfer H hp).IsPath
have nil : ∀ {u : V}
  (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet)
  (pp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil), (Walk.transfer Walk.nil H hp).IsPath
Tactic: induction p with
  | nil => simp
  | cons _ _ ih =>
    simp only [Walk.transfer, cons_isPath_iff, support_transfer _] at pp ⊢
    exact ⟨ih _ pp.1, pp.2⟩
Cleared hypotheses: hp, pp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
pp : p.IsPath
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet)
    (pp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil), (Walk.transfer Walk.nil H hp).IsPath
⊢ (p.transfer H hp).IsPath
have cons : ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w)
  (ih : ∀ (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (pp : p.IsPath), (p.transfer H hp).IsPath)
  (hp : ∀ e ∈ (cons h p).edges, e ∈ H.edgeSet) (pp : (cons h p).IsPath), ((cons h p).transfer H hp).IsPath
Tactic: induction p with
  | nil => simp
  | cons _ _ ih =>
    simp only [Walk.transfer, cons_isPath_iff, support_transfer _] at pp ⊢
    exact ⟨ih _ pp.1, pp.2⟩
Cleared hypotheses: hp, pp
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v : V
h : G.Adj u v
q : G.Walk v u
qc : (cons h q).IsCycle
hq : ∀ e ∈ (cons h q).edges, e ∈ H.edgeSet
⊢ ((cons h q).transfer H hq).IsCycle
have hq₁ : s(u, v) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
Tactic: simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v : V
h : G.Adj u v
q : G.Walk v u
qc : (cons h q).IsCycle
hq_1 : ∀ e ∈ (cons h q).edges, e ∈ H.edgeSet
hq : s(u, v) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
⊢ ((cons h q).transfer H hq_1).IsCycle
have cons : ∀ (qc : q.IsPath ∧ s(u, v) ∉ q.edges), (q.transfer H sorry).IsPath ∧ s(u, v) ∉ q.edges
Tactic: simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
Cleared hypotheses: qc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
q : G.Walk u u
qc : q.IsCycle
hq : ∀ e ∈ q.edges, e ∈ H.edgeSet
⊢ (q.transfer H hq).IsCycle
have nil : ∀ (qc : IsCycle.{u} (V := V) (G := G) (u := u) nil)
  (hq : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e → e ∈ H.edgeSet),
  (Walk.transfer nil H hq).IsCycle
Tactic: cases q with
  | nil => simp at qc
  | cons _ q =>
    simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq
    simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
    exact ⟨qc.1.transfer hq.2, qc.2⟩
Cleared hypotheses: q, qc, hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
q : G.Walk u u
qc : q.IsCycle
hq : ∀ e ∈ q.edges, e ∈ H.edgeSet
nil :
  ∀ (qc : IsCycle.{u} (V := V) (G := G) (u := u) Walk.nil)
    (hq : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet),
    (Walk.transfer Walk.nil H hq).IsCycle
⊢ (q.transfer H hq).IsCycle
have cons : ∀ {v : V} (h : G.Adj u v) (q : G.Walk v u) (qc : (cons h q).IsCycle) (hq : ∀ e ∈ (cons h q).edges, e ∈ H.edgeSet),
  ((cons h q).transfer H hq).IsCycle
Tactic: cases q with
  | nil => simp at qc
  | cons _ q =>
    simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq
    simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
    exact ⟨qc.1.transfer hq.2, qc.2⟩
Cleared hypotheses: q, qc, hq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v_1 w v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s
have subst_vars : ∀ (p : G.Walk u' v') (h : ∀ e ∈ (p.copy sorry sorry).edges, e ∉ s), ∀ e ∈ p.edges, e ∉ s
Tactic: subst_vars
Cleared hypotheses: v, u, p, hu, hv, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Paths (goal)
Goal:
V : Type u
G : SimpleGraph V
v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
⊢ toDeleteEdges s (p.copy hu hv) h = (toDeleteEdges s p ⋯).copy hu hv
have subst_vars : ∀ (p : G.Walk u' v') (h : ∀ e ∈ (p.copy sorry sorry).edges, e ∉ s),
  toDeleteEdges s (p.copy sorry sorry) h = (toDeleteEdges s p sorry).copy sorry sorry
Tactic: subst_vars
Cleared hypotheses: v, u, p, hu, hv, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
have obtain : ∀ (t : Set V) (ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard),
  ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
Tactic: obtain ⟨t, ht⟩ := Set.exists_subset_card_eq hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
have refine : ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
Tactic: refine ⟨t, ht.1, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑t : Type u_1))
have rw : Cardinal.mk (↑s : Type u_1) = Cardinal.mk (↑t : Type u_1)
Tactic: rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
rw : Cardinal.mk (↑s : Type u_1) = Cardinal.mk (↑t : Type u_1)
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑t : Type u_1))
have rw₁ : Cardinal.mk (↑s : Type u_1) = (↑t.ncard : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
rw : Cardinal.mk (↑s : Type u_1) = Cardinal.mk (↑t : Type u_1)
rw₁ : Cardinal.mk (↑s : Type u_1) = (↑t.ncard : Cardinal.{u_1})
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑t : Type u_1))
have rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑s.ncard : Cardinal.{u_1}) (↑t.ncard : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
rw : Cardinal.mk (↑s : Type u_1) = Cardinal.mk (↑t : Type u_1)
rw₁ : Cardinal.mk (↑s : Type u_1) = (↑t.ncard : Cardinal.{u_1})
rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑s.ncard : Cardinal.{u_1}) (↑t.ncard : Cardinal.{u_1})
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑t : Type u_1))
have rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑s.ncard : Cardinal.{u_1}) (↑s.ncard : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
have obtain : ∀ (f : (↑s : Type u_1) ≃ (↑t : Type u_1)), ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
Tactic: obtain ⟨f⟩ : Nonempty (s ≃ t) := by
    rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.UniversalVerts (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hd : Disjoint t s := ⋯
⊢ ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
have hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
Tactic: have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2)
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)
have h : ∀ (y : List α), y ∈ M.accepts.leftQuotient x ↔ y ∈ M.acceptsFrom (M.eval x)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
L : Language α
h : L.IsRegular
⊢ (Set.range L.leftQuotient).Finite
have have : ∀ (σ : Type) (x : Fintype σ) (M : DFA α σ) (hM : M.accepts = L), (Set.range L.leftQuotient).Finite
Tactic: have ⟨σ, x, M, hM⟩ := h
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range L.leftQuotient).Finite
have rw : (Set.range (M.acceptsFrom ∘ M.eval)).Finite
Tactic: rw [← hM, leftQuotient_accepts]
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
⊢ (↑(Set.range L.leftQuotient) : Type u)
have refine : (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient
Tactic: refine ⟨s.val.leftQuotient [a], ?_⟩
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
⊢ (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient
have obtain : ∀ (y : List α) (hy : L.leftQuotient y = (↑s : Language α)),
  (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient
Tactic: obtain ⟨y, hy⟩ := s.prop
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
y : List α
hy : L.leftQuotient y = (↑s : Language α)
⊢ (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient
have exists : L.leftQuotient (y ++ [a]) = (↑s : Language α).leftQuotient [a]
Tactic: exists y ++ [a]
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
y : List α
hy : L.leftQuotient y = (↑s : Language α)
⊢ L.leftQuotient (y ++ [a]) = (↑s : Language α).leftQuotient [a]
have rw : L.leftQuotient (y ++ [a]) = (L.leftQuotient y).leftQuotient [a]
Tactic: rw [← hy, leftQuotient_append]
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
y : List α
hy : L.leftQuotient y = (↑s : Language α)
rw : L.leftQuotient (y ++ [a]) = (L.leftQuotient y).leftQuotient [a]
⊢ L.leftQuotient (y ++ [a]) = (↑s : Language α).leftQuotient [a]
have rw₁ : (L.leftQuotient y).leftQuotient [a] = (L.leftQuotient y).leftQuotient [a]
Tactic: rw [← hy, leftQuotient_append]
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
σ : Type v
L : Language α
⊢ L ∈ Set.range L.leftQuotient
have exists : L.leftQuotient [] = L
Tactic: exists []
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
L : Language α
⊢ L.toDFA.accepts = L
have h : ∀ (x : List α), x ∈ L.toDFA.accepts ↔ x ∈ L
Tactic: ext x
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
L : Language α
x : List α
⊢ x ∈ L.toDFA.accepts ↔ x ∈ L
have h : L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L
Tactic: rw [DFA.mem_accepts]
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
L : Language α
x : List α
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L
have h : (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x
Tactic: suffices L.toDFA.eval x = L.leftQuotient x by simp [this]
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
L : Language α
x : List α
⊢ (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x
have h : (↑(L.toDFA.eval []) : Language α) = L.leftQuotient []
Tactic: induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih, leftQuotient_append]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.MyhillNerode (goal)
Goal:
α : Type u
L : Language α
x : List α
h : (↑(L.toDFA.eval []) : Language α) = L.leftQuotient []
⊢ (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x
have h₁ : ∀ (x : List α) (a : α) (ih : (↑(L.toDFA.eval x) : Language α) = L.leftQuotient x),
  (↑(L.toDFA.eval (x ++ [a])) : Language α) = L.leftQuotient (x ++ [a])
Tactic: induction x using List.reverseRecOn with
  | nil => simp
  | append_singleton x a ih => simp [ih, leftQuotient_append]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n : ℕ
xy : ℕ × ℕ
⊢ xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ : Finset (ℕ × ℕ) } ↔ xy.1 + xy.2 = n
have rw : xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := sorry : Finset (ℕ × ℕ) }.val ↔ xy.1 + xy.2 = n
Tactic: rw [mem_def, Multiset.Nat.mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n : ℕ
xy : ℕ × ℕ
rw : xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ : Finset (ℕ × ℕ) }.val ↔ xy.1 + xy.2 = n
⊢ xy ∈ { val := Multiset.Nat.antidiagonal n, nodup := ⋯ : Finset (ℕ × ℕ) } ↔ xy.1 + xy.2 = n
have rw₁ : xy.1 + xy.2 = n ↔ xy.1 + xy.2 = n
Tactic: rw [mem_def, Multiset.Nat.mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ @antidiagonal _ Nat.instAddMonoid _ n = map { toFun := fun (i : ℕ) ↦ (n - i, i), inj' := ⋯ } (range (n + 1))
have rw : Eq (α := Finset (ℕ × ℕ))
  (map
    (Embedding.trans { toFun := fun (i : ℕ) ↦ (i, n - i), inj' := sorry } { toFun := Prod.swap, inj' := sorry : ℕ × ℕ ↪ ℕ × ℕ })
    (range (n + 1)))
  (map { toFun := fun (i : ℕ) ↦ (n - i, i), inj' := sorry } (range (n + 1)))
Tactic: rw [← map_swap_antidiagonal, antidiagonal_eq_map, map_map]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ @antidiagonal _ Nat.instAddMonoid _ (n + 1) =
    cons (0, n + 1)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ n))
      ⋯
have a : (@antidiagonal _ Nat.instAddMonoid _ (n + 1)).val =
  (cons (0, n + 1)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ n))
      sorry).val
Tactic: apply eq_of_veq
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ @antidiagonal _ Nat.instAddMonoid _ (n + 1) =
    cons (n + 1, 0)
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      ⋯
have a : (@antidiagonal _ Nat.instAddMonoid _ (n + 1)).val =
  (cons (n + 1, 0)
      (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      sorry).val
Tactic: apply eq_of_veq
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ @antidiagonal _ Nat.instAddMonoid _ (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap
            { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
          (@antidiagonal _ Nat.instAddMonoid _ n))
        ⋯)
      ⋯
have simp_rw : cons (0, n + 1 + 1)
    (cons
      (({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ) : (a : ℕ × ℕ) → ℕ × ℕ)
        (n + 1, 0))
      (map
        (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }).trans
          ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ)))
        (@antidiagonal _ Nat.instAddMonoid _ n))
      sorry)
    sorry =
  cons (0, n + 2)
    (cons (n + 2, 0)
      (map
        ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap
          { toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      sorry)
    sorry
Tactic: simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.2 ≤ k} =
    map ({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
      (@antidiagonal _ Nat.instAddMonoid _ k)
have h₁ : ∀ (i j : ℕ),
  (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.2 ≤ k} ↔
    (i, j) ∈
      map ({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := sorry : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ k)
Tactic: ext ⟨i, j⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ (i, j) ∈ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.2 ≤ k} ↔
    (i, j) ∈
      map ({ toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
        (@antidiagonal _ Nat.instAddMonoid _ k)
have h₁ : i + j = n ∧ j ≤ k ↔ ∃ (a : ℕ), a + j = k ∧ a + (n - k) = i
Tactic: suffices i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
⊢ i + j = n ∧ j ≤ k ↔ ∃ (a : ℕ), a + j = k ∧ a + (n - k) = i
have h₁ : ∀ (hi : i + j = n ∧ j ≤ k), k - j + (n - k) = i
Tactic: refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
h₁ : ∀ (hi : i + j = n ∧ j ≤ k), k - j + (n - k) = i
⊢ i + j = n ∧ j ≤ k ↔ ∃ (a : ℕ), a + j = k ∧ a + (n - k) = i
have h₂ : (∃ (a : ℕ), a + j = k ∧ a + (n - k) = i) → i + j = n ∧ j ≤ k
Tactic: refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ k - j + (n - k) = i
have h₁ : n - k + (k - j) = i
Tactic: rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
h₁ : n - k + (k - j) = i
⊢ k - j + (n - k) = i
have h₂ : n + (k - j) - k = i
Tactic: rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
h₁ : n - k + (k - j) = i
h₂ : n + (k - j) - k = i
⊢ k - j + (n - k) = i
have h₃ : i + j + (k - j) - k = i
Tactic: rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
h₁ : n - k + (k - j) = i
h₂ : n + (k - j) - k = i
h₃ : i + j + (k - j) - k = i
⊢ k - j + (n - k) = i
have h₄ : i + (j + (k - j)) - k = i
Tactic: rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
h₁ : n - k + (k - j) = i
h₂ : n + (k - j) - k = i
h₃ : i + j + (k - j) - k = i
h₄ : i + (j + (k - j)) - k = i
⊢ k - j + (n - k) = i
have h₅ : i + k - k = i
Tactic: rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
h₁ : n - k + (k - j) = i
h₂ : n + (k - j) - k = i
h₃ : i + j + (k - j) - k = i
h₄ : i + (j + (k - j)) - k = i
h₅ : i + k - k = i
⊢ k - j + (n - k) = i
have h₆ : i = i
Tactic: rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n ∧ j ≤ k
have h₁ : l + (n - k) + j = n
Tactic: refine ⟨?_, hl ▸ Nat.le_add_left j l⟩
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k) + j = n
have h₁ : n - k + k = n
Tactic: rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (hypothesis)
Goal:
n k : ℕ
h : k ≤ n
⊢ {a ∈ @antidiagonal _ Nat.instAddMonoid _ n | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun (x : ℕ) ↦ x + (n - k), inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ Nat.instAddMonoid _ k)
have aux₁ : Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
  ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
Tactic: have aux₁ : fun a ↦ a.fst ≤ k = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j : ℕ
⊢ (∃ (a : ℕ) (b : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j
have rw : (∃ (b : ℕ) (a : ℕ), a + b = k ∧ b = i ∧ a + (n - k) = j) ↔ ∃ (a : ℕ) (b : ℕ), a + b = k ∧ a = i ∧ b + (n - k) = j
Tactic: rw [exists_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.NatAntidiagonal (goal)
Goal:
n k : ℕ
h : k ≤ n
aux₁ :
  Eq (α := (a : ℕ × ℕ) → Prop) (fun (a : ℕ × ℕ) ↦ a.1 ≤ k)
    ((fun (a : ℕ × ℕ) ↦ a.2 ≤ k) ∘ (⇑(Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ))
i j a b : ℕ
⊢ b + a = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j
have rw : a + b = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j
Tactic: rw [add_comm]