awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.WithTopBot
Goal:
α : Type u_1
inst : Finite α
⊢ Finite.{u_1 + 1} (WithTop α)

Tactic:
have := Fintype.ofFinite α
  Finite.of_fintype _

Premises used: Fintype.ofFinite, Finite.of_fintype, WithTop
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
⊢ Eq (α := F → (a : α) → β a) (coe (β := β)) fun (f : F) ↦ (⇑f : (a : α) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
⊢ Function.Injective (β := (a : α) → β a) fun (f : F) ↦ (⇑f : (a : α) → β a)

Tactic:
DFunLike.coe_injective'

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f = g
refl : (⇑f : (a : α) → β a) = (⇑f : (a : α) → β a)
⊢ (⇑f : (a : α) → β a) = (⇑g : (a : α) → β a)

Tactic:
cases h
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f : F
⊢ (⇑f : (a : α) → β a) = (⇑f : (a : α) → β a)

Tactic:
rfl
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : (⇑f : (a : α) → β a) = (⇑g : (a : α) → β a)
⊢ f = g

Tactic:
DFunLike.coe_injective' h

Premises used: DFunLike.coe_injective'
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
⊢ f = g ↔ (⇑f : (a : α) → β a) = (⇑g : (a : α) → β a)

Tactic:
coe_fn_eq.symm

Premises used: DFunLike.coe_fn_eq, Iff.symm
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : ∀ (x : α), (f : (a : α) → β a) x = (g : (a : α) → β a) x
⊢ f = g

Tactic:
DFunLike.coe_injective' (funext h)

Premises used: funext, DFunLike.coe_injective'
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
⊢ f = g ↔ ∀ (x : α), (f : (a : α) → β a) x = (g : (a : α) → β a) x

Tactic:
coe_fn_eq.symm.trans funext_iff

Premises used: funext_iff, DFunLike.coe_fn_eq, Iff.trans, Iff.symm
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h₁ : f = g
x : α
⊢ (f : (a : α) → β a) x = (g : (a : α) → β a) x

Tactic:
congr_fun (congr_arg _ h₁) x

Premises used: congr_arg, congr_fun
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
⊢ f ≠ g ↔ ∃ (a : α), (f : (a : α) → β a) a ≠ (g : (a : α) → β a) a

Tactic:
ext_iff.not.trans not_forall

Premises used: Iff.not, DFunLike.ext_iff, Iff.trans, Classical.not_forall
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f ≠ g
⊢ ∃ (x : α), (f : (a : α) → β a) x ≠ (g : (a : α) → β a) x

Tactic:
ne_iff.mp h

Premises used: DFunLike.ne_iff, Iff.mp
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
inst : ∀ (a : α), Subsingleton.{u_3} (β a)
⊢ Subsingleton F

Tactic:
coe_injective.subsingleton

Premises used: Function.Injective.subsingleton, DFunLike.coe_injective
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
inst : IsEmpty α
⊢ Subsingleton F

Tactic:
coe_injective.subsingleton

Premises used: Function.Injective.subsingleton, DFunLike.coe_injective
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
f g : F
x y : α
h₁ : f = g
h₂ : x = y
⊢ Eq.{u_3} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) y : β)

Tactic:
congr (congr_arg _ h₁) h₂

Premises used: congr_arg, congr
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
f : F
x y : α
h₂ : x = y
⊢ Eq.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
congr_arg _ h₂

Premises used: congr_arg
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst : Decidable P
f : P → F
g : ¬P → F
x : α
pos : ∀ (h : P), Eq.{u_3} (α := β) ((f h : (a : α) → β) x : β) ((f h : (a : α) → β) x : β)
neg : ∀ (h : ¬P), Eq.{u_3} (α := β) ((g h : (a : α) → β) x : β) ((g h : (a : α) → β) x : β)
⊢ Eq.{u_3} (α := β) ((if h : P then f h else g h : (a : α) → β) x : β)
    (if h : P then (f h : (a : α) → β) x else (g h : (a : α) → β) x : β)

