awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
⊢ #right.toLeft = #right

Tactic:
exact card_bij (fun j hj ↦ .inl j) (fun j hj ↦ by simpa using hj) (fun i hi j hj ↦ by simp)
          (fun j hj ↦ ⟨j.getLeft <| (hmem_right hj).left Sum.isLeft_inl, by simp [hj]⟩)

Premises used: Finset.card_bij, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
i : V
hi : i ∈ (↑left.toRight : Set V)
j : V
hj : j ∈ (↑right.toLeft : Set V)
refine_1 : ∀ (hi : Sum.inr i ∈ left) (j : V) (hj : j ∈ (↑right.toLeft : Set V)), G.Adj i j
⊢ G.Adj i j

Tactic:
rw [mem_coe, mem_toRight] at hi

Premises used: Finset.mem_toRight, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : j ∈ (↑right.toLeft : Set V)
⊢ Sum.inl j ∈ right

Tactic:
rw [mem_coe, mem_toLeft] at hj

Premises used: Finset.mem_toLeft, Finset.mem_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
r : V
hr : Sum.inl r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (β := V) (Sum.inl r) = true → r'.isLeft = true) ∧
      (Sum.isRight (β := V) (Sum.inl r) = true → r'.isRight = true)
i : V
hi : Sum.inr i ∈ left
j : V
hj : Sum.inl j ∈ right
⊢ G.Adj i j

Tactic:
simpa using h hi hj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
left right : Finset (V ⊕ V)
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))
l : V
hl : Sum.inr l ∈ left
hmem_left :
  ∀ {l' : V ⊕ V} (hl' : l' ∈ left),
    (Sum.isLeft (α := V) (Sum.inr l) = true → l'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr l) = true → l'.isRight = true)
r : V
hr : Sum.inr r ∈ right
hmem_right :
  ∀ {r' : V ⊕ V} (hr' : r' ∈ right),
    (Sum.isLeft (α := V) (Sum.inr r) = true → r'.isLeft = true) ∧
      (Sum.isRight (α := V) (Sum.inr r) = true → r'.isRight = true)
⊢ ∃ (left_1 : Finset V) (right_1 : Finset V),
    #left_1 = #left ∧ #right_1 = #right ∧ G.IsCompleteBetween (↑left_1 : Set V) (↑right_1 : Set V)

Tactic:
simpa using h hl hr
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
refine_2 :
  ∃ (left_1 : Finset (V ⊕ V)) (right_1 : Finset (V ⊕ V)),
    #left_1 = #left ∧
      #right_1 = #right ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left_1 : Set (V ⊕ V)) (↑right_1 : Set (V ⊕ V))
⊢ ∃ (left : Finset (V ⊕ V)) (right : Finset (V ⊕ V)),
    #left = Fintype.card α ∧
      #right = Fintype.card β ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left : Set (V ⊕ V)) (↑right : Set (V ⊕ V))

Tactic:
simp_rw [← card_left, ← card_right]
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
⊢ ∃ (left_1 : Finset (V ⊕ V)) (right_1 : Finset (V ⊕ V)),
    #left_1 = #left ∧
      #right_1 = #right ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left_1 : Set (V ⊕ V)) (↑right_1 : Set (V ⊕ V))

Tactic:
⟨left.map .inl, right.map .inr, card_map _, card_map _, fun i hi j hj ↦ ?_⟩

Premises used: Finset.card_map, Finset.map, Function.Embedding.inl, Function.Embedding.inr, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
refine_2 :
  ∀ (i : V ⊕ V) (hi : i ∈ (↑(map Function.Embedding.inl left) : Set (V ⊕ V))) (j : V ⊕ V)
    (hj : j ∈ (↑(map Function.Embedding.inr right) : Set (V ⊕ V))), G.bipartiteDoubleCover.Adj i j
⊢ ∃ (left_1 : Finset (V ⊕ V)) (right_1 : Finset (V ⊕ V)),
    #left_1 = #left ∧
      #right_1 = #right ∧ G.bipartiteDoubleCover.IsCompleteBetween (↑left_1 : Set (V ⊕ V)) (↑right_1 : Set (V ⊕ V))

Tactic:
refine ⟨left.map .inl, right.map .inr, card_map _, card_map _, fun i hi j hj ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
i : V ⊕ V
hi : i ∈ (↑(map Function.Embedding.inl left) : Set (V ⊕ V))
j : V ⊕ V
hj : j ∈ (↑(map Function.Embedding.inr right) : Set (V ⊕ V))
⊢ ∃ a ∈ left, Sum.inl a = i

Tactic:
simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj

Premises used: Finset.mem_map, Function.Embedding.inr_apply, Finset.mem_coe, Function.Embedding.inl_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
i : V ⊕ V
hi : i ∈ (↑(map Function.Embedding.inl left) : Set (V ⊕ V))
j : V ⊕ V
hj : j ∈ (↑(map Function.Embedding.inr right) : Set (V ⊕ V))
hi₁ : ∃ a ∈ left, Sum.inl a = i
⊢ ∃ a ∈ right, Sum.inr a = j

Tactic:
simp_rw [mem_coe, mem_map, Function.Embedding.inl_apply,
      Function.Embedding.inr_apply] at hi hj

Premises used: Finset.mem_map, Function.Embedding.inr_apply, Finset.mem_coe, Function.Embedding.inl_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
i j : V ⊕ V
hi : ∃ a ∈ left, Sum.inl a = i
hj : ∃ a ∈ right, Sum.inr a = j
refine_2 : ∀ (i' : V) (hi' : i' ∈ left) (hi : Sum.inl i' = i), G.bipartiteDoubleCover.Adj i j
⊢ G.bipartiteDoubleCover.Adj i j

Tactic:
obtain ⟨i', hi', hi⟩ := hi
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
i j : V ⊕ V
hj : ∃ a ∈ right, Sum.inr a = j
i' : V
hi' : i' ∈ left
hi : Sum.inl i' = i
refine_2 : ∀ (j' : V) (hj' : j' ∈ right) (hj : Sum.inr j' = j), G.bipartiteDoubleCover.Adj i j
⊢ G.bipartiteDoubleCover.Adj i j

Tactic:
obtain ⟨j', hj', hj⟩ := hj
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
α : Type u_2
β : Type u_3
inst : Finite α
inst_1 : Finite β
inst_2 : Nonempty α
inst_3 : Nonempty β
this_1 : Fintype α
this : Fintype β
h_1 :
  ∃ (left : Finset V) (right : Finset V),
    #left = Fintype.card α ∧ #right = Fintype.card β ∧ G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween (↑left : Set V) (↑right : Set V)
i j : V ⊕ V
i' : V
hi' : i' ∈ left
hi : Sum.inl i' = i
j' : V
hj' : j' ∈ right
hj : Sum.inr j' = j
⊢ G.bipartiteDoubleCover.Adj i j

Tactic:
simpa [← hi, ← hj] using h hi' hj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Disjoint.{u_1} (α := Set (V ⊕ V)) {v : V ⊕ V | v.isLeft = true} {w : V ⊕ V | w.isRight = true}

Tactic:
simp [Set.disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
⊢ ∀ ⦃v w : V ⊕ V⦄,
    G.bipartiteDoubleCover.Adj v w →
      Membership.mem (γ := Set (V ⊕ V)) {v : V ⊕ V | v.isLeft = true} v ∧
          Membership.mem (γ := Set (V ⊕ V)) {w : V ⊕ V | w.isRight = true} w ∨
        Membership.mem (γ := Set (V ⊕ V)) {w : V ⊕ V | w.isRight = true} v ∧
          Membership.mem (γ := Set (V ⊕ V)) {v : V ⊕ V | v.isLeft = true} w

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Bipartite
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.bipartiteDoubleCover.IsBipartite

Tactic:
isBipartiteWith_bipartiteDoubleCover.isBipartite

Premises used: SimpleGraph.IsBipartiteWith.isBipartite, SimpleGraph.isBipartiteWith_bipartiteDoubleCover
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
u v : M
⊢ (mulCayley s).Adj u v ↔ u ≠ v ∧ ∃ g ∈ s, u * g = v ∨ u = v * g

Tactic:
simp [mulCayley, ← exists_or, ← and_or_left, eq_comm]

Premises used: and_or_left, exists_or, eq_comm, SimpleGraph.mulCayley
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
simp :
  (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
⊢ (∀ (v w : M), (mulCayley s).Adj v w → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a

Tactic:
simp only [mulCayley_adj', ne_eq, and_imp, forall_exists_index]

Premises used: and_imp, forall_exists_index, ne_eq, SimpleGraph.mulCayley_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
mp :
  (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) → ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
mpr :
  (∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a) → ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
⊢ (∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
h : ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
g : M
hg : g ∈ s
a : M
ha : ¬a * g = a
⊢ G.Adj (a * g) a

Tactic:
h (a * g) a ha g hg (Or.inr rfl)

Premises used: HMul.hMul, Or.inr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
h : ∀ (v w : M), ¬v = w → ∀ x ∈ s, v * x = w ∨ v = w * x → G.Adj v w
g : M
hg : g ∈ s
a : M
ha : ¬a * g = a
⊢ G.Adj (a * g) a

Tactic:
exact h (a * g) a ha g hg (Or.inr rfl)

Premises used: HMul.hMul, Or.inr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
h : ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
v g : M
hg : g ∈ s
hvw : ¬v = v * g
⊢ G.Adj v (v * g)

Tactic:
(h g hg v (hvw ·.symm)).symm

Premises used: SimpleGraph.Adj.symm, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
h : ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
v g : M
hg : g ∈ s
hvw : ¬v = v * g
⊢ G.Adj v (v * g)

Tactic:
exact (h g hg v (hvw ·.symm)).symm

Premises used: SimpleGraph.Adj.symm, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
h : ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
w g : M
hg : g ∈ s
hvw : ¬w * g = w
⊢ G.Adj (w * g) w

Tactic:
h g hg w hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Mul M
G : SimpleGraph M
h : ∀ g ∈ s, ∀ (a : M), ¬a * g = a → G.Adj (a * g) a
w g : M
hg : g ∈ s
hvw : ¬w * g = w
⊢ G.Adj (w * g) w

Tactic:
exact h g hg w hvw
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Mul M
S : Set M
G : SimpleGraph M
⊢ (fun (x : Set M) ↦ mulCayley x) S ≤ G ↔
    S ≤ (fun (x : SimpleGraph M) ↦ ({g : M | ∀ (a : M), a * g ≠ a → x.Adj (a * g) a} : Set M)) G

Tactic:
simp [mulCayley_le_iff, Set.subset_def]

Premises used: Set.subset_def, SimpleGraph.mulCayley_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Mul M
⊢ Monotone (β := SimpleGraph M) fun (x : Set M) ↦ mulCayley x

Tactic:
(mulCayley_gc M).monotone_l

Premises used: SimpleGraph.mulCayley_gc, GaloisConnection.monotone_l
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Mul M
U V : Set M
hUV : U ⊆ V
⊢ mulCayley U ≤ mulCayley V

Tactic:
mulCayley_monotone hUV

Premises used: SimpleGraph.mulCayley_monotone
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Mul M
⊢ Eq.{u_1 + 1} (α := SimpleGraph M) (mulCayley ∅) ⊥

Tactic:
(mulCayley_gc M).l_bot

Premises used: SimpleGraph.mulCayley_gc, GaloisConnection.l_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Mul M
s₁ s₂ : Set M
⊢ mulCayley (s₁ ∪ s₂) = mulCayley s₁ ⊔ mulCayley s₂

Tactic:
(mulCayley_gc M).l_sup

Premises used: SimpleGraph.mulCayley_gc, GaloisConnection.l_sup
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Semigroup M
inst_1 : IsLeftCancelMul M
s : Set M
u v d : M
⊢ (mulCayley s).Adj (d * u) (d * v) ↔ (mulCayley s).Adj u v

Tactic:
simp [mulCayley_adj', mul_assoc]

Premises used: mul_assoc, SimpleGraph.mulCayley_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
nth_rw : mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})
⊢ mulCayley (s \ {1}) = mulCayley s

Tactic:
nth_rw 2 [← Set.diff_union_inter s {1}]

Premises used: Set.diff_union_inter, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
rw : mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1} ∪ s ∩ {1})

Tactic:
rw [mulCayley_union]

Premises used: SimpleGraph.mulCayley_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
Adj : ∀ (u v : M), (mulCayley (s \ {1})).Adj u v ↔ (mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})).Adj u v
⊢ mulCayley (s \ {1}) = mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})

Tactic:
ext u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
u v : M
⊢ (mulCayley (s \ {1})).Adj u v ↔ (mulCayley (s \ {1}) ⊔ mulCayley (s ∩ {1})).Adj u v

Tactic:
simp +contextual [mulCayley_adj']

Premises used: SimpleGraph.mulCayley_adj'
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : MulOneClass M
⊢ mulCayley (insert 1 s) = mulCayley s

Tactic:
simp [← Set.union_singleton, ← mulCayley_erase_one]

Premises used: SimpleGraph.mulCayley_erase_one, Set.union_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : MulOneClass M
rw : Eq (α := SimpleGraph M) (mulCayley ({1} \ {1})) ⊥
rw₁ : Eq.{u_1 + 1} (α := SimpleGraph M) (mulCayley ∅) ⊥
rw₂ rw₃ : Eq.{u_1 + 1} (α := SimpleGraph M) ⊥ ⊥
⊢ Eq (α := SimpleGraph M) (mulCayley {1}) ⊥

Tactic:
rw [← mulCayley_erase_one, Set.diff_self, mulCayley_empty]

Premises used: SimpleGraph.mulCayley_empty, SimpleGraph.mulCayley_erase_one, Set.diff_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Group M
u v : M
⊢ (mulCayley s).Adj u v ↔ u ≠ v ∧ (u⁻¹ * v ∈ s ∨ v⁻¹ * u ∈ s)

Tactic:
simp [mulCayley_adj', ← eq_inv_mul_iff_mul_eq (b := u), ← inv_mul_eq_iff_eq_mul (a := v),
    and_or_left, exists_or]

Premises used: and_or_left, exists_or, eq_inv_mul_iff_mul_eq, SimpleGraph.mulCayley_adj', inv_mul_eq_iff_eq_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Group M
Adj : ∀ (u v : M), (mulCayley s⁻¹).Adj u v ↔ (mulCayley s).Adj u v
⊢ mulCayley s⁻¹ = mulCayley s

Tactic:
ext u v
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
s : Set M
inst : Group M
u v : M
⊢ (mulCayley s⁻¹).Adj u v ↔ (mulCayley s).Adj u v

Tactic:
simp [mulCayley_adj, or_comm]

Premises used: SimpleGraph.mulCayley_adj, or_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Group M
Adj : ∀ (x x_1 : M), SimpleGraph.Adj (mulCayley Set.univ) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph M) (mulCayley Set.univ) ⊤

Tactic:
ext _ _
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Group M
x x_1 : M
⊢ Adj (mulCayley Set.univ) x x_1 ↔ Adj ⊤ x x_1

Tactic:
simp [mulCayley_adj]

Premises used: SimpleGraph.mulCayley_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Cayley
Goal:
M : Type u_1
inst : Group M
⊢ Eq (α := SimpleGraph M) (mulCayley {1}ᶜ) ⊤

Tactic:
simp [Set.compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
Adj : ∀ (u v : G), (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v
⊢ circulantGraph s = circulantGraph (s \ {0})

Tactic:
ext (u v : G)
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
Adj : u ≠ v → (u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0})
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v

Tactic:
simp only [circulantGraph, fromRel_adj, and_congr_right_iff]

Premises used: and_congr_right_iff, SimpleGraph.circulantGraph, SimpleGraph.fromRel_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
Adj : u - v ∈ s ∨ v - u ∈ s → u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}
Adj₁ : u - v ∈ s \ {0} ∨ v - u ∈ s \ {0} → u - v ∈ s ∨ v - u ∈ s
⊢ u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
apply Iff.intro

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
Or.inl ⟨h1, sub_ne_zero_of_ne h⟩

Premises used: sub_ne_zero_of_ne, And.intro, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : u - v ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
exact Or.inl ⟨h1, sub_ne_zero_of_ne h⟩

Premises used: Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Circulant
Goal:
G : Type u_1
inst : AddGroup G
s : Set G
u v : G
h : u ≠ v
h1 : v - u ∈ s
⊢ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0}

Tactic:
Or.inr ⟨h1, sub_ne_zero_of_ne h.symm⟩

Premises used: Ne.symm, sub_ne_zero_of_ne, And.intro, Or.inr