awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
zero :
  (↑(numDerangements (HAdd.hAdd (α := ℕ) 0 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑0 : ℤ) 1 * (↑(numDerangements 0) : ℤ) - HPow.hPow (α := ℤ) (β := ℕ) (-1) 0
succ :
  ∀ (n : ℕ)
    (hn :
      (↑(numDerangements (n + 1)) : ℤ) =
        HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n),
    (↑(numDerangements (n + 1 + 1)) : ℤ) =
      HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * (↑(numDerangements (n + 1)) : ℤ) - HPow.hPow (α := ℤ) (-1) (n + 1)
⊢ (↑(numDerangements (n + 1)) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑(numDerangements n) : ℤ) - HPow.hPow (α := ℤ) (-1) n

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
    ring

Premises used: Int.natCast_add, numDerangements_add_two, pow_succ, Int.natCast_mul
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hyp : ∀ m < n, card (↑(derangements (Fin m)) : Type) = numDerangements m
⊢ card (↑(derangements (Fin n)) : Type) = numDerangements n

Tactic:
_
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
ind :
  ∀ (n : ℕ) (hyp : ∀ m < n, card (↑(derangements (Fin m)) : Type) = numDerangements m),
    card (↑(derangements (Fin n)) : Type) = numDerangements n
⊢ card (↑(derangements (Fin n)) : Type) = numDerangements n

Tactic:
induction n using Nat.strongRecOn with | ind n hyp => _
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hyp : ∀ m < n, card (↑(derangements (Fin m)) : Type) = numDerangements m
ind :
  ∀ (hyp : ∀ m < 0, card (↑(derangements (Fin m)) : Type) = numDerangements m),
    card (↑(derangements (Fin 0)) : Type) = numDerangements 0
ind₁ :
  ∀ (hyp : ∀ m < HAdd.hAdd (α := ℕ) 0 1, card (↑(derangements (Fin m)) : Type) = numDerangements m),
    card (↑(derangements (Fin (HAdd.hAdd (α := ℕ) 0 1))) : Type) = numDerangements (HAdd.hAdd (α := ℕ) 0 1)
ind₂ :
  ∀ (n : ℕ) (hyp : ∀ m < n + 1 + 1, card (↑(derangements (Fin m)) : Type) = numDerangements m),
    card (↑(derangements (Fin (n + 1 + 1))) : Type) = numDerangements (n + 1 + 1)
⊢ card (↑(derangements (Fin n)) : Type) = numDerangements n

Tactic:
rcases n with _ | _ | n
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
hyp : ∀ m < 0, card (↑(derangements (Fin m)) : Type) = numDerangements m
⊢ card (↑(derangements (Fin 0)) : Type) = numDerangements 0

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
hyp : ∀ m < HAdd.hAdd (α := ℕ) 0 1, card (↑(derangements (Fin m)) : Type) = numDerangements m
⊢ card (↑(derangements (Fin (HAdd.hAdd (α := ℕ) 0 1))) : Type) = numDerangements (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hyp : ∀ m < n + 1 + 1, card (↑(derangements (Fin m)) : Type) = numDerangements m
ind : n + 1 < n + 1 + 1
ind₁ : n < n + 1 + 1
⊢ card (↑(derangements (Fin (n + 1 + 1))) : Type) = numDerangements (n + 1 + 1)

Tactic:
rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp, hyp]

Premises used: numDerangements_add_two, card_derangements_fin_add_two, mul_add
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hyp : ∀ m < n + 1 + 1, card (↑(derangements (Fin m)) : Type) = numDerangements m
⊢ n + 1 < n + 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hyp : ∀ m < n + 1 + 1, card (↑(derangements (Fin m)) : Type) = numDerangements m
⊢ n < n + 1 + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
rw : card (↑(derangements (Fin (card α))) : Type) = numDerangements (card α)
⊢ card.{u_2} (↑(derangements α) : Type u_2) = numDerangements (card α)

Tactic:
rw [← card_derangements_invariant (card_fin _)]

Premises used: Fintype.card_fin, card_derangements_invariant
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
⊢ card (↑(derangements (Fin (card α))) : Type) = numDerangements (card α)

Tactic:
card_derangements_fin_eq_numDerangements

Premises used: card_derangements_fin_eq_numDerangements
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
α : Type u_2
inst : Fintype α
inst_1 : DecidableEq α
⊢ card (↑(derangements (Fin (card α))) : Type) = numDerangements (card α)

Tactic:
exact card_derangements_fin_eq_numDerangements

Premises used: card_derangements_fin_eq_numDerangements
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
⊢ Eq (α := ℤ) (↑(numDerangements 0) : ℤ)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (0 - k)) : ℤ))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
succ :
  ∀ x ∈ Finset.range (n + 1),
    HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
      HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)
