internlm/Lean-Github huggingface dataset:
Theorem: AlgHom.list_map_sum
Proof state before:
case cons
F : Type
inst✝⁵ : Field F
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ : A →ₐ[R] B
ι : Type u_1
f : ι → A
x : ι
xs : List ι
ih : φ (List.map (fun x => f x) xs).sum = (List.map (fun x => φ (f x)) xs).sum
⊢ φ (List.map (fun x => f x) (x :: xs)).sum = (List.map (fun x => φ (f x)) (x :: xs)).sum
Tactic:
simp only [List.map_cons, List.sum_cons, map_add, ih]
Proof state after:
no goals
Theorem: Groth16TypeIII.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ f = g ↔ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
Tactic:
rw [DFunLike.ext_iff]
Proof state after:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
Theorem: Groth16TypeIII.Vars.finsupp_eq_ext
Proof state before:
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) ↔ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
Tactic:
constructor
Proof state after:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ

case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ → ∀ (x : Vars), f x = g x
Theorem: Groth16TypeIII.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
⊢ (∀ (x : Vars), f x = g x) → f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
Tactic:
intro h
Proof state after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
Theorem: Groth16TypeIII.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
Tactic:
simp_rw [h]
Proof state after:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True ∧ True ∧ True
Theorem: Groth16TypeIII.Vars.finsupp_eq_ext
Proof state before:
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True ∧ True ∧ True
Tactic:
simp only [and_self]
Proof state after:
no goals
Theorem: Groth16TypeIII.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ → ∀ (x : Vars), f x = g x
Tactic:
intro h x
Proof state after:
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
x : Vars
⊢ f x = g x
Theorem: Groth16TypeIII.Vars.finsupp_eq_ext
Proof state before:
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β = g β ∧ f γ = g γ ∧ f δ = g δ
x : Vars
⊢ f x = g x
Tactic:
cases x <;> tauto
Proof state after:
no goals
Theorem: Groth16TypeIII.Polynomial.mul_self_modByMonic
Proof state before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ (t * p).modByMonic t = 0
Tactic:
rw [Polynomial.dvd_iff_modByMonic_eq_zero]
Proof state after:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t ∣ t * p

F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Theorem: Groth16TypeIII.Polynomial.mul_self_modByMonic
Proof state before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t ∣ t * p

F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Tactic:
apply dvd_mul_right
Proof state after:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Theorem: Groth16TypeIII.Polynomial.mul_self_modByMonic
Proof state before:
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
Tactic:
exact mt
Proof state after:
no goals
Theorem: Groth16TypeIII.is_sound_quotient_version
Proof state before:
F : Type
inst✝ : Field F
n_stmt n_wit n_var : ℕ
u_stmt : Fin n_stmt → Polynomial F
u_wit : Fin n_wit → Polynomial F
v_stmt : Fin n_stmt → Polynomial F
v_wit : Fin n_wit → Polynomial F
w_stmt : Fin n_stmt → Polynomial F
w_wit : Fin n_wit → Polynomial F
t : Polynomial F
stmt : Groth16TypeIII.Stmt
prover : Prover F Groth16TypeIII
sum_C_x_t sum_C_w_wit sum_C_v_wit sum_C_u_wit : Polynomial F ⧸ Ideal.span {t}
C_3 C_2 C_1 : Polynomial F
sum_B_x B_3 B_2 B_1 sum_A_x_t sum_A_w_wit : Polynomial F ⧸ Ideal.span {t}
h0021 : sum_A_w_wit * sum_B_x = 0
sum_A_v_wit : Polynomial F ⧸ Ideal.span {t}
h1121 : sum_A_v_wit * B_1 = 0
sum_A_u_wit : Polynomial F ⧸ Ideal.span {t}
h0221 : sum_A_u_wit * B_1 = 0
h0121 : -(sum_A_u_wit * sum_B_x) + -(sum_A_w_wit * B_1) = 0
sum_A_w_stmt : Polynomial F ⧸ Ideal.span {t}
h0012 : sum_A_w_stmt * sum_B_x = 0
sum_A_v_stmt : Polynomial F ⧸ Ideal.span {t}
h1112 : sum_A_v_stmt * B_1 = 0
sum_A_u_stmt : Polynomial F ⧸ Ideal.span {t}
h0212 : sum_A_u_stmt * B_1 = 0
h0112 : -(sum_A_u_stmt * sum_B_x) + -(sum_A_w_stmt * B_1) = 0
sum_A_x A_3 A_2 : Polynomial F ⧸ Ideal.span {t}
h0222 : A_2 * B_1 = 0
A_1 : Polynomial F ⧸ Ideal.span {t}
h1122 : -(A_1 * B_1) + 1 = 0
sum_w_stmt : Polynomial F ⧸ Ideal.span {t}
h0022 : -(sum_A_x * sum_B_x) + -(sum_A_w_wit * B_3) + -(sum_A_w_stmt * B_2) + (sum_w_stmt + sum_C_w_wit) = 0
sum_v_stmt : Polynomial F ⧸ Ideal.span {t}
h1022 : -(A_1 * sum_B_x) + -(sum_A_v_wit * B_3) + -(sum_A_v_stmt * B_2) + (sum_v_stmt + sum_C_v_wit) = 0
sum_u_stmt : Polynomial F ⧸ Ideal.span {t}
h0122 :
  -(A_2 * sum_B_x) + -(sum_A_u_wit * B_3) + -(sum_A_u_stmt * B_2) + -(sum_A_x * B_1) + (sum_u_stmt + sum_C_u_wit) = 0
