awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f : A.Copy B
a : α
⊢ Eq.{u_5 + 1} (α := β) ((f.toHom : (a : α) → β) a : β) ((f : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f : A →g B
hf : Injective.{u_4 + 1, u_5 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Eq (α := (a : α) → β) (⇑{ toHom := f, injective' := hf : A.Copy B } : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
a : α
x x_1 : (↑(A.neighborSet a) : Type u_4)
h :
  Eq.{u_5 + 1} (α := (↑(B.neighborSet ((f : (a : α) → β) a)) : Type u_5))
    ((fun (v : (↑(A.neighborSet a) : Type u_4)) ↦
        (Subtype.mk (p := fun (x : β) ↦ x ∈ B.neighborSet ((f : (a : α) → β) a)) ((f : (a : α) → β) (↑v : α)) ⋯ :
          { x : β // x ∈ B.neighborSet ((f : (a : α) → β) a) }))
      x)
    ((fun (v : (↑(A.neighborSet a) : Type u_4)) ↦
        (Subtype.mk (p := fun (x : β) ↦ x ∈ B.neighborSet ((f : (a : α) → β) a)) ((f : (a : α) → β) (↑v : α)) ⋯ :
          { x : β // x ∈ B.neighborSet ((f : (a : α) → β) a) }))
      x_1)
rw :
  ∀ (h : Eq.{u_5 + 1} (α := β) ((f : (a : α) → β) (↑x : α) : β) ((f : (a : α) → β) (↑x_1 : α) : β)),
    (↑x : α) = (↑x_1 : α)
⊢ x = x_1

Tactic:
rw [Subtype.mk_eq_mk] at h ⊢

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
a : α
x x_1 : (↑(A.neighborSet a) : Type u_4)
h : Eq.{u_5 + 1} (α := β) ((f : (a : α) → β) (↑x : α) : β) ((f : (a : α) → β) (↑x_1 : α) : β)
⊢ (↑x : α) = (↑x_1 : α)

Tactic:
f.injective h

Premises used: SimpleGraph.Copy.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
a : α
x x_1 : (↑(A.neighborSet a) : Type u_4)
h : Eq.{u_5 + 1} (α := β) ((f : (a : α) → β) (↑x : α) : β) ((f : (a : α) → β) (↑x_1 : α) : β)
⊢ (↑x : α) = (↑x_1 : α)

Tactic:
exact f.injective h

Premises used: SimpleGraph.Copy.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Eq (α := (a : V) → V) (⇑(id G) : (a : V) → V) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
injective' : Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ) (⇑(g.toHom.comp f.toHom) : (a : α) → γ)
⊢ A.Copy C

Tactic:
use g.toHom.comp f.toHom

Premises used: SimpleGraph.Copy.toHom, SimpleGraph.Hom.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
injective' :
  Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g.toHom : (a : β) → γ) (⇑f.toHom : (a : α) → β))
⊢ Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ) (⇑(g.toHom.comp f.toHom) : (a : α) → γ)

Tactic:
rw [Hom.coe_comp]

Premises used: SimpleGraph.Hom.coe_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g.toHom : (a : β) → γ) (⇑f.toHom : (a : α) → β))

Tactic:
g.injective.comp f.injective

Premises used: SimpleGraph.Copy.injective, Function.Injective.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
⊢ Injective.{u_4 + 1, u_6 + 1} (α := α) (β := γ)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g.toHom : (a : β) → γ) (⇑f.toHom : (a : α) → β))

Tactic:
exact g.injective.comp f.injective

Premises used: SimpleGraph.Copy.injective, Function.Injective.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
a : α
⊢ Eq.{u_6 + 1} (α := γ) ((g.comp f : (a : α) → γ) a : γ) ((g : (a : β) → γ) ((f : (a : α) → β) a : β) : γ)

Tactic:
RelHom.comp_apply g.toHom f.toHom a

Premises used: SimpleGraph.Copy.toHom, RelHom.comp_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
h :
  ∀ (x : α),
    Eq.{u_6 + 1} (α := γ) ((g.comp f : (a : α) → γ) x : γ)
      (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β) x : γ)
⊢ Eq (α := (a : α) → γ) (⇑(g.comp f) : (a : α) → γ)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
g : B.Copy C
f : A.Copy B
x : α
⊢ Eq.{u_6 + 1} (α := γ) ((g.comp f : (a : α) → γ) x : γ)
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β) x : γ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
h : G₁ ≤ G₂
⊢ Eq (α := (a : V) → V) (⇑(ofLE G₁ G₂ h) : (a : V) → V) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
a : ∀ (a : V), Eq (α := V) ((ofLE G G ⋯ : (a : V) → V) a : V) ((id G : (a : V) → V) a : V)
⊢ ofLE G G ⋯ = id G

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
a : V
⊢ Eq (α := V) ((ofLE G G ⋯ : (a : V) → V) a : V) ((id G : (a : V) → V) a : V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
a :
  ∀ (a : V),
    Eq (α := V) (((ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) : (a : V) → V) a : V) ((ofLE G₁ G₃ ⋯ : (a : V) → V) a : V)
⊢ (ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) = ofLE G₁ G₃ ⋯

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G₁ G₂ G₃ : SimpleGraph V
h₁₂ : G₁ ≤ G₂
h₂₃ : G₂ ≤ G₃
a : V
⊢ Eq (α := V) (((ofLE G₂ G₃ h₂₃).comp (ofLE G₁ G₂ h₁₂) : (a : V) → V) a : V) ((ofLE G₁ G₃ ⋯ : (a : V) → V) a : V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
map_rel_iff' :
  ∀ {a b : (↑A'.verts : Type u_4)},
    (Subgraph.map f.toHom A').coe.Adj
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          a)
        ((Equiv.Set.image (⇑f.toHom : (a : α) → β) A'.verts ⋯ :
            (a : (↑A'.verts : Type u_4)) → (↑(Subgraph.map f.toHom A').verts : Type u_5))
          b) ↔
      A'.coe.Adj a b
⊢ A'.coe ≃g (Subgraph.map f.toHom A').coe

Tactic:
use Equiv.Set.image f.toHom _ f.injective

Premises used: Equiv.Set.image, SimpleGraph.Copy.injective, SimpleGraph.Copy.toHom, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
h :
  ∀ (H' : B.Subgraph),
    Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' ↔
      Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
⊢ Eq.{u_5 + 1} (α := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)}

Tactic:
ext H'
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
h :
  Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' →
    Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
h₁ :
  Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H' →
    Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H'
⊢ Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H' ↔
    Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
f : A.Copy B
⊢ Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} f.toSubgraph

Tactic:
simpa [toSubgraph] using ⟨f.isoToSubgraph⟩

Premises used: SimpleGraph.Copy.toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
e : A ≃g H'.coe
⊢ Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H'

Tactic:
⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩

Premises used: SimpleGraph.Copy.mk, Set.Mem, setOf, SimpleGraph.Subgraph.hom, SimpleGraph.Iso.toHom, RelIso.injective, SimpleGraph.Subgraph.hom_injective, Function.Injective.comp, Exists.intro, Set.range, SimpleGraph.Hom.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
e : A ≃g H'.coe
h : { toHom := H'.hom.comp e.toHom, injective' := ⋯ : A.Copy B }.toSubgraph = H'
⊢ Membership.mem (γ := Set B.Subgraph) (Set.range (ι := A.Copy B) toSubgraph) H'

Tactic:
refine ⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
e : A ≃g H'.coe
⊢ { toHom := H'.hom.comp e.toHom, injective' := ⋯ : A.Copy B }.toSubgraph = H'

Tactic:
simp [toSubgraph, Subgraph.map_comp]

Premises used: SimpleGraph.Subgraph.map_comp, SimpleGraph.Copy.toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
hH' : Membership.mem (γ := Set B.Subgraph) {B' : B.Subgraph | Nonempty (A ≃g B'.coe)} H'
⊢ Membership.mem (γ := Set B.Subgraph) (Set.image (α := A.Copy B) toSubgraph Set.univ) H'

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
inst : Subsingleton (V → W)
⊢ Subsingleton (G.Copy H)

Tactic:
DFunLike.coe_injective.subsingleton

Premises used: Function.Injective.subsingleton, DFunLike.coe_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : Copy.{u_4, u_1} (α := α) ⊤ G
v w : α
h : G.Adj ((f.toEmbedding : (a : α) → V) v) ((f.toEmbedding : (a : α) → V) w)
⊢ Adj ⊤ v w

Tactic:
simpa using h.ne

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G ⊑ G

Tactic:
⟨.id G⟩

Premises used: SimpleGraph.Copy.id, Nonempty.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G ⊑ G

Tactic:
IsContained.refl G

Premises used: SimpleGraph.IsContained.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
h : G₁ ≤ G₂
⊢ G₁ ⊑ G₂

Tactic:
⟨.ofLE G₁ G₂ h⟩

Premises used: Nonempty.intro, SimpleGraph.Copy.ofLE
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
⊢ A ⊑ B → B ⊑ C → A ⊑ C

Tactic:
fun ⟨f⟩ ⟨g⟩ ↦ ⟨g.comp f⟩

Premises used: SimpleGraph.IsContained, Nonempty.intro, _private.0.SimpleGraph.IsContained.trans.match_1, SimpleGraph.Copy.comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
⊢ B ⊑ C → A ⊑ B → A ⊑ C

Tactic:
flip IsContained.trans

Premises used: SimpleGraph.IsContained.trans, flip
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B B' : SimpleGraph β
h_isub : A ⊑ B
h_sub : B ≤ B'
⊢ A ⊑ B'

Tactic:
h_isub.trans <| IsContained.of_le h_sub

Premises used: SimpleGraph.IsContained.trans, SimpleGraph.IsContained.of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
A' : SimpleGraph α
h_sub : A ≤ A'
h_isub : A' ⊑ B
⊢ A ⊑ B

Tactic:
(IsContained.of_le h_sub).trans h_isub

Premises used: SimpleGraph.IsContained.trans, SimpleGraph.IsContained.of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
α : Type u_4
β : Type u_5
G : SimpleGraph V
H : SimpleGraph W
A : SimpleGraph α
B : SimpleGraph β
e₁ : A ≃g H
e₂ : B ≃g G
⊢ A ⊑ B ↔ H ⊑ G

Tactic:
⟨.trans' ⟨e₂.toCopy⟩ ∘ .trans ⟨e₁.symm.toCopy⟩, .trans' ⟨e₂.symm.toCopy⟩ ∘ .trans ⟨e₁.toCopy⟩⟩

Premises used: SimpleGraph.IsContained.trans, Function.comp, Nonempty.intro, SimpleGraph.Iso.toCopy, Iff.intro, SimpleGraph.Iso.symm, SimpleGraph.IsContained.trans'
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
e₁ : A ≃g B
⊢ A ⊑ C ↔ B ⊑ C

Tactic:
isContained_congr e₁ .refl

Premises used: SimpleGraph.Iso.refl, SimpleGraph.isContained_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
e₂ : B ≃g C
⊢ A ⊑ B ↔ A ⊑ C

Tactic:
isContained_congr .refl e₂

Premises used: SimpleGraph.Iso.refl, SimpleGraph.isContained_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
inst : IsEmpty α
⊢ A ⊑ B

Tactic:
⟨⟨isEmptyElim, fun {a} ↦ isEmptyElim a⟩, isEmptyElim⟩

Premises used: SimpleGraph.Copy.mk, isEmptyElim, Nonempty.intro, RelHom.mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
B : SimpleGraph β
inst : Fintype α
inst_1 : Fintype β
⊢ IsContained.{u_4, u_5} (α := α) ⊥ B ↔ Fintype.card α ≤ Fintype.card β

Tactic:
⟨fun ⟨f⟩ ↦ Fintype.card_le_of_embedding f.toEmbedding,
    fun h ↦ ⟨Copy.bot (Function.Embedding.nonempty_of_card_le h).some⟩⟩

Premises used: Fintype.card, Nonempty.some, LE.le, Nonempty.intro, SimpleGraph.Copy.toEmbedding, Iff.intro, SimpleGraph.Copy.bot, _private.0.SimpleGraph.bot_isContained_iff_card_le.match_1, Fintype.card_le_of_embedding, Function.Embedding.nonempty_of_card_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
⊢ G'.coe ⊑ G

Tactic:
⟨G'.coeCopy⟩

Premises used: Nonempty.intro, SimpleGraph.Subgraph.coeCopy
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G.Copy H
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑(H.neighborSet ((f : (a : V) → W) v)) : Type u_2)
⊢ G.degree v ≤ H.degree ((f : (a : V) → W) v)

Tactic:
simpa [card_neighborSet_eq_degree] using
    Fintype.card_le_of_injective _ (f.mapNeighborSet v).injective

Premises used: Fintype.card_le_of_injective, SimpleGraph.card_neighborSet_eq_degree, SimpleGraph.Copy.mapNeighborSet, Function.Embedding.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
inl : IsEmpty V → G.maxDegree ≤ H.maxDegree
inr : Nonempty V → G.maxDegree ≤ H.maxDegree
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
cases isEmpty_or_nonempty V

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
h : IsEmpty V
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
h : Nonempty V
inr : ∀ (v : V) (h : G.maxDegree = G.degree v), G.maxDegree ≤ H.maxDegree
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
obtain ⟨v, h⟩ := exists_maximal_degree_vertex G

Premises used: SimpleGraph.exists_maximal_degree_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
h_1 : Nonempty V
v : V
h : G.maxDegree = G.degree v
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
grind [degree_le_maxDegree H (f v), f.degree_le v]

Premises used: SimpleGraph.degree_le_maxDegree, SimpleGraph.Copy.degree_le, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
h : G ⊑ H
have : ∀ (f : G.Copy H), G.maxDegree ≤ H.maxDegree
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
have ⟨f⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
h : G ⊑ H
f : G.Copy H
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
f.max_degree_le

Premises used: SimpleGraph.Copy.max_degree_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
h : G ⊑ H
f : G.Copy H
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
exact f.max_degree_le

Premises used: SimpleGraph.Copy.max_degree_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
G H : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
hle : G ≤ H
⊢ G.maxDegree ≤ H.maxDegree

Tactic:
IsContained.of_le hle |>.max_degree_le

Premises used: SimpleGraph.IsContained.max_degree_le, SimpleGraph.IsContained.of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
inl : IsEmpty W → G.minDegree ≤ H.minDegree
inr : Nonempty W → G.minDegree ≤ H.minDegree
⊢ G.minDegree ≤ H.minDegree

Tactic:
cases isEmpty_or_nonempty W

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : IsEmpty W
⊢ G.minDegree ≤ H.minDegree

Tactic:
simp [Function.isEmpty f]

Premises used: Function.isEmpty, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
⊢ G.minDegree ≤ H.minDegree

Tactic:
H.le_minDegree_of_forall_le_degree _ fun w ↦ ?_

Premises used: SimpleGraph.le_minDegree_of_forall_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
inr : ∀ (w : W), G.minDegree ≤ H.degree w
⊢ G.minDegree ≤ H.minDegree

Tactic:
refine H.le_minDegree_of_forall_le_degree _ fun w ↦ ?_

Premises used: SimpleGraph.le_minDegree_of_forall_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
w : W
inr : ∀ (v : V), G.minDegree ≤ H.degree ((f : (a : V) → W) v)
⊢ G.minDegree ≤ H.degree w

Tactic:
obtain ⟨v, rfl⟩ := hf w

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G.Copy H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
h : Nonempty W
v : V
inr : G.minDegree ≤ G.degree v
inr₁ inr₂ : G.minDegree ≤ G.minDegree
⊢ G.minDegree ≤ H.degree ((f : (a : V) → W) v)

Tactic:
grw [← f.degree_le, ← minDegree_le_degree]

Premises used: SimpleGraph.Copy.degree_le, SimpleGraph.minDegree_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst : Fintype V
inst_1 : Fintype W
inst_2 : DecidableRel G.Adj
inst_3 : DecidableRel H.Adj
f : G →g H
hf : Bijective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
⊢ G.minDegree ≤ H.minDegree

Tactic:
Copy.minDegree_le (f := ⟨f, hf.injective⟩) hf.surjective

Premises used: Function.Bijective.surjective, SimpleGraph.Copy.minDegree_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
⊢ ¬A.Free B ↔ A ⊑ B

Tactic:
not_not

Premises used: Classical.not_not
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
V : Type u_1
W : Type u_2
α : Type u_4
β : Type u_5
G : SimpleGraph V
H : SimpleGraph W
A : SimpleGraph α
B : SimpleGraph β
e₁ : A ≃g H
e₂ : B ≃g G
⊢ A.Free B ↔ H.Free G

Tactic:
(isContained_congr e₁ e₂).not

Premises used: Iff.not, SimpleGraph.isContained_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
e₁ : A ≃g B
⊢ A.Free C ↔ B.Free C

Tactic:
free_congr e₁ .refl

Premises used: SimpleGraph.Iso.refl, SimpleGraph.free_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
e₂ : B ≃g C
⊢ A.Free B ↔ A.Free C

Tactic:
free_congr .refl e₂

Premises used: SimpleGraph.Iso.refl, SimpleGraph.free_congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Copy
Goal:
α : Type u_4
β : Type u_5
A : SimpleGraph α
h : A ≠ ⊥
⊢ A.edgeSet.Nonempty

Tactic:
rw [← edgeSet_nonempty] at h

Premises used: SimpleGraph.edgeSet_nonempty