⊢ Eq (α := ℤ) (↑(numDerangements (n + 1)) : ℤ)
    (∑ k ∈ Finset.range (n + 1 + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n + 1 - k)) : ℤ))

Tactic:
rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]

Premises used: Finset.mul_sum, numDerangements_succ, tsub_self, sub_eq_add_neg, neg_one_mul, Nat.ascFactorial_zero, add_left_inj, Int.ofNat_one, mul_one, Finset.sum_range_succ, Finset.sum_congr, pow_succ', rfl
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ x ≤ n

Tactic:
have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
hn :
  Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
succ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x).succ) : ℤ)
succ₁ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1 + (n - x)) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₂ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + (n - x) + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₃ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((n + 1) * (x + 1).ascFactorial (n - x)) : ℤ)
succ₄ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * HMul.hMul (α := ℤ) (↑(n + 1) : ℤ) (↑((x + 1).ascFactorial (n - x)) : ℤ)
succ₅ :
  HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * (↑((x + 1).ascFactorial (n - x)) : ℤ))
succ₆ :
  HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * (↑((x + 1).ascFactorial (n - x)) : ℤ))
succ₇ succ₈ :
  HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑((x + 1).ascFactorial (n - x)) : ℤ))
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n - x)) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) x * (↑((x + 1).ascFactorial (n + 1 - x)) : ℤ)

Tactic:
rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]

Premises used: Int.natCast_add, Nat.ascFactorial_succ, add_right_comm, mul_left_comm, Int.natCast_mul, Nat.succ_sub, Nat.cast_one, add_tsub_cancel_of_le
-- Module: Mathlib.Combinatorics.Derangements.Finite
Goal:
n : ℕ
zero :
  Eq (α := ℤ) (↑(numDerangements 0) : ℤ)
    (∑ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (0 - k)) : ℤ))
succ :
  ∀ (n : ℕ)
    (hn :
      Eq (α := ℤ) (↑(numDerangements n) : ℤ)
        (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))),
    Eq (α := ℤ) (↑(numDerangements (n + 1)) : ℤ)
      (∑ k ∈ Finset.range (n + 1 + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n + 1 - k)) : ℤ))
⊢ Eq (α := ℤ) (↑(numDerangements n) : ℤ)
    (∑ k ∈ Finset.range (n + 1), HPow.hPow (α := ℤ) (-1) k * (↑((k + 1).ascFactorial (n - k)) : ℤ))

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self,
      Nat.ascFactorial_zero, Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg,
      add_left_inj, Finset.sum_congr rfl]
    -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
    intro x hx
    have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
    rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le,
      Int.natCast_mul, Int.natCast_add, mul_left_comm, Nat.cast_one]

