awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Inv F
inst_2 : Inv β
inst_3 : IsInvApply F α β
f : F
x : α
⊢ Eq.{u_6 + 1} (α := β) ((f⁻¹ : (a : α) → β) x : β) ((⇑f : (a : α) → β)⁻¹ x : β)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : SMul M F
inst_2 : SMul M β
inst_3 : IsSMulApply M F α β
n : M
f : F
h : ∀ (x : α), (n • f : (a : α) → β) x = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) x
⊢ (⇑(n • f) : (a : α) → β) = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β)

Tactic:
ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : SMul M F
inst_2 : SMul M β
inst_3 : IsSMulApply M F α β
n : M
f : F
x : α
⊢ (n • f : (a : α) → β) x = HSMul.hSMul (β := (a : α) → β) n (⇑f : (a : α) → β) x

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Pow F M
inst_2 : Pow β M
inst_3 : IsPowApply M F α β
f : F
n : M
h : ∀ (x : α), (f ^ n : (a : α) → β) x = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) n x
⊢ (⇑(f ^ n) : (a : α) → β) = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) n

Tactic:
ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
M : Type u_1
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Pow F M
inst_2 : Pow β M
inst_3 : IsPowApply M F α β
f : F
n : M
x : α
⊢ (f ^ n : (a : α) → β) x = HPow.hPow (α := (a : α) → β) (⇑f : (a : α) → β) n x

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : One F'
inst_2 : IsOneApplyEqSelf F' α
h : ∀ (x : α), (1 : (a : α) → α) x = id x
⊢ Eq.{u_5 + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id

Tactic:
ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : One F'
inst_2 : IsOneApplyEqSelf F' α
x : α
⊢ (1 : (a : α) → α) x = id x

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : Mul F'
inst_2 : IsMulApplyEqComp F' α
f g : F'
h :
  ∀ (x : α),
    Eq (α := α) ((f * g : (a : α) → α) x : α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) x : α)
⊢ Eq.{u_5 + 1} (α := α → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))