Tactic:
split_ifs
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst : Decidable P
f : P → F
g : ¬P → F
x : α
h : P
⊢ Eq.{u_3} (α := β) ((f h : (a : α) → β) x : β) ((f h : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst : Decidable P
f : P → F
g : ¬P → F
x : α
h : ¬P
⊢ Eq.{u_3} (α := β) ((g h : (a : α) → β) x : β) ((g h : (a : α) → β) x : β)

Tactic:
rfl
-- Module: Mathlib.Data.FunLike.Basic
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst : Decidable P
f g : F
x : α
⊢ Eq.{u_3} (α := β) ((if P then f else g : (a : α) → β) x : β)
    (if P then (f : (a : α) → β) x else (g : (a : α) → β) x : β)

Tactic:
dite_apply _ _ _

Premises used: DFunLike.dite_apply, ite
-- Module: Mathlib.Data.FunLike.Embedding
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
inst : FunLike F α β
i : EmbeddingLike F α β
f : F
⊢ Function.Injective.{u_2, u_3} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
injective' f

Premises used: EmbeddingLike.injective'
-- Module: Mathlib.Data.FunLike.Embedding
Goal:
F : Sort u_1
α : Sort u_2
β : Sort u_3
inst : FunLike F α β
i : EmbeddingLike F α β
f : F
x y : α
⊢ Eq.{u_3} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x = y

Tactic:
(EmbeddingLike.injective f).eq_iff

Premises used: Function.Injective.eq_iff, EmbeddingLike.injective
-- Module: Mathlib.Data.FunLike.Embedding
Goal:
α : Sort u_2
β : Sort u_3
γ : Sort u_4
F : Sort u_5
inst : FunLike F β γ
inst_1 : EmbeddingLike F β γ
f : α → β
e : F
⊢ Function.Injective.{u_2, u_4} (β := γ) ((⇑e : (a : β) → γ) ∘ f) ↔ Function.Injective f

Tactic:
(EmbeddingLike.injective e).of_comp_iff f

Premises used: EmbeddingLike.injective, Function.Injective.of_comp_iff
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
⊢ Function.Injective (α := E) inv

Tactic:
fun e g h ↦
  coe_injective' e g ((right_inv e).eq_rightInverse (h.symm ▸ left_inv g)) h

Premises used: EquivLike.right_inv, Eq.rec, Function.LeftInverse.eq_rightInverse, EquivLike.coe_injective', Function.Injective, Eq.symm, EquivLike.left_inv
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
a : α
⊢ coe e a = (e : (a : α) → β) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
b : β
a : α
mp : inv e b = a → b = (e : (a : α) → β) a
mpr : b = (e : (a : α) → β) a → inv e b = a
⊢ inv e b = a ↔ b = (e : (a : α) → β) a

Tactic:
constructor
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
b : β
⊢ b = (e : (a : α) → β) (inv e b)

Tactic:
(right_inv e b).symm

Premises used: EquivLike.right_inv, Eq.symm
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
a : α
⊢ inv.{u_1, u_3, u_4} (β := β) e ((e : (a : α) → β) a : β) = a

Tactic:
left_inv e a

Premises used: EquivLike.left_inv
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
b : β
⊢ b = (e : (a : α) → β) (inv e b)

Tactic:
exacts [(right_inv e b).symm, left_inv e a]

Premises used: EquivLike.right_inv, Eq.symm
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
⊢ Function.Injective.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
EmbeddingLike.injective e

Premises used: EmbeddingLike.injective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
⊢ Function.Surjective.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
(right_inv e).surjective

Premises used: EquivLike.right_inv, Function.RightInverse.surjective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
⊢ Function.Bijective.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
⟨EquivLike.injective e, EquivLike.surjective e⟩

Premises used: And.intro, Function.Bijective, EquivLike.surjective, EquivLike.injective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
f : E
x y : α
⊢ Eq.{u_4} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) ↔ x = y

Tactic:
EmbeddingLike.apply_eq_iff_eq f

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
γ : Sort u_5
inst : EquivLike E α β
e : E
f : β → γ
⊢ Function.Injective.{u_3, u_5} (α := α) (f ∘ (⇑e : (a : α) → β)) ↔ Function.Injective f

Tactic:
Function.Injective.of_comp_iff' f (EquivLike.bijective e)

Premises used: Function.Injective.of_comp_iff', EquivLike.bijective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
γ : Sort u_5
inst : EquivLike E α β
e : E
f : β → γ
⊢ Function.Surjective.{u_3, u_5} (α := α) (f ∘ (⇑e : (a : α) → β)) ↔ Function.Surjective f

Tactic:
(EquivLike.surjective e).of_comp_iff f

Premises used: Function.Surjective.of_comp_iff, EquivLike.surjective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
γ : Sort u_5
inst : EquivLike E α β
e : E
f : β → γ
⊢ Function.Bijective.{u_3, u_5} (α := α) (f ∘ (⇑e : (a : α) → β)) ↔ Function.Bijective f

Tactic:
(EquivLike.bijective e).of_comp_iff f

Premises used: Function.Bijective.of_comp_iff, EquivLike.bijective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
a : α
⊢ inv.{u_1, u_3, u_4} (β := β) e ((e : (a : α) → β) a : β) = a

Tactic:
left_inv _ _

Premises used: EquivLike.left_inv
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
e : E
b : β
⊢ (e : (a : α) → β) (inv e b) = b

Tactic:
right_inv _ _

Premises used: EquivLike.right_inv
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
F : Sort u_2
α : Sort u_3
β : Sort u_4
γ : Sort u_5
inst : EquivLike F β γ
f : α → β
e : F
⊢ Function.Injective.{u_3, u_5} (β := γ) ((⇑e : (a : β) → γ) ∘ f) ↔ Function.Injective f

Tactic:
EmbeddingLike.comp_injective f e

Premises used: EmbeddingLike.comp_injective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
F : Sort u_2
α : Sort u_3
β : Sort u_4
γ : Sort u_5
inst : EquivLike F β γ
f : α → β
e : F
⊢ Function.Surjective.{u_3, u_5} (β := γ) ((⇑e : (a : β) → γ) ∘ f) ↔ Function.Surjective f

Tactic:
Function.Surjective.of_comp_iff' (EquivLike.bijective e) f

Premises used: Function.Surjective.of_comp_iff', EquivLike.bijective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
F : Sort u_2
α : Sort u_3
β : Sort u_4
γ : Sort u_5
inst : EquivLike F β γ
f : α → β
e : F
⊢ Function.Bijective.{u_3, u_5} (β := γ) ((⇑e : (a : β) → γ) ∘ f) ↔ Function.Bijective f

Tactic:
(EquivLike.bijective e).of_comp_iff' f

Premises used: Function.Bijective.of_comp_iff', EquivLike.bijective
-- Module: Mathlib.Data.FunLike.Equiv
Goal:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst : EquivLike E α β
inst_1 : Subsingleton α
⊢ Subsingleton E

Tactic:
⟨fun f g ↦ DFunLike.ext f g fun _ ↦ (right_inv f).injective <| Subsingleton.elim _ _⟩

Premises used: EquivLike.right_inv, DFunLike.ext, Subsingleton.intro, EquivLike.inv, Subsingleton.elim, DFunLike.coe, Function.RightInverse.injective
-- Module: Mathlib.Data.FunLike.Fintype
Goal:
F : Sort u_1
α : Sort u_3
β : α → Sort u_5
inst : DFunLike F α β
inst_1 : Finite α
inst_2 : ∀ (i : α), Finite.{u_5} (β i)
⊢ Finite F

Tactic:
Finite.of_injective _ DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Finite.of_injective
-- Module: Mathlib.Data.FunLike.Fintype
Goal:
G : Sort u_2
α : Sort u_3
γ : Sort u_4
inst : FunLike G α γ
inst_1 : Finite α
inst_2 : Finite γ
⊢ Finite G

Tactic:
DFunLike.finite G

Premises used: DFunLike.finite
-- Module: Mathlib.Data.FunLike.Graded
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : FunLike F A B
inst_3 : GradedFunLike F 𝒜 ℬ
f : F
i : ι
x : A
h : x ∈ 𝒜 i
⊢ Membership.mem.{u_3, u_5} (α := B) (ℬ i) ((f : (a : A) → B) x : B)

Tactic:
GradedFunLike.map_mem f h

Premises used: GradedFunLike.map_mem
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : A
⊢ Membership.mem.{u_3, u_5} (α := B) (ℬ i) ((e : (a : A) → B) x : B) ↔ x ∈ 𝒜 i

Tactic:
GradedEquivLike.map_mem_iff e

Premises used: GradedEquivLike.map_mem_iff
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
rw : (↑y : B) ∈ ℬ i
⊢ Membership.mem.{u_3, u_5} (α := B) (ℬ i) ((e : (a : A) → B) (EquivLike.inv e (↑y : B)) : B)

Tactic:
rw [EquivLike.apply_inv_apply]

Premises used: EquivLike.apply_inv_apply
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ (↑y : B) ∈ ℬ i

Tactic:
y.2

Premises used: Subtype.property
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
y : ↥(ℬ i)
⊢ (↑y : B) ∈ ℬ i

Tactic:
exact y.2

Premises used: Subtype.property
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(𝒜 i)
a :
  (↑((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i)))
          (subtypeMap e i x)) :
      A) =
    (↑x : A)