⊢ NoZeroDivisors (Polynomial F ⧸ Ideal.span {t})
Tactic:
sorry
Proof state after:
no goals
Theorem: SimpleGraph.Menger.AB_Walk.minimal_ext
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
p : AB_Walk G₁ A B
p' : AB_Walk G₂ A B
h : Walk.support p.to_Walk = Walk.support p'.to_Walk
⊢ minimal p ↔ minimal p'
Tactic:
simp_rw [minimal, Walk.init_eq_take_support, Walk.tail_eq_tail_support, h]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.AB_Walk.tototo
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : A ∩ B = ∅
x : V
hA : x ∈ A
hB : x ∈ B
⊢ False
Tactic:
cases h ▸ Finset.mem_inter.mpr ⟨hA, hB⟩
Proof state after:
no goals
Theorem: SimpleGraph.Menger.AB_Walk.tototo
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
⊢ A ∩ B = ∅
Tactic:
ext x
Proof state after:
case a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
⊢ x ∈ A ∩ B ↔ x ∈ ∅
Theorem: SimpleGraph.Menger.AB_Walk.tototo
Proof state before:
case a
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
⊢ x ∈ A ∩ B ↔ x ∈ ∅
Tactic:
constructor <;> intro h'
Proof state after:
case a.mp
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
⊢ x ∈ ∅

case a.mpr
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ ∅
⊢ x ∈ A ∩ B
Theorem: SimpleGraph.Menger.AB_Walk.tototo
Proof state before:
case a.mp
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
⊢ x ∈ ∅
Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_inter.mp h'
Proof state after:
case a.mp.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
h1 : x ∈ A
h2 : x ∈ B
⊢ x ∈ ∅
Theorem: SimpleGraph.Menger.AB_Walk.tototo
Proof state before:
case a.mp.intro
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ A ∩ B
h1 : x ∈ A
h2 : x ∈ B
⊢ x ∈ ∅
Tactic:
cases h x h1 h2
Proof state after:
no goals
Theorem: SimpleGraph.Menger.AB_Walk.tototo
Proof state before:
case a.mpr
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
h : ∀ x ∈ A, x ∉ B
x : V
h' : x ∈ ∅
⊢ x ∈ A ∩ B
Tactic:
cases h'
Proof state after:
no goals
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
⊢ LeftInverse (push f) (lift f hf)
Tactic:
rintro ⟨a, b, ha, hb, p⟩
Proof state after:
case mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ push f (lift f hf { a := a, b := b, ha := ha, hb := hb, to_Walk := p }) =
    { a := a, b := b, ha := ha, hb := hb, to_Walk := p }
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
case mk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ push f (lift f hf { a := a, b := b, ha := ha, hb := hb, to_Walk := p }) =
    { a := a, b := b, ha := ha, hb := hb, to_Walk := p }