Tactic:
ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : Mul F'
inst_2 : IsMulApplyEqComp F' α
f g : F'
x : α
⊢ Eq (α := α) ((f * g : (a : α) → α) x : α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : NatCast F'
inst_2 : One F'
inst_3 : SMul Nat α
inst_4 : SMul Nat F'
inst_5 : IsSMulApply Nat F' α α
inst_6 : IsNatCastApply F' α
inst_7 : IsOneApplyEqSelf F' α
n : Nat
h : ∀ (x : α), Eq (α := α) (((↑n : F') : (a : α) → α) x : α) ((HSMul.hSMul (β := F') n 1 : (a : α) → α) x : α)
⊢ (↑n : F') = HSMul.hSMul (β := F') n 1

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : NatCast F'
inst_2 : One F'
inst_3 : SMul Nat α
inst_4 : SMul Nat F'
inst_5 : IsSMulApply Nat F' α α
inst_6 : IsNatCastApply F' α
inst_7 : IsOneApplyEqSelf F' α
n : Nat
⊢ ∀ (x : α), Eq (α := α) (((↑n : F') : (a : α) → α) x : α) ((HSMul.hSMul (β := F') n 1 : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : IntCast F'
inst_2 : One F'
inst_3 : SMul Int α
inst_4 : SMul Int F'
inst_5 : IsSMulApply Int F' α α
inst_6 : IsIntCastApply F' α
inst_7 : IsOneApplyEqSelf F' α
n : Int
h : ∀ (x : α), Eq (α := α) (((↑n : F') : (a : α) → α) x : α) ((HSMul.hSMul (β := F') n 1 : (a : α) → α) x : α)
⊢ (↑n : F') = HSMul.hSMul (β := F') n 1

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F' : Type u_4
α : Type u_5
inst : FunLike F' α α
inst_1 : IntCast F'
inst_2 : One F'
inst_3 : SMul Int α
inst_4 : SMul Int F'
inst_5 : IsSMulApply Int F' α α
inst_6 : IsIntCastApply F' α
inst_7 : IsOneApplyEqSelf F' α
n : Int
⊢ ∀ (x : α), Eq (α := α) (((↑n : F') : (a : α) → α) x : α) ((HSMul.hSMul (β := F') n 1 : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Module
Goal:
M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M β
inst_1 : SMul M' β
inst_2 : SMul M F
inst_3 : SMul M' F
inst_4 : IsSMulApply M F α β
inst_5 : IsSMulApply M' F α β
inst_6 : SMul M M'
inst_7 : IsScalarTower M M' β
x : M
x_1 : M'
x_2 : F
h : ∀ (x_3 : α), Eq.{u_5 + 1} (α := β) (((x • x_1) • x_2 : (a : α) → β) x_3 : β) ((x • x_1 • x_2 : (a : α) → β) x_3 : β)
⊢ (x • x_1) • x_2 = x • x_1 • x_2

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Module
Goal:
M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M β
inst_1 : SMul M' β
inst_2 : SMul M F
inst_3 : SMul M' F
inst_4 : IsSMulApply M F α β
inst_5 : IsSMulApply M' F α β
inst_6 : SMul M M'
inst_7 : IsScalarTower M M' β
x : M
x_1 : M'
x_2 : F
⊢ ∀ (x_3 : α), Eq.{u_5 + 1} (α := β) (((x • x_1) • x_2 : (a : α) → β) x_3 : β) ((x • x_1 • x_2 : (a : α) → β) x_3 : β)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Module
Goal:
M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M β
inst_1 : SMul M' β
inst_2 : SMul M F
inst_3 : SMul M' F
inst_4 : IsSMulApply M F α β
inst_5 : IsSMulApply M' F α β
inst_6 : SMulCommClass M M' β
x : M
x_1 : M'
x_2 : F
h : ∀ (x_3 : α), Eq.{u_5 + 1} (α := β) ((x • x_1 • x_2 : (a : α) → β) x_3 : β) ((x_1 • x • x_2 : (a : α) → β) x_3 : β)
⊢ x • x_1 • x_2 = x_1 • x • x_2

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Module
Goal:
M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M β
inst_1 : SMul M' β
inst_2 : SMul M F
inst_3 : SMul M' F
inst_4 : IsSMulApply M F α β
inst_5 : IsSMulApply M' F α β
inst_6 : SMulCommClass M M' β
x : M
x_1 : M'
x_2 : F
⊢ ∀ (x_3 : α), Eq.{u_5 + 1} (α := β) ((x • x_1 • x_2 : (a : α) → β) x_3 : β) ((x_1 • x • x_2 : (a : α) → β) x_3 : β)

Tactic:
simp [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Data.FunLike.Module
Goal:
M : Type u_1
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M F
inst_1 : SMul.{u_1, u_3} Mᵐᵒᵖ F
inst_2 : SMul M β
inst_3 : SMul.{u_1, u_5} Mᵐᵒᵖ β
inst_4 : IsCentralScalar M β
inst_5 : IsSMulApply M F α β
inst_6 : IsSMulApply.{u_1, u_3, u_4, u_5} Mᵐᵒᵖ F α β
a : M
b : F
h : ∀ (x : α), Eq.{u_5 + 1} (α := β) ((MulOpposite.op a • b : (a : α) → β) x : β) ((a • b : (a : α) → β) x : β)
⊢ MulOpposite.op a • b = a • b

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Module
Goal:
M : Type u_1
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M F
inst_1 : SMul.{u_1, u_3} Mᵐᵒᵖ F
inst_2 : SMul M β
inst_3 : SMul.{u_1, u_5} Mᵐᵒᵖ β
inst_4 : IsCentralScalar M β
inst_5 : IsSMulApply M F α β
inst_6 : IsSMulApply.{u_1, u_3, u_4, u_5} Mᵐᵒᵖ F α β
a : M
b : F
⊢ ∀ (x : α), Eq.{u_5 + 1} (α := β) ((MulOpposite.op a • b : (a : α) → β) x : β) ((a • b : (a : α) → β) x : β)

Tactic:
simp [op_smul_eq_smul]

Premises used: IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x x_1 x_2 : F
h : ∀ (x_3 : α), Eq (α := α) ((x * x_1 * x_2 : (a : α) → α) x_3 : α) ((x * (x_1 * x_2) : (a : α) → α) x_3 : α)
⊢ x * x_1 * x_2 = x * (x_1 * x_2)

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x x_1 x_2 : F
⊢ ∀ (x_3 : α), Eq (α := α) ((x * x_1 * x_2 : (a : α) → α) x_3 : α) ((x * (x_1 * x_2) : (a : α) → α) x_3 : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
h : ∀ (x_1 : α), Eq (α := α) ((1 * x : (a : α) → α) x_1 : α) ((x : (a : α) → α) x_1 : α)
⊢ 1 * x = x

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
⊢ ∀ (x_1 : α), Eq (α := α) ((1 * x : (a : α) → α) x_1 : α) ((x : (a : α) → α) x_1 : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
h : ∀ (x_1 : α), Eq (α := α) ((x * 1 : (a : α) → α) x_1 : α) ((x : (a : α) → α) x_1 : α)
⊢ x * 1 = x

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
⊢ ∀ (x_1 : α), Eq (α := α) ((x * 1 : (a : α) → α) x_1 : α) ((x : (a : α) → α) x_1 : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
h : ∀ (x_1 : α), Eq (α := α) ((0 * x : (a : α) → α) x_1 : α) ((0 : (a : α) → α) x_1 : α)
⊢ 0 * x = 0

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
⊢ ∀ (x_1 : α), Eq (α := α) ((0 * x : (a : α) → α) x_1 : α) ((0 : (a : α) → α) x_1 : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
f : F
h : ∀ (x : α), Eq (α := α) ((f * 0 : (a : α) → α) x : α) ((0 : (a : α) → α) x : α)
⊢ f * 0 = 0

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
f : F
⊢ ∀ (x : α), Eq (α := α) ((f * 0 : (a : α) → α) x : α) ((0 : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
f g h : F
h₁ : ∀ (x : α), Eq (α := α) ((f * (g + h) : (a : α) → α) x : α) ((f * g + f * h : (a : α) → α) x : α)
⊢ f * (g + h) = f * g + f * h

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
f g h : F
⊢ ∀ (x : α), Eq (α := α) ((f * (g + h) : (a : α) → α) x : α) ((f * g + f * h : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
x x_1 x_2 : F
h : ∀ (x_3 : α), Eq (α := α) (((x + x_1) * x_2 : (a : α) → α) x_3 : α) ((x * x_2 + x_1 * x_2 : (a : α) → α) x_3 : α)
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
x x_1 x_2 : F
⊢ ∀ (x_3 : α), Eq (α := α) (((x + x_1) * x_2 : (a : α) → α) x_3 : α) ((x * x_2 + x_1 * x_2 : (a : α) → α) x_3 : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
h : ∀ (x : α), Eq (α := α) ((↑0 : (a : α) → α) x : α) ((0 : (a : α) → α) x : α)
⊢ Eq.{u_1 + 1} (α := F) (↑0) 0

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
⊢ ∀ (x : α), Eq (α := α) ((↑0 : (a : α) → α) x : α) ((0 : (a : α) → α) x : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
n : ℕ
h : ∀ (x : α), Eq (α := α) ((↑(n + 1) : (a : α) → α) x : α) ((HAdd.hAdd (α := F) (↑n) 1 : (a : α) → α) x : α)
⊢ ↑(n + 1) = HAdd.hAdd (α := F) (↑n) 1

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
n : ℕ
⊢ ∀ (x : α), Eq (α := α) ((↑(n + 1) : (a : α) → α) x : α) ((HAdd.hAdd (α := F) (↑n) 1 : (a : α) → α) x : α)

Tactic:
simp [succ_nsmul]

Premises used: succ_nsmul
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : Neg F
inst_6 : Sub F
inst_7 : AddCommGroup α
inst_8 : IsZeroApply F α α
inst_9 : IsAddApply F α α
inst_10 : IsOneApplyEqSelf F α
inst_11 : IsMulApplyEqComp F α
inst_12 : IsNegApply F α α
inst_13 : IsSubApply F α α
inst_14 : SMul ℕ F
inst_15 : IsSMulApply ℕ F α α
inst_16 : SMul ℤ F
inst_17 : IsSMulApply ℤ F α α
inst_18 : AddMonoidHomClass F α α
inst_19 : NatCast F
inst_20 : IsNatCastApply F α
inst_21 : IntCast F
inst_22 : IsIntCastApply F α
x : ℕ
h : ∀ (x_1 : α), Eq (α := α) ((IntCast.intCast (↑x : ℤ) : (a : α) → α) x_1 : α) (((↑x : F) : (a : α) → α) x_1 : α)
⊢ Eq.{u_1 + 1} (α := F) (IntCast.intCast (↑x : ℤ)) (↑x : F)

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : Neg F
inst_6 : Sub F
inst_7 : AddCommGroup α
inst_8 : IsZeroApply F α α
inst_9 : IsAddApply F α α
inst_10 : IsOneApplyEqSelf F α
inst_11 : IsMulApplyEqComp F α
inst_12 : IsNegApply F α α
inst_13 : IsSubApply F α α
inst_14 : SMul ℕ F
inst_15 : IsSMulApply ℕ F α α
inst_16 : SMul ℤ F
inst_17 : IsSMulApply ℤ F α α
inst_18 : AddMonoidHomClass F α α
inst_19 : NatCast F
inst_20 : IsNatCastApply F α
inst_21 : IntCast F
inst_22 : IsIntCastApply F α
x : ℕ
⊢ ∀ (x_1 : α), Eq (α := α) ((IntCast.intCast (↑x : ℤ) : (a : α) → α) x_1 : α) (((↑x : F) : (a : α) → α) x_1 : α)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : Neg F
inst_6 : Sub F
inst_7 : AddCommGroup α
inst_8 : IsZeroApply F α α
inst_9 : IsAddApply F α α
inst_10 : IsOneApplyEqSelf F α
inst_11 : IsMulApplyEqComp F α
inst_12 : IsNegApply F α α
inst_13 : IsSubApply F α α
inst_14 : SMul ℕ F
inst_15 : IsSMulApply ℕ F α α
inst_16 : SMul ℤ F
inst_17 : IsSMulApply ℤ F α α
inst_18 : AddMonoidHomClass F α α
inst_19 : NatCast F
inst_20 : IsNatCastApply F α
inst_21 : IntCast F
inst_22 : IsIntCastApply F α
n : ℕ
h :
  ∀ (x : α), Eq (α := α) ((IntCast.intCast (Int.negSucc n) : (a : α) → α) x : α) ((-(↑(n + 1) : F) : (a : α) → α) x : α)
⊢ Eq.{u_1 + 1} (α := F) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : F))

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Data.FunLike.Ring
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : Neg F
inst_6 : Sub F
inst_7 : AddCommGroup α
inst_8 : IsZeroApply F α α
inst_9 : IsAddApply F α α
inst_10 : IsOneApplyEqSelf F α
inst_11 : IsMulApplyEqComp F α
inst_12 : IsNegApply F α α
inst_13 : IsSubApply F α α
inst_14 : SMul ℕ F
inst_15 : IsSMulApply ℕ F α α
inst_16 : SMul ℤ F
inst_17 : IsSMulApply ℤ F α α
inst_18 : AddMonoidHomClass F α α
inst_19 : NatCast F
inst_20 : IsNatCastApply F α
inst_21 : IntCast F
inst_22 : IsIntCastApply F α
n : ℕ
⊢ ∀ (x : α), Eq (α := α) ((IntCast.intCast (Int.negSucc n) : (a : α) → α) x : α) ((-(↑(n + 1) : F) : (a : α) → α) x : α)

Tactic:
simp [succ_nsmul]

Premises used: succ_nsmul
-- Module: Mathlib.Data.Holor
Goal:
ds₁ ds₂ is : List ℕ
eq : ds₁ = ds₂
h : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁
subst :
  (↑(cast ⋯ (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁) is h)) : List ℕ) = is
⊢ (↑(cast ⋯ (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁) is h)) : List ℕ) = is

Tactic:
subst eq
-- Module: Mathlib.Data.Holor
Goal:
ds₁ is : List ℕ
h : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁
⊢ (↑(cast ⋯ (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁) is h)) : List ℕ) = is

Tactic:
rfl
-- Module: Mathlib.Data.Holor
Goal:
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ (↑(take (ds₂ := ds₂ ++ ds₃)
          (assocRight
            (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)) is h))) :
      List ℕ) =
    (↑(take (ds₂ := ds₂)
          (take (ds₂ := ds₃)
            (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)) is h))) :
      List ℕ)

Tactic:
simp [assocRight, take, cast_type, List.take_take, Nat.le_add_right]

Premises used: Nat.le_add_right, HolorIndex.assocRight, HolorIndex.cast_type, List.take_take, HolorIndex.take
-- Module: Mathlib.Data.Holor
Goal:
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ (↑(take (ds₂ := ds₃)
          (drop (ds₁ := ds₁)
            (assocRight
              (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)) is
                h)))) :
      List ℕ) =
    (↑(drop (ds₁ := ds₁)
          (take (ds₂ := ds₃)
            (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)) is h))) :
      List ℕ)

Tactic:
simp [assocRight, take, drop, cast_type, List.drop_take]

Premises used: List.drop_take, HolorIndex.assocRight, HolorIndex.cast_type, HolorIndex.take, HolorIndex.drop
-- Module: Mathlib.Data.Holor
Goal:
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ (↑(drop (ds₁ := ds₂)
          (drop (ds₁ := ds₁)
            (assocRight
              (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)) is
                h)))) :
      List ℕ) =
    (↑(drop (ds₁ := ds₁ ++ ds₂)
          (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)) is h)) :
      List ℕ)