⊢ (fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i)))
      (subtypeMap e i x) =
    x

Tactic:
ext
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(𝒜 i)
⊢ (↑((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i)))
          (subtypeMap e i x)) :
      A) =
    (↑x : A)

Tactic:
EquivLike.inv_apply_apply e _

Premises used: EquivLike.inv_apply_apply
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(𝒜 i)
⊢ (↑((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i)))
          (subtypeMap e i x)) :
      A) =
    (↑x : A)

Tactic:
exact EquivLike.inv_apply_apply e _

Premises used: EquivLike.inv_apply_apply
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(ℬ i)
a :
  (↑(subtypeMap e i
          ((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i))) x)) :
      B) =
    (↑x : B)
⊢ subtypeMap e i
      ((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i))) x) =
    x

Tactic:
ext
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(ℬ i)
⊢ (↑(subtypeMap e i
          ((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i))) x)) :
      B) =
    (↑x : B)

Tactic:
EquivLike.apply_inv_apply e _

Premises used: EquivLike.apply_inv_apply
-- Module: Mathlib.Data.FunLike.Graded
Goal:
E : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
τ : Type u_5
ι : Type u_6
inst : SetLike σ A
inst_1 : SetLike τ B
𝒜 : ι → σ
ℬ : ι → τ
inst_2 : EquivLike E A B
inst_3 : GradedEquivLike E 𝒜 ℬ
e : E
i : ι
x : ↥(ℬ i)
⊢ (↑(subtypeMap e i
          ((fun (y : ↥(ℬ i)) ↦ (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 i) (EquivLike.inv e (↑y : B)) ⋯ : ↥(𝒜 i))) x)) :
      B) =
    (↑x : B)

