internlm/Lean-Github huggingface dataset:
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, (mu 𝕜) x y * ∑ z ∈ Ici y, (zeta 𝕜) y z * f z = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (mu 𝕜) x y * (zeta 𝕜) y z * f z
Tactic:
simp [mul_sum]
Proof state after:
no goals
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, ∑ z ∈ Ici y, (mu 𝕜) x y * (zeta 𝕜) y z * f z =
    ∑ z ∈ Ici x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z
Tactic:
erw [sum_sigma' (Ici x) fun y ↦ Ici y]
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ z ∈ Ici x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ z ∈ Ici x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z
Tactic:
erw [sum_sigma' (Ici x) fun z ↦ Icc x z]
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, (mu 𝕜) x x_1.snd * (zeta 𝕜) x_1.snd x_1.fst * f x_1.fst
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ x_1 ∈ (Ici x).sigma fun y => Ici y, (mu 𝕜) x x_1.fst * (zeta 𝕜) x_1.fst x_1.snd * f x_1.snd =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, (mu 𝕜) x x_1.snd * (zeta 𝕜) x_1.snd x_1.fst * f x_1.fst
Tactic:
simp only [mul_boole, MulZeroClass.zero_mul, ite_mul, zeta_apply]
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ x_1 ∈ (Ici x).sigma fun y => Ici y, if x_1.fst ≤ x_1.snd then (mu 𝕜) x x_1.fst * f x_1.snd else 0) =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, if x_1.snd ≤ x_1.fst then (mu 𝕜) x x_1.snd * f x_1.fst else 0
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ x_1 ∈ (Ici x).sigma fun y => Ici y, if x_1.fst ≤ x_1.snd then (mu 𝕜) x x_1.fst * f x_1.snd else 0) =
    ∑ x_1 ∈ (Ici x).sigma fun z => Icc x z, if x_1.snd ≤ x_1.fst then (mu 𝕜) x x_1.snd * f x_1.fst else 0
Tactic:
apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
  aesop (add simp mul_assoc) (add unsafe le_trans)