Premises used: Finset.mul_sum, numDerangements_succ, Int.natCast_add, tsub_self, sub_eq_add_neg, neg_one_mul, Nat.ascFactorial_zero, Nat.ascFactorial_succ, add_right_comm, add_left_inj, mul_left_comm, Int.natCast_mul, Int.ofNat_one, mul_one, Nat.cast_one, Finset.sum_range_succ, Finset.sum_congr, pow_succ', rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
adj adj' : V → V → Bool
simp_rw :
  (Eq.{u_1 + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true) → adj = adj'
⊢ Eq.{u_1 + 1} (α := Digraph V) ((fun (x : V → V → Bool) ↦ ({ Adj := fun (v w : V) ↦ x v w = true } : Digraph V)) adj)
      ((fun (x : V → V → Bool) ↦ ({ Adj := fun (v w : V) ↦ x v w = true } : Digraph V)) adj') →
    adj = adj'

Tactic:
simp_rw [mk.injEq]

Premises used: Digraph.mk.injEq
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
adj adj' : V → V → Bool
h : Eq.{u_1 + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true
h₁ : ∀ (v w : V), adj v w = adj' v w
⊢ adj = adj'

Tactic:
funext v w
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
adj adj' : V → V → Bool
h : Eq.{u_1 + 1} (α := V → V → Prop) (fun (v w : V) ↦ adj v w = true) fun (v w : V) ↦ adj' v w = true
v w : V
⊢ adj v w = adj' v w

Tactic:
simpa only [eq_iff_iff, Bool.coe_iff_coe] using congr($h v w)

Premises used: Bool.coe_iff_coe, eq_iff_iff
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)

Tactic:
⟨Embedding.injective _, ?_⟩

Premises used: And.intro, Function.Embedding.injective, Function.Bijective
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
refine :
  Surjective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)

Tactic:
refine ⟨Embedding.injective _, ?_⟩
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
G : Digraph V
h : ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) = G
⊢ ∃ (a : V → V → Bool), (Digraph.mk' : (a : V → V → Bool) → Digraph V) a = G

Tactic:
use fun v w ↦ G.Adj v w

Premises used: Digraph.Adj
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
G : Digraph V
h :
  ∀ (v w : V),
    Digraph.Adj ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) v w ↔ G.Adj v w
⊢ ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) = G

Tactic:
ext v w
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
G : Digraph V
v w : V
⊢ Digraph.Adj ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) v w ↔ G.Adj v w

Tactic:
simp
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_1
inst : DecidableEq V
inst_1 : Fintype V
refine :
  Surjective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)