Tactic:
exact EquivLike.apply_inv_apply e _

Premises used: EquivLike.apply_inv_apply
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
⊢ Eq (α := (a : F) → α → β) (⇑(coeMulHom F α β) : (a : F) → α → β) (DFunLike.coe (β := fun (a : α) ↦ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
rw : Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))
⊢ Function.Injective (α := F) (β := α → β) (⇑(coeMulHom F α β) : (a : F) → α → β)

Tactic:
rw [coe_coeMulHom]

Premises used: FunLike.coe_coeMulHom
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
⊢ Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
⊢ Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))

Tactic:
exact DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : MulOne F
inst_2 : MulOneClass β
inst_3 : IsOneApply F α β
inst_4 : IsMulApply F α β
⊢ Eq (α := (a : F) → α → β) (⇑(coeMonoidHom F α β) : (a : F) → α → β) (DFunLike.coe (β := fun (a : α) ↦ β))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : MulOne F
inst_2 : MulOneClass β
inst_3 : IsOneApply F α β
inst_4 : IsMulApply F α β
⊢ Eq (α := F →ₙ* α → β) (↑(coeMonoidHom F α β) : F →ₙ* α → β) (coeMulHom F α β)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, FunLike.coeMulHom, rfl
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : MulOne F
inst_2 : MulOneClass β
inst_3 : IsOneApply F α β
inst_4 : IsMulApply F α β
rw : Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))
⊢ Function.Injective (α := F) (β := α → β) (⇑(coeMonoidHom F α β) : (a : F) → α → β)