Tactic:
simp [assocRight, drop, cast_type, List.drop_drop]

Premises used: List.drop_drop, HolorIndex.assocRight, HolorIndex.cast_type, HolorIndex.drop
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ : List ℕ
eq : ds₁ = ds₂
a : Holor α ds₁
subst : cast ⋯ a = fun (t : HolorIndex ds₁) ↦ a (cast ⋯ t)
⊢ cast ⋯ a = fun (t : HolorIndex ds₂) ↦ a (cast ⋯ t)

Tactic:
subst eq
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ : List ℕ
a : Holor α ds₁
⊢ cast ⋯ a = fun (t : HolorIndex ds₁) ↦ a (cast ⋯ t)

Tactic:
rfl
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
rw : (x ⊗ y ⊗ z) t = cast ⋯ (x ⊗ (y ⊗ z)) t
⊢ (x ⊗ y ⊗ z) t = (x ⊗ (y ⊗ z)).assocLeft t

Tactic:
rw [assocLeft]

Premises used: Holor.assocLeft
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
unfold :
  x t.take.take * y t.take.drop * z t.drop =
    cast ⋯ (fun (t : HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
⊢ (x ⊗ y ⊗ z) t = cast ⋯ (x ⊗ (y ⊗ z)) t

Tactic:
unfold mul

Premises used: Holor.mul
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
rw :
  x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    (fun (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) ↦ x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t
eq : ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
⊢ x t.take.take * y t.take.drop * z t.drop =
    cast ⋯ (fun (t : HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) ↦ x t.take * (y t.drop.take * z t.drop.drop)) t

Tactic:
rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
      cast_type]

Premises used: HolorIndex.drop_take, mul_assoc, HolorIndex.take_take, HolorIndex.drop_drop, Holor.cast_type