awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
nil :
  LiftRelAux.{u, u} (α := Option (α × WSeq α)) (β := Option (α × WSeq α))
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (Computation.destruct (destruct (join (join WSeq.nil))))
    (Computation.destruct (destruct (join (map join WSeq.nil))))
nil₁ :
  ∀ (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    LiftRelAux
      (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          c1 = (s.append (S.append SS.join).join).destruct ∧
            c2 = (s.append (S.join.append (map join SS).join)).destruct)
      (cons S SS).join.join.destruct.destruct (map join (cons S SS)).join.destruct.destruct
nil₂ :
  ∀ (SS : WSeq (WSeq (WSeq α))),
    LiftRelAux
      (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
          c1 = (s.append (S.append SS.join).join).destruct ∧
            c2 = (s.append (S.join.append (map join SS).join)).destruct)
      SS.think.join.join.destruct.destruct (map join SS.think).join.destruct.destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    SS.join.join.destruct.destruct (map join SS).join.destruct.destruct

Tactic:
induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp

Premises used: Stream'.WSeq.cons, Stream'.WSeq.think, Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
s : WSeq α
S : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append nil ((cons s S).append SS.join).join).destruct.destruct
    (append nil ((cons s S).join.append (map join SS).join)).destruct.destruct

Tactic:
simpa using ⟨s, S, SS, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append nil (S.think.append SS.join).join).destruct.destruct
    (append nil (S.think.join.append (map join SS).join)).destruct.destruct

Tactic:
⟨nil, S, SS, ?_, ?_⟩

Premises used: Computation.LiftRelAux, And.intro, Exists.intro, Stream'.WSeq.nil
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
nil : (append WSeq.nil (S.think.append SS.join).join).destruct.tail = (append WSeq.nil (S.append SS.join).join).destruct
nil₁ :
  (append WSeq.nil (S.think.join.append (map join SS).join)).destruct.tail =
    (append WSeq.nil (S.join.append (map join SS).join)).destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (append WSeq.nil (S.think.append SS.join).join).destruct.destruct
    (append WSeq.nil (S.think.join.append (map join SS).join)).destruct.destruct

Tactic:
refine ⟨nil, S, SS, ?_, ?_⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (append nil (S.think.append SS.join).join).destruct.tail = (append nil (S.append SS.join).join).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (append nil (S.think.join.append (map join SS).join)).destruct.tail =
    (append nil (S.join.append (map join SS).join)).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
a : α
s : WSeq α
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    ((cons a s).append (S.append SS.join).join).destruct.destruct
    ((cons a s).append (S.join.append (map join SS).join)).destruct.destruct

Tactic:
simpa using ⟨s, S, SS, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS_1 : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
s : WSeq α
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    (s.think.append (S.append SS.join).join).destruct.destruct
    (s.think.append (S.join.append (map join SS).join)).destruct.destruct

Tactic:
simpa using ⟨s, S, SS, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h_1 :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
h :
  ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
    c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct
⊢ LiftRelAux
    (LiftRelO (fun (x1 x2 : α) ↦ x1 = x2) fun (s1 s2 : WSeq α) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (S : WSeq (WSeq α)) (SS : WSeq (WSeq (WSeq α))),
        c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct)
    c1.destruct c2.destruct

Tactic:
exact
    match c1, c2, h with
    | _, _, ⟨s, S, SS, rfl, rfl⟩ => by
      clear h
      induction s using WSeq.recOn with
      | nil =>
        induction S using WSeq.recOn with
        | nil =>
          simp only [nil_append, join_nil]
          induction SS using WSeq.recOn with
          | nil => simp
          | cons S SS => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
          | think SS => refine ⟨nil, nil, SS, ?_, ?_⟩ <;> simp
        | cons s S => simpa using ⟨s, S, SS, rfl, rfl⟩
        | think S => refine ⟨nil, S, SS, ?_, ?_⟩ <;> simp
      | cons a s => simpa using ⟨s, S, SS, rfl, rfl⟩
      | think s => simpa using ⟨s, S, SS, rfl, rfl⟩
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
simp : (map (map g) (map f s)).join.join ~ʷ join (map ((fun (y : WSeq β) ↦ (map g y).join) ∘ f) s)
⊢ (s.bind f).bind g ~ʷ s.bind ((fun (y : WSeq β) ↦ y.bind g) ∘ f)