refine₁ : ∀ (G : Digraph V), ∃ (a : V → V → Bool), (Digraph.mk' : (a : V → V → Bool) → Digraph V) a = G
h : ∀ (G : Digraph V), ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) = G
h₁ :
  ∀ (G : Digraph V) (v w : V),
    Digraph.Adj ((Digraph.mk' : (a : V → V → Bool) → Digraph V) fun (v w : V) ↦ decide (G.Adj v w)) v w ↔ G.Adj v w
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := V → V → Bool) (β := Digraph V) (⇑Digraph.mk' : (a : V → V → Bool) → Digraph V)

Tactic:
classical
    refine ⟨Embedding.injective _, ?_⟩
    intro G
    use fun v w ↦ G.Adj v w
    ext v w
    simp
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
⊢ Injective.{u_2 + 1, u_2 + 1} (α := Digraph V) Adj

Tactic:
fun _ _ ↦ Digraph.ext

Premises used: Digraph.ext, Function.Injective
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
G H : Digraph V
⊢ G.Adj = H.Adj ↔ G = H

Tactic:
Digraph.ext_iff.symm

Premises used: Iff.symm, Digraph.ext_iff
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
⊢ Eq.{u_2 + 1} (α := (x y : Digraph V) → Prop) Digraph.IsSubgraph fun (x1 x2 : Digraph V) ↦ x1 ≤ x2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
x y : Digraph V
v w : V
⊢ (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
x y : Digraph V
v w : V
⊢ (x ⊓ y).Adj v w ↔ x.Adj v w ∧ y.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
G : Digraph V
v w : V
⊢ Gᶜ.Adj v w ↔ ¬G.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl, Not
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
x y : Digraph V
v w : V
⊢ (x \ y).Adj v w ↔ x.Adj v w ∧ ¬y.Adj v w

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
a b : V
s : Set (Digraph V)
⊢ (sSup s).Adj a b ↔ ∃ G ∈ s, G.Adj a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
a b : V
s : Set (Digraph V)
⊢ (sInf s).Adj a b ↔ ∀ G ∈ s, G.Adj a b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
a b : V
f : ι → Digraph V
⊢ Adj (⨆ (i : ι), f i) a b ↔ ∃ (i : ι), (f i).Adj a b

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
a b : V
f : ι → Digraph V
⊢ Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), (f i).Adj a b

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G_1 : Digraph V
a b : V
G : Digraph V
v w : V
h : (Digraph.completeDigraph V).Adj v w
tauto : ¬G.Adj v w → Gᶜ.Adj v w
⊢ (G ⊔ Gᶜ).Adj v w

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
ι_1 : Type u_2
κ : ι_1 → Type u_2
f : (a : ι_1) → κ a → Digraph V
Adj :
  ∀ (x x_1 : V),
    Digraph.Adj (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔
      Digraph.Adj (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1
⊢ Eq.{u_2 + 1} (α := Digraph V) (⨅ (a : ι_1), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a))

Tactic:
ext
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
ι_1 : Type u_2
κ : ι_1 → Type u_2
f : (a : ι_1) → κ a → Digraph V
x x_1 : V
⊢ Adj (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔ Adj (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1

Tactic:
simp [Classical.skolem]

Premises used: Classical.skolem
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
v w : V
⊢ Adj ⊤ v w

Tactic:
trivial

Premises used: trivial
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_2
v w : V
⊢ Adj ⊥ v w ↔ False

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_3
⊢ Digraph.completeDigraph V = ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
V : Type u_3
⊢ Digraph.emptyDigraph V = ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G_1 : Digraph V
a b : V
inst : IsEmpty V
G : Digraph V
Adj : G.Adj = Digraph.Adj ⊥
⊢ G = ⊥

Tactic:
ext1
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G_1 : Digraph V
a b : V
inst : IsEmpty V
G : Digraph V
⊢ G.Adj = Adj ⊥

Tactic:
congr!
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst : Nonempty V
h : Ne.{u_2 + 1} (α := Digraph V) ⊥ ⊤
⊢ Nontrivial.{u_2} (Digraph V)

Tactic:
use ⊥, ⊤
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst : Nonempty V
h : ∀ (v : V), Ne.{u_2 + 1} (α := Digraph V) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := Digraph V) ⊥ ⊤

Tactic:
have v := Classical.arbitrary V
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst : Nonempty V
v : V
⊢ Ne (α := Prop) ((fun (x : Digraph V) ↦ x.Adj v v) ⊥) ((fun (x : Digraph V) ↦ x.Adj v v) ⊤)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Digraph.Basic
Goal:
ι : Sort u_1
V : Type u_2
G : Digraph V
a b : V
inst : Nonempty V
v : V
⊢ Ne.{u_2 + 1} (α := Digraph V) ⊥ ⊤

Tactic:
exact ne_of_apply_ne (·.Adj v v) (by simp)

Premises used: ne_of_apply_ne
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
G : Digraph V
⊢ G.toSimpleGraphStrict ≤ G.toSimpleGraphInclusive

Tactic:
fun _ _ h ↦ ⟨h.1, Or.inl h.2.1⟩

Premises used: And.right, And.left, And.intro, Or.inl
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
⊢ Monotone.{u_1, u_1} (α := Digraph V) toSimpleGraphInclusive

Tactic:
fun _ _ h₁ _ _ h₂ ↦ ⟨h₂.1, h₂.2.imp (@h₁ _ _) (@h₁ _ _)⟩

Premises used: Monotone, And.right, And.left, And.intro, Or.imp
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
⊢ Monotone.{u_1, u_1} (α := Digraph V) toSimpleGraphStrict

Tactic:
fun _ _ h₁ _ _ h₂ ↦ ⟨h₂.1, h₁ h₂.2.1, h₁ h₂.2.2⟩

Premises used: Monotone, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphInclusive ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphInclusive ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
⊢ SimpleGraph.Adj (toSimpleGraphInclusive ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1

Tactic:
⟨And.left, fun h ↦ ⟨h.ne, Or.inl trivial⟩⟩

Premises used: trivial, SimpleGraph.Adj.ne, And.left, And.intro, Iff.intro, Or.inl
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
⊢ SimpleGraph.Adj (toSimpleGraphInclusive ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1

Tactic:
exact ⟨And.left, fun h ↦ ⟨h.ne, Or.inl trivial⟩⟩
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphStrict ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphStrict ⊤) ⊤

Tactic:
ext
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
⊢ SimpleGraph.Adj (toSimpleGraphStrict ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1

Tactic:
⟨And.left, fun h ↦ ⟨h.ne, trivial, trivial⟩⟩

Premises used: trivial, SimpleGraph.Adj.ne, And.left, And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
⊢ SimpleGraph.Adj (toSimpleGraphStrict ⊤) x x_1 ↔ SimpleGraph.Adj ⊤ x x_1

Tactic:
exact ⟨And.left, fun h ↦ ⟨h.ne, trivial, trivial⟩⟩
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphInclusive ⊥) x x_1 ↔ SimpleGraph.Adj ⊥ x x_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphInclusive ⊥) ⊥

Tactic:
ext
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
h_1 : SimpleGraph.Adj (toSimpleGraphInclusive ⊥) x x_1
left : x ≠ x_1
h : Adj ⊥ x x_1 ∨ Adj ⊥ x_1 x
inl : ∀ (h : Adj ⊥ x x_1), SimpleGraph.Adj ⊥ x x_1
inr : ∀ (h : Adj ⊥ x_1 x), SimpleGraph.Adj ⊥ x x_1
⊢ SimpleGraph.Adj ⊥ x x_1

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
⊢ SimpleGraph.Adj (toSimpleGraphInclusive ⊥) x x_1 ↔ SimpleGraph.Adj ⊥ x x_1

Tactic:
exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
Adj : ∀ (x x_1 : V), SimpleGraph.Adj (toSimpleGraphStrict ⊥) x x_1 ↔ SimpleGraph.Adj ⊥ x x_1
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (toSimpleGraphStrict ⊥) ⊥

Tactic:
ext
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
h_1 : SimpleGraph.Adj (toSimpleGraphStrict ⊥) x x_1
left : x ≠ x_1
h : Adj ⊥ x x_1 ∧ Adj ⊥ x_1 x
⊢ Adj ⊥ x x_1

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
h_1 : SimpleGraph.Adj (toSimpleGraphStrict ⊥) x x_1
left_1 : x ≠ x_1
h : Adj ⊥ x x_1 ∧ Adj ⊥ x_1 x
left : Adj ⊥ x x_1
⊢ Adj ⊥ x_1 x

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Digraph.Orientation
Goal:
V : Type u_1
x x_1 : V
⊢ SimpleGraph.Adj (toSimpleGraphStrict ⊥) x x_1 ↔ SimpleGraph.Adj ⊥ x x_1

Tactic:
exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
⊢ bell 0 = 1

Tactic:
rfl

Premises used: Multiset.bell, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
⊢ HPow.hPow (β := ℕ) x ! 0 * 0! * ∏ j ∈ Finset.range 0, (j * x + x - 1).choose (x - 1) = (x * 0)!

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
rw :
  x ! ^ c * x ! * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)
⊢ x ! ^ (c + 1) * (c + 1)! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)

Tactic:
rw [factorial_succ, pow_succ]

Premises used: Nat.factorial_succ, pow_succ
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ x ! ^ c * x ! * ((c + 1) * c !) * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1)

Tactic:
ring
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
x : ℕ
hx : x ≠ 0
c : ℕ
rw :
  x ! * (c + 1) * x ! ^ c * c ! *
      ((∏ x_1 ∈ Finset.range c, (x_1 * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1)) =
    (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1)
⊢ x ! * (c + 1) * x ! ^ c * c ! * ∏ j ∈ Finset.range (c + 1), (j * x + x - 1).choose (x - 1) =
    (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1)

Tactic:
rw [Finset.prod_range_succ]

Premises used: Finset.prod_range_succ