Proof state after:
no goals
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ z ∈ Ici x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜) x z * f z
Tactic:
simp_rw [mul_apply, sum_mul]
Proof state after:
no goals
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜) x z * f z = ∑ y ∈ Ici x, ∑ z ∈ Ici y, 1 x z * f z
Tactic:
simp [mu_mul_zeta 𝕜, ← add_sum_Ioi]
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0
Tactic:
exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_le
Proof state after:
no goals
Theorem: IncidenceAlgebra.moebius_inversion_top
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ ∑ y ∈ Ici x, ∑ z ∈ Ici y, 1 x z * f z = f x
Tactic:
simp [one_apply, ← add_sum_Ioi]
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Ici x, f y
x : α
this : DecidableRel fun x x_1 => x ≤ x_1 := Classical.decRel fun x x_1 => x ≤ x_1
⊢ (∑ x_1 ∈ Ioi x, if x_1 ≤ x then f x else 0) = 0
Theorem: IncidenceAlgebra.moebius_inversion_bot
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x : α
⊢ f x = ∑ y ∈ Iic x, (mu 𝕜) y x * g y
Tactic:
convert moebius_inversion_top (α := αᵒᵈ) f g h x using 3
Proof state after:
case h.e'_3.a.h.e'_5
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) x✝ x = (mu 𝕜) x x✝
Theorem: IncidenceAlgebra.moebius_inversion_bot
Proof state before:
case h.e'_3.a.h.e'_5
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ∈ Iic x, f y
x x✝ : α
a✝ : x✝ ∈ Ici x
⊢ (mu 𝕜) x✝ x = (mu 𝕜) x x✝
Tactic:
erw [mu_toDual]
Proof state after:
no goals
Theorem: IncidenceAlgebra.zeta_prod_apply
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α × β
⊢ (zeta 𝕜) a b = (zeta 𝕜) a.1 b.1 * (zeta 𝕜) a.2 b.2
Tactic:
simp [← ite_and, Prod.le_def, and_comm]
Proof state after:
no goals
Theorem: SimpleGraph.deleteEdges_eq_self
Proof state before:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
s✝ s : Set (Sym2 α)
⊢ G.deleteEdges s = G ↔ Disjoint G.edgeSet s
Tactic:
rw [deleteEdges, sdiff_eq_left, disjoint_fromEdgeSet]
Proof state after:
no goals
Theorem: SimpleGraph.ind_empty
Proof state before:
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
⊢ G.ind ∅ = ⊥
Tactic:
ext
Proof state after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
⊢ (G.ind ∅).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Theorem: SimpleGraph.ind_empty
Proof state before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
⊢ (G.ind ∅).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.ind_univ
Proof state before:
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
⊢ G.ind univ = G
Tactic:
ext
Proof state after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
⊢ (G.ind univ).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Theorem: SimpleGraph.ind_univ
Proof state before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
⊢ (G.ind univ).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.ind_singleton
Proof state before:
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a : α
⊢ G.ind {a} = ⊥
Tactic:
ext
Proof state after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ (G.ind {a}).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Theorem: SimpleGraph.ind_singleton
Proof state before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ (G.ind {a}).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
Tactic:
simp
Proof state after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ → x✝¹ = a → ¬x✝ = a
Theorem: SimpleGraph.ind_singleton
Proof state before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a✝ b : α
G : SimpleGraph α
a x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ → x✝¹ = a → ¬x✝ = a
Tactic:
rintro h rfl
Proof state after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
h : G.Adj x✝¹ x✝
⊢ ¬x✝ = x✝¹
Theorem: SimpleGraph.ind_singleton
Proof state before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
G : SimpleGraph α
x✝¹ x✝ : α
h : G.Adj x✝¹ x✝
⊢ ¬x✝ = x✝¹
Tactic:
exact h.ne'
Proof state after:
no goals
Theorem: SimpleGraph.ind_inter
Proof state before:
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝¹ : Set (Sym2 α)
s✝ t✝ : Set α
a b : α
G : SimpleGraph α
s t : Set α
⊢ G.ind (s ∩ t) = G.ind s ⊓ G.ind t
Tactic:
ext
Proof state after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝¹ : Set (Sym2 α)
s✝ t✝ : Set α
a b : α
G : SimpleGraph α
s t : Set α
x✝¹ x✝ : α
⊢ (G.ind (s ∩ t)).Adj x✝¹ x✝ ↔ (G.ind s ⊓ G.ind t).Adj x✝¹ x✝
Theorem: SimpleGraph.ind_inter
Proof state before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝¹ : Set (Sym2 α)
s✝ t✝ : Set α
a b : α
G : SimpleGraph α
s t : Set α
x✝¹ x✝ : α
⊢ (G.ind (s ∩ t)).Adj x✝¹ x✝ ↔ (G.ind s ⊓ G.ind t).Adj x✝¹ x✝
Tactic:
simp
Proof state after:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝¹ : Set (Sym2 α)
s✝ t✝ : Set α
a b : α
G : SimpleGraph α
s t : Set α
x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ ∧ (x✝¹ ∈ s ∧ x✝¹ ∈ t) ∧ x✝ ∈ s ∧ x✝ ∈ t ↔
    (G.Adj x✝¹ x✝ ∧ x✝¹ ∈ s ∧ x✝ ∈ s) ∧ G.Adj x✝¹ x✝ ∧ x✝¹ ∈ t ∧ x✝ ∈ t
Theorem: SimpleGraph.ind_inter
Proof state before:
case Adj.h.h.a
α : Type u_1
β : Type u_2
G✝ H : SimpleGraph α
s✝¹ : Set (Sym2 α)
s✝ t✝ : Set α
a b : α
G : SimpleGraph α
s t : Set α
x✝¹ x✝ : α
⊢ G.Adj x✝¹ x✝ ∧ (x✝¹ ∈ s ∧ x✝¹ ∈ t) ∧ x✝ ∈ s ∧ x✝ ∈ t ↔
    (G.Adj x✝¹ x✝ ∧ x✝¹ ∈ s ∧ x✝ ∈ s) ∧ G.Adj x✝¹ x✝ ∧ x✝¹ ∈ t ∧ x✝ ∈ t