Tactic:
simp only [bind, map_join]

Premises used: Stream'.WSeq.map_join, Stream'.WSeq.bind
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
rw : (map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join
⊢ (map (map g) (map f s)).join.join ~ʷ join (map ((fun (y : WSeq β) ↦ (map g y).join) ∘ f) s)

Tactic:
rw [← map_comp f (map g), ← Function.comp_def, comp_assoc, map_comp (map g ∘ f) join s]

Premises used: Stream'.WSeq.join, Stream'.WSeq.map_comp, Function.comp, Function.comp_def, Stream'.WSeq.map, Function.comp_assoc
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join

Tactic:
join_join (map (map g ∘ f) s)

Premises used: Function.comp, Stream'.WSeq.join_join, Stream'.WSeq.map
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (map (map g ∘ f) s).join.join ~ʷ (map join (map (map g ∘ f) s)).join

Tactic:
exact join_join (map (map g ∘ f) s)

Premises used: Function.comp, Stream'.WSeq.join_join, Stream'.WSeq.map
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind fun (x : α) ↦ (f x).bind g

Tactic:
bind_assoc_comp s f g

Premises used: Stream'.WSeq.join, Stream'.WSeq.bind_assoc_comp, Stream'.Seq.join, Stream'.WSeq.bind, Stream'.Seq.corec
-- Module: Mathlib.Data.WSeq.Relation
Goal:
α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind fun (x : α) ↦ (f x).bind g

Tactic:
exact bind_assoc_comp s f g

Premises used: Stream'.WSeq.bind_assoc_comp
-- Module: Mathlib.Data.ZMod.Aut
Goal:
n : ℕ
f : AddAut (ZMod n)
x : ZMod n
rw : x * (f : (a : ZMod n) → ZMod n) 1 = (f : (a : ZMod n) → ZMod n) x
rw₁ :
  HMul.hMul (α := ZMod n) (↑x.cast : ZMod n) ((f : (a : ZMod n) → ZMod n) 1) =
    (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
rw₂ :
  HSMul.hSMul (α := ℤ) (β := ZMod n) x.cast ((f : (a : ZMod n) → ZMod n) 1) =
    (f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)
rw₃ :
  Eq (α := ZMod n) ((f : (a : ZMod n) → ZMod n) (HSMul.hSMul (α := ℤ) (β := ZMod n) x.cast 1) : ZMod n)
    ((f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n) : ZMod n)
rw₄ rw₅ :
  Eq (α := ZMod n) ((f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n)) ((f : (a : ZMod n) → ZMod n) (↑x.cast : ZMod n))
⊢ (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x

Tactic:
rw [mul_comm, ← x.intCast_zmod_cast, ← zsmul_eq_mul, ← map_zsmul, zsmul_one]

Premises used: zsmul_eq_mul, mul_comm, ZMod.intCast_zmod_cast, zsmul_one, map_zsmul
-- Module: Mathlib.Data.ZMod.Aut
Goal:
n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
f : AddAut (ZMod n)
⊢ (AddAut.mulLeft : (a : (ZMod n)ˣ) → AddAut (ZMod n))
      ((fun (f : AddAut (ZMod n)) ↦
          Units.mkOfMulEqOne ((f : (a : ZMod n) → ZMod n) 1) ((f⁻¹ : (a : ZMod n) → ZMod n) 1) ⋯)
        f) =
    f

Tactic:
simp [DFunLike.ext_iff, Units.smul_def, h]

Premises used: DFunLike.ext_iff, Units.smul_def
-- Module: Mathlib.Data.ZMod.Aut
Goal:
n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
x : (ZMod n)ˣ
⊢ (fun (f : AddAut (ZMod n)) ↦ Units.mkOfMulEqOne ((f : (a : ZMod n) → ZMod n) 1) ((f⁻¹ : (a : ZMod n) → ZMod n) 1) ⋯)
      ((AddAut.mulLeft : (a : (ZMod n)ˣ) → AddAut (ZMod n)) x) =
    x

Tactic:
simp [Units.ext_iff, Units.smul_def]

Premises used: Units.ext_iff, Units.smul_def
-- Module: Mathlib.Data.ZMod.Aut
Goal:
n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), (f : (a : ZMod n) → ZMod n) 1 * x = (f : (a : ZMod n) → ZMod n) x
f g : AddAut (ZMod n)
⊢ Units.mkOfMulEqOne ((f * g : (a : ZMod n) → ZMod n) 1) (((f * g)⁻¹ : (a : ZMod n) → ZMod n) 1) ⋯ =
    Units.mkOfMulEqOne ((f : (a : ZMod n) → ZMod n) 1) ((f⁻¹ : (a : ZMod n) → ZMod n) 1) ⋯ *
      Units.mkOfMulEqOne ((g : (a : ZMod n) → ZMod n) 1) ((g⁻¹ : (a : ZMod n) → ZMod n) 1) ⋯

Tactic:
simp [Units.ext_iff, h]

Premises used: Units.ext_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ IsDomain (ZMod 0)

Tactic:
inferInstanceAs (IsDomain ℤ)

Premises used: _private.0.ZMod.instIsDomainOfNatNat._proof_1
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ CharZero (ZMod 0)

Tactic:
inferInstanceAs (CharZero ℤ)

Premises used: _private.0.ZMod.charZero._proof_1
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
zero : ∀ [NeZero (R := ℕ) 0] (a : ZMod 0), a.val < 0
succ : ∀ (n : ℕ) [NeZero (n + 1)] (a : ZMod (n + 1)), a.val < n + 1
⊢ a.val < n

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
inst : NeZero (R := ℕ) 0
a : ZMod 0
⊢ a.val < 0

Tactic:
cases NeZero.ne 0 rfl

Premises used: OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero (n + 1)
a : ZMod (n + 1)
⊢ a.val < n + 1

Tactic:
Fin.is_lt a

Premises used: Fin.is_lt, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero (n + 1)
a : ZMod (n + 1)
⊢ a.val < n + 1

Tactic:
exact Fin.is_lt a

Premises used: Fin.is_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
inst : NeZero n
a : ZMod n
⊢ a.val ≤ n

Tactic:
a.val_lt.le

Premises used: LT.lt.le, ZMod.val_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
⊢ val (n := 0) 1 = 1

Tactic:
rfl

Premises used: Int.natAbs, rfl, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ZMod 0
⊢ (-n).val = n.val

Tactic:
Int.natAbs_neg n

Premises used: Int.natAbs_neg, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
m n : ZMod 0
⊢ (m * n).val = m.val * n.val

Tactic:
Int.natAbs_mul m n

Premises used: Int.natAbs_mul, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n a : ℕ
zero : val (n := 0) (↑a : ZMod 0) = a % 0
succ : ∀ (n : ℕ), val (n := n + 1) (↑a : ZMod (n + 1)) = a % (n + 1)
⊢ val (n := n) (↑a : ZMod n) = a % n

Tactic:
cases n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
zero : val (n := 0) (↑a : ZMod 0) = a
⊢ val (n := 0) (↑a : ZMod 0) = a % 0

Tactic:
rw [Nat.mod_zero]

Premises used: Nat.mod_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
⊢ val (n := 0) (↑a : ZMod 0) = a

Tactic:
Int.natAbs_natCast a

Premises used: ZMod, Int.natAbs_natCast, ZMod.val
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a : ℕ
⊢ val (n := 0) (↑a : ZMod 0) = a

Tactic:
exact Int.natAbs_natCast a

Premises used: Int.natAbs_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a n : ℕ
⊢ val (n := n + 1) (↑a : ZMod (n + 1)) = a % (n + 1)

Tactic:
apply Fin.val_natCast

Premises used: Fin.val_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n a : ℕ
h : a < n
rwa : a % n = a
rwa₁ : a = a
rwa₂ : a < n
rwa₃ : a = a
rwa₄ rwa₅ rwa₆ : a < n
⊢ val (n := n) (↑a : ZMod n) = a

Tactic:
rwa [val_natCast, Nat.mod_eq_of_lt]

Premises used: Nat.mod_eq_of_lt, ZMod.val_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n a : ℕ
inst : a.AtLeastTwo
⊢ val (n := n) (OfNat.ofNat a) = OfNat.ofNat a % n

Tactic:
val_natCast ..

Premises used: ZMod.val_natCast
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n a : ℕ
inst : a.AtLeastTwo
han : a < n
⊢ val (n := n) (OfNat.ofNat a) = OfNat.ofNat a

Tactic:
val_natCast_of_lt han

Premises used: ZMod.val_natCast_of_lt
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ZMod 0
rw : n = 1 ∨ n = -1 ↔ Int.natAbs n = 1
rw₁ : n = 1 ∨ n = -1 ↔ n = (↑1 : ℤ) ∨ n = -(↑1 : ℤ)
rw₂ rw₃ : n = 1 ∨ n = -1 ↔ n = 1 ∨ n = -1
⊢ IsUnit n ↔ Int.natAbs n = 1

Tactic:
rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]

Premises used: Int.natAbs_eq_iff, Int.isUnit_iff, Nat.cast_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
h : IsUnit (M := ZMod 0) (↑n : ZMod 0)
rw : n % 0 = 1
rw₁ : val (n := 0) (↑n : ZMod 0) = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ n = 1

Tactic:
rw [← Nat.mod_zero n, ← val_natCast, val_unit'.mp h]

Premises used: Nat.mod_zero, ZMod.val_unit', ZMod.val_natCast, Iff.mp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n k : ℕ
zero : Eq (α := ZMod 0) (↑k : ZMod 0) 0 ↔ 0 ∣ k
succ : ∀ (n : ℕ), Eq (α := ZMod (n + 1)) (↑k : ZMod (n + 1)) 0 ↔ n + 1 ∣ k
⊢ Eq (α := ZMod n) (↑k : ZMod n) 0 ↔ n ∣ k

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.ZMod.Basic
Goal:
k : ℕ
⊢ Eq (α := ZMod 0) (↑k : ZMod 0) 0 ↔ 0 ∣ k

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
k n : ℕ
⊢ Eq (α := ZMod (n + 1)) (↑k : ZMod (n + 1)) 0 ↔ n + 1 ∣ k

Tactic:
Fin.natCast_eq_zero

Premises used: Fin.natCast_eq_zero, ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
k n : ℕ
⊢ Eq (α := ZMod (n + 1)) (↑k : ZMod (n + 1)) 0 ↔ n + 1 ∣ k

Tactic:
exact Fin.natCast_eq_zero

Premises used: Fin.natCast_eq_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Lean.Grind.IsCharP (ZMod n) n

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ addOrderOf (G := ZMod n) 1 = n

Tactic:
CharP.eq _ (CharP.addOrderOf_one _) (ZMod.charP n)

Premises used: CharP.addOrderOf_one, CharP.eq, ZMod.charP
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a n : ℕ
n0 : n ≠ 0
zero : addOrderOf (G := ZMod n) (↑0 : ZMod n) = n / n.gcd 0
succ : ∀ (a : ℕ), addOrderOf (G := ZMod n) (↑(a + 1) : ZMod n) = n / n.gcd (a + 1)
⊢ addOrderOf (G := ZMod n) (↑a : ZMod n) = n / n.gcd a

Tactic:
rcases a with - | a
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
n0 : n ≠ 0
⊢ addOrderOf (G := ZMod n) (↑0 : ZMod n) = n / n.gcd 0

Tactic:
simp only [Nat.cast_zero, addOrderOf_zero, Nat.gcd_zero_right,
      Nat.pos_of_ne_zero n0, Nat.div_self]

Premises used: Nat.gcd_zero_right, addOrderOf_zero, Nat.pos_of_ne_zero, Nat.div_self, Nat.cast_zero
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
n0 : n ≠ 0
a : ℕ
succ : addOrderOf (HSMul.hSMul (β := ZMod n) (a + 1) 1) = n / n.gcd (a + 1)
succ₁ : addOrderOf (G := ZMod n) 1 / (addOrderOf (G := ZMod n) 1).gcd a.succ = n / n.gcd (a + 1)
succ₂ succ₃ : n / n.gcd a.succ = n / n.gcd (a + 1)
⊢ addOrderOf (G := ZMod n) (↑(a + 1) : ZMod n) = n / n.gcd (a + 1)

Tactic:
rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a.succ_ne_zero, ZMod.addOrderOf_one]

Premises used: addOrderOf_nsmul', Nat.succ_ne_zero, Nat.smul_one_eq_cast, ZMod.addOrderOf_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
a n : ℕ
a0 : a ≠ 0
rw : addOrderOf (HSMul.hSMul (β := ZMod n) a 1) = n / n.gcd a
rw₁ : addOrderOf (G := ZMod n) 1 / (addOrderOf (G := ZMod n) 1).gcd a = n / n.gcd a
rw₂ rw₃ : n / n.gcd a = n / n.gcd a
⊢ addOrderOf (G := ZMod n) (↑a : ZMod n) = n / n.gcd a

Tactic:
rw [← Nat.smul_one_eq_cast, addOrderOf_nsmul' _ a0, ZMod.addOrderOf_one]

Premises used: addOrderOf_nsmul', Nat.smul_one_eq_cast, ZMod.addOrderOf_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
rw : CharP (ZMod n) n
⊢ ringChar (ZMod n) = n

Tactic:
rw [ringChar.eq_iff]

Premises used: ringChar.eq_iff
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ CharP (ZMod n) n

Tactic:
ZMod.charP n

Premises used: ZMod.charP
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ CharP (ZMod n) n

Tactic:
exact ZMod.charP n

Premises used: ZMod.charP
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
⊢ Eq (α := ZMod n) (↑n : ZMod n) 0

Tactic:
CharP.cast_eq_zero (ZMod n) n

Premises used: CharP.cast_eq_zero, ZMod
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
rw : Eq (α := ZMod (n + 1)) (↑(n + 1) : ZMod (n + 1)) 0
rw₁ rw₂ : Eq (α := ZMod (n + 1)) 0 0
⊢ HAdd.hAdd (α := ZMod (n + 1)) (↑n : ZMod (n + 1)) 1 = 0

Tactic:
rw [← Nat.cast_add_one, natCast_self (n + 1)]

Premises used: ZMod.natCast_self, HAdd.hAdd, OfNat.ofNat, Nat.cast_add_one
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p m n : ℕ
h : n ≤ m
obtain : ∀ (q : ℕ) (h : n ≤ n + q), HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) (n + q) = 0
⊢ HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) m = 0

Tactic:
obtain ⟨q, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n q : ℕ
h : n ≤ n + q
rw : (↑(p ^ n) : ZMod (p ^ n)) * HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) q = 0
⊢ HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) (n + q) = 0

Tactic:
rw [pow_add, ← Nat.cast_pow]

Premises used: pow_add, Nat.cast_pow
-- Module: Mathlib.Data.ZMod.Basic
Goal:
p n q : ℕ
h : n ≤ n + q
⊢ (↑(p ^ n) : ZMod (p ^ n)) * HPow.hPow (α := ZMod (p ^ n)) (↑p : ZMod (p ^ n)) q = 0

Tactic:
simp
-- Module: Mathlib.Data.ZMod.Basic
Goal:
n : ℕ
R : Type u_1
inst : AddGroupWithOne R
delta :
  Eq.{u_1 + 1} (α := R)
    ((match (motive := (x : ℕ) → ZMod x → R) n with
        | 0 => Int.cast
        | n.succ => fun (i : ZMod (n + 1)) ↦ (↑i.val : R))
        0 :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) (cast (n := n) 0) 0

Tactic:
delta ZMod.cast

Premises used: ZMod.cast