Tactic:
rw [coe_coeMonoidHom]

Premises used: FunLike.coe_coeMonoidHom
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : MulOne F
inst_2 : MulOneClass β
inst_3 : IsOneApply F α β
inst_4 : IsMulApply F α β
⊢ Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : MulOne F
inst_2 : MulOneClass β
inst_3 : IsOneApply F α β
inst_4 : IsMulApply F α β
⊢ Function.Injective (α := F) (β := α → β) (DFunLike.coe (β := fun (a : α) ↦ β))

Tactic:
exact DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsLeftCancelMul β
inst_4 : IsMulApply F α β
⊢ IsLeftCancelMul F

Tactic:
DFunLike.coe_injective.isLeftCancelMul (fun (f : F) ↦ (f : α → β)) coe_mul

Premises used: FunLike.coe_mul, DFunLike.coe_injective, DFunLike.coe, Function.Injective.isLeftCancelMul
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsRightCancelMul β
inst_4 : IsMulApply F α β
⊢ IsRightCancelMul F

Tactic:
DFunLike.coe_injective.isRightCancelMul (fun (f : F) ↦ (f : α → β)) coe_mul

Premises used: FunLike.coe_mul, Function.Injective.isRightCancelMul, DFunLike.coe_injective, DFunLike.coe
-- Module: Mathlib.Data.FunLike.Group
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsCancelMul β
inst_4 : IsMulApply F α β
⊢ IsCancelMul F

Tactic:
DFunLike.coe_injective.isCancelMul (fun (f : F) ↦ (f : α → β)) coe_mul

Premises used: FunLike.coe_mul, Function.Injective.isCancelMul, DFunLike.coe_injective, DFunLike.coe
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : One F
inst_2 : One β
inst_3 : IsOneApply F α β
h : ∀ (x : α), Eq.{u_6 + 1} (α := β) ((1 : (a : α) → β) x : β) (1 x : β)
⊢ Eq (α := α → β) (⇑1 : (a : α) → β) 1

Tactic:
ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : One F
inst_2 : One β
inst_3 : IsOneApply F α β
x : α
⊢ Eq.{u_6 + 1} (α := β) ((1 : (a : α) → β) x : β) (1 x : β)

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
f g : F
h :
  ∀ (x : α),
    (f * g : (a : α) → β) x = HMul.hMul (α := (a : α) → β) (β := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) x
⊢ (⇑(f * g) : (a : α) → β) = HMul.hMul (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Mul F
inst_2 : Mul β
inst_3 : IsMulApply F α β
f g : F
x : α
⊢ (f * g : (a : α) → β) x = HMul.hMul (α := (a : α) → β) (β := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) x

Tactic:
simp
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Div F
inst_2 : Div β
inst_3 : IsDivApply F α β
f g : F
h :
  ∀ (x : α),
    (f / g : (a : α) → β) x = HDiv.hDiv (α := (a : α) → β) (β := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) x
⊢ (⇑(f / g) : (a : α) → β) = HDiv.hDiv (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)

Tactic:
ext
-- Module: Mathlib.Data.FunLike.IsApply
Goal:
F : Type u_3
α : Type u_5
β : Type u_6
inst : FunLike F α β
inst_1 : Div F
inst_2 : Div β
inst_3 : IsDivApply F α β
f g : F
x : α
⊢ (f / g : (a : α) → β) x = HDiv.hDiv (α := (a : α) → β) (β := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β) x

Tactic:
simp
-- 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
h : ∀ (x : α), Eq.{u_6 + 1} (α := β) ((f⁻¹ : (a : α) → β) x : β) ((⇑f : (a : α) → β)⁻¹ x : β)
⊢ Eq (α := (a : α) → β) (⇑f⁻¹ : (a : α) → β) (⇑f : (a : α) → β)⁻¹

Tactic:
ext