Tactic:
tauto
Proof state after:
no goals
Theorem: SimpleGraph.disjoint_ind
Proof state before:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
h : Disjoint s t
⊢ Disjoint (G.ind s) (G.ind t)
Tactic:
rw [disjoint_iff, ← ind_inter, disjoint_iff_inter_eq_empty.1 h, ind_empty]
Proof state after:
no goals
Theorem: ZMod.pow_card_sub_one
Proof state before:
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
⊢ x ^ (p - 1) = if x ≠ 0 then 1 else 0
Tactic:
split_ifs with hx
Proof state after:
case pos
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : x ≠ 0
⊢ x ^ (p - 1) = 1

case neg
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : ¬x ≠ 0
⊢ x ^ (p - 1) = 0
Theorem: ZMod.pow_card_sub_one
Proof state before:
case pos
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : x ≠ 0
⊢ x ^ (p - 1) = 1
Tactic:
exact pow_card_sub_one_eq_one hx
Proof state after:
no goals
Theorem: ZMod.pow_card_sub_one
Proof state before:
case neg
p : ℕ
inst✝ : Fact p.Prime
x : ZMod p
hx : ¬x ≠ 0
⊢ x ^ (p - 1) = 0
Tactic:
simp [of_not_not hx, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]
Proof state after:
no goals
Theorem: AffineIndependent.convexIndependent
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 p
Tactic:
intro s x hx
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s
Theorem: AffineIndependent.convexIndependent
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s
Tactic:
by_contra
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
x✝ : x ∉ s
⊢ False
Theorem: AffineIndependent.convexIndependent
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
x✝ : x ∉ s
⊢ False
Tactic:
sorry
Proof state after:
no goals
Theorem: Finset.mem_posDiffs
Proof state before:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \₊ t ↔ ∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b \ c = a
Tactic:
simp_rw [posDiffs, mem_image, mem_filter, mem_product, Prod.exists, and_assoc, exists_and_left]
Proof state after:
no goals
Theorem: Finset.posDiffs_empty
Proof state before:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s \₊ ∅ = ∅
Tactic:
simp [posDiffs]
Proof state after:
no goals
Theorem: Finset.empty_posDiffs
Proof state before:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ ∅ \₊ s = ∅
Tactic:
simp [posDiffs]
Proof state after:
no goals
Theorem: Finset.posDiffs_subset_diffs
Proof state before:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s \₊ t ⊆ s \\ t
Tactic:
simp only [subset_iff, mem_posDiffs, mem_diffs]
Proof state after:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∀ ⦃x : α⦄, (∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b \ c = x) → ∃ a ∈ s, ∃ b ∈ t, a \ b = x
Theorem: Finset.posDiffs_subset_diffs
Proof state before:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∀ ⦃x : α⦄, (∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b \ c = x) → ∃ a ∈ s, ∃ b ∈ t, a \ b = x
Tactic:
exact fun a ⟨b, hb, c, hc, _, ha⟩ ↦ ⟨b, hb, c, hc, ha⟩
Proof state after:
no goals
Theorem: Finset.card_posDiffs_self_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : (↑𝒜).OrdConnected
⊢ (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Tactic:
revert h𝒜
Proof state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Theorem: Finset.card_posDiffs_self_le
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Tactic:
refine' Finset.memberFamily_induction_on 𝒜 _ _ _
Proof state after:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑∅).OrdConnected → (∅ \₊ ∅).card ≤ ∅.card

case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑{∅}).OrdConnected → ({∅} \₊ {∅}).card ≤ {∅}.card