Tactic:
ext <;> try simp [push, lift]
Proof state after:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
have h1 := Classical.choose_spec (mem_image.mp ha) |>.2
Proof state after:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
have h2 := Classical.choose_spec (mem_image.mp hb) |>.2
Proof state after:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
have : HEq (p.copy rfl rfl) p := by rfl
Proof state after:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
this : HEq (Walk.copy p (_ : a = a) (_ : b = b)) p
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
this : HEq (Walk.copy p (_ : a = a) (_ : b = b)) p
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Tactic:
convert this
Proof state after:
no goals
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq (push f (lift f hf { a := a, b := b, ha := ha, hb := hb, to_Walk := p })).to_Walk
    { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.to_Walk
Tactic:
simp [push, lift]
Proof state after:
case mk.to_Walk
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
⊢ HEq
    (Walk.copy p
      (_ : a = f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = { a := a, b := b, ha := ha, hb := hb, to_Walk := p }.a)))
      (_ : b = f (Classical.choose (_ : ∃ a ∈ B, f a = b))))
    p
Theorem: SimpleGraph.Menger.AB_Walk.push_lift
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a✝ : V
A B X Y Z : Finset V
f : V → V'
hf : Adapted G f
a b : V'
ha : a ∈ image f A
hb : b ∈ image f B
p : Walk (map' f G) a b
h1 : f (Classical.choose (_ : ∃ a_1 ∈ A, f a_1 = a)) = a
h2 : f (Classical.choose (_ : ∃ a ∈ B, f a = b)) = b
⊢ HEq (Walk.copy p (_ : a = a) (_ : b = b)) p
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
⊢ card P ≤ card A
Tactic:
let φ (p : P) : A := ⟨p.val.a, p.val.ha⟩
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
⊢ card P ≤ card A
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
⊢ card P ≤ card A
Tactic:
have : Injective φ := by
  rintro p₁ p₂ h
  by_contra h'
  have h'' : p₁.val ≠ p₂.val := by simpa [← Subtype.ext_iff]
  have h1 : p₁.val.a ∈ p₁.val.to_Walk.support := Walk.start_mem_support _
  have h2 : p₁.val.a ∈ p₂.val.to_Walk.support := by
    simp at h ; rw [h]
    exact Walk.start_mem_support _
  exact dis p₁.prop p₂.prop h'' h1 h2
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ card P ≤ card A
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ card P ≤ card A
Tactic:
simp_rw [← Fintype.card_coe]
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ Fintype.card { x // x ∈ P } ≤ Fintype.card { x // x ∈ A }
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
this : Injective φ
⊢ Fintype.card { x // x ∈ P } ≤ Fintype.card { x // x ∈ A }
Tactic:
exact Fintype.card_le_of_injective φ this
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
⊢ Injective φ
Tactic:
rintro p₁ p₂ h
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
⊢ p₁ = p₂
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
⊢ p₁ = p₂
Tactic:
by_contra h'
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
⊢ False
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
⊢ False
Tactic:
have h'' : p₁.val ≠ p₂.val := by simpa [← Subtype.ext_iff]
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
⊢ False
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
⊢ False
Tactic:
have h1 : p₁.val.a ∈ p₁.val.to_Walk.support := Walk.start_mem_support _
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
⊢ False
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
⊢ False
Tactic:
have h2 : p₁.val.a ∈ p₂.val.to_Walk.support := by
  simp at h ; rw [h]
  exact Walk.start_mem_support _
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h2 : (↑p₁).a ∈ Walk.support (↑p₂).to_Walk
⊢ False
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h2 : (↑p₁).a ∈ Walk.support (↑p₂).to_Walk
⊢ False
Tactic:
exact dis p₁.prop p₂.prop h'' h1 h2
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
⊢ ↑p₁ ≠ ↑p₂
Tactic:
simpa [← Subtype.ext_iff]
Proof state after:
no goals
Theorem: SimpleGraph.Menger.le_A
Proof state before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h : φ p₁ = φ p₂
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
⊢ (↑p₁).a ∈ Walk.support (↑p₂).to_Walk
Tactic:
simp at h
Proof state after:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
P : Finset (AB_Walk G A B)
dis : pwd P
φ : { x // x ∈ P } → { x // x ∈ A } := fun p => { val := (↑p).a, property := (_ : (↑p).a ∈ A) }
p₁ p₂ : { x // x ∈ P }
h' : ¬p₁ = p₂
h'' : ↑p₁ ≠ ↑p₂
h1 : (↑p₁).a ∈ Walk.support (↑p₁).to_Walk
h : (↑p₁).a = (↑p₂).a
⊢ (↑p₁).a ∈ Walk.support (↑p₂).to_Walk