case refine'_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    ((↑(nonMemberSubfamily a 𝒜)).OrdConnected →
        (nonMemberSubfamily a 𝒜 \₊ nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).card) →
      ((↑(memberSubfamily a 𝒜)).OrdConnected →
          (memberSubfamily a 𝒜 \₊ memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).card) →
        (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Theorem: Finset.card_posDiffs_self_le
Proof state before:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑∅).OrdConnected → (∅ \₊ ∅).card ≤ ∅.card
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.card_posDiffs_self_le
Proof state before:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ (↑{∅}).OrdConnected → ({∅} \₊ {∅}).card ≤ {∅}.card
Tactic:
intro
Proof state after:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜✝ : (↑{∅}).OrdConnected
⊢ ({∅} \₊ {∅}).card ≤ {∅}.card
Theorem: Finset.card_posDiffs_self_le
Proof state before:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜✝ : (↑{∅}).OrdConnected
⊢ ({∅} \₊ {∅}).card ≤ {∅}.card
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.card_posDiffs_self_le
Proof state before:
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    ((↑(nonMemberSubfamily a 𝒜)).OrdConnected →
        (nonMemberSubfamily a 𝒜 \₊ nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).card) →
      ((↑(memberSubfamily a 𝒜)).OrdConnected →
          (memberSubfamily a 𝒜 \₊ memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).card) →
        (↑𝒜).OrdConnected → (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Tactic:
rintro a 𝒜 h𝒜₀ h𝒜₁ h𝒜
Proof state after:
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
h𝒜₀ :
  (↑(nonMemberSubfamily a 𝒜)).OrdConnected →
    (nonMemberSubfamily a 𝒜 \₊ nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).card
h𝒜₁ :
  (↑(memberSubfamily a 𝒜)).OrdConnected → (memberSubfamily a 𝒜 \₊ memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).card
h𝒜 : (↑𝒜).OrdConnected
⊢ (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Theorem: Finset.card_posDiffs_self_le
Proof state before:
case refine'_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ ℬ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
h𝒜₀ :
  (↑(nonMemberSubfamily a 𝒜)).OrdConnected →
    (nonMemberSubfamily a 𝒜 \₊ nonMemberSubfamily a 𝒜).card ≤ (nonMemberSubfamily a 𝒜).card
h𝒜₁ :
  (↑(memberSubfamily a 𝒜)).OrdConnected → (memberSubfamily a 𝒜 \₊ memberSubfamily a 𝒜).card ≤ (memberSubfamily a 𝒜).card
h𝒜 : (↑𝒜).OrdConnected
⊢ (𝒜 \₊ 𝒜).card ≤ 𝒜.card
Tactic:
sorry
Proof state after:
no goals
Theorem: Finset.le_card_upper_inter_lower
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (𝒜 \₊ ℬ).card ≤ (𝒜 ∩ ℬ).card
Tactic:
refine' (card_le_card _).trans (card_posDiffs_self_le _)
Proof state after:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 𝒜 \₊ ℬ ⊆ 𝒜 ∩ ℬ \₊ (𝒜 ∩ ℬ)

case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑(𝒜 ∩ ℬ)).OrdConnected
Theorem: Finset.le_card_upper_inter_lower
Proof state before:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 𝒜 \₊ ℬ ⊆ 𝒜 ∩ ℬ \₊ (𝒜 ∩ ℬ)
Tactic:
simp_rw [subset_iff, mem_posDiffs, mem_inter]
Proof state after:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ ∀ ⦃x : Finset α⦄,
    (∃ b ∈ 𝒜, ∃ c ∈ ℬ, c ≤ b ∧ b \ c = x) → ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = x
Theorem: Finset.le_card_upper_inter_lower
Proof state before:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ ∀ ⦃x : Finset α⦄,
    (∃ b ∈ 𝒜, ∃ c ∈ ℬ, c ≤ b ∧ b \ c = x) → ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = x
Tactic:
rintro _ ⟨s, hs, t, ht, hts, rfl⟩
Proof state after:
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
s : Finset α
hs : s ∈ 𝒜
t : Finset α
ht : t ∈ ℬ
hts : t ≤ s
⊢ ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = s \ t
Theorem: Finset.le_card_upper_inter_lower
Proof state before:
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
s : Finset α
hs : s ∈ 𝒜
t : Finset α
ht : t ∈ ℬ
hts : t ≤ s
⊢ ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = s \ t
Tactic:
exact ⟨s, ⟨hs, hℬ hts ht⟩, t, ⟨h𝒜 hts hs, ht⟩, hts, rfl⟩
Proof state after:
no goals
Theorem: Finset.le_card_upper_inter_lower
Proof state before:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑(𝒜 ∩ ℬ)).OrdConnected
Tactic:
rw [coe_inter]
Proof state after:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑𝒜 ∩ ↑ℬ).OrdConnected
Theorem: Finset.le_card_upper_inter_lower
Proof state before:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑𝒜 ∩ ↑ℬ).OrdConnected
Tactic:
exact h𝒜.ordConnected.inter hℬ.ordConnected
Proof state after:
no goals