mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
⊢ ∀ (a b : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }),
    ∑ i ∈ (↑a).toFinset, (φ i) (f i) = ∑ i ∈ (↑b).toFinset, (φ i) (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (f + g) = comapDomain' h hh' f + comapDomain' h hh' g

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
k : κ
x : β (h k)
⊢ comapDomain' h hh' (single (h k) x) = single k x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
i : ι
⊢ 0 ≍ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
⊢ (fun c ↦ Trunc.lift (fun s ↦ ∑ i ∈ (↑s).toFinset, (φ i) (0 i)) c (support' 0)) ⋯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
⊢ (fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) (comapDomain' ⇑h.symm ⋯ f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
i : ι
x : β i
⊢ (sumZeroHom φ) (single i x) = (φ i) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
⊢ comapDomain' ⇑h.symm ⋯ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
hi : i ∉ sf.toFinset
⊢ i ∉ sf

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
⊢ sumZeroHom (Pi.single i φ) = φ.comp { toFun := fun x ↦ x i, map_zero' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ extendWith 0 (single i x) = single (some i) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin n.succ → α), P x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ prod a = ∏ i, a i

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
⊢ extendWith x 0 = single none x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
⊢ (fun f ↦ extendWith f.1 f.2) ((fun f ↦ (f none, comapDomain some ⋯ f)) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
⊢ (sumZeroHom φ) f = f.sum fun x ↦ ⇑(φ x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
⊢ (fun f ↦ (f none, comapDomain some ⋯ f)) ((fun f ↦ extendWith f.1 f.2) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (g₁ + g₂) = mapRange f hf g₁ + mapRange f hf g₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
f₂ : (i : ι) → β i →+ β₁ i
⊢ (addMonoidHom fun i ↦ (f i).comp (f₂ i)) = (addMonoidHom f).comp (addMonoidHom f₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i x ↦ (e i).symm x) ⋯ (mapRange (fun i x ↦ (e i) x) ⋯ x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
⊢ ∀ (x y : Π₀ (i : ι), β i),
    (sumZeroHom fun i ↦ ↑(φ i)).toFun (x + y) =
      (sumZeroHom fun i ↦ ↑(φ i)).toFun x + (sumZeroHom fun i ↦ ↑(φ i)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : β i →+ γ
⊢ ↑(sumAddHom (Pi.single i φ)) = ↑(φ.comp (evalAddMonoidHom i))

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
e : (i : ι) → β₁ i ≃+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ mapRange (fun i x ↦ (e i) x) ⋯ (mapRange (fun i x ↦ (e i).symm x) ⋯ x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
f₁ : Π₀ (i : ι₁), β₁ i
f₂ : Π₀ (i : ι₂), β₂ i
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
⊢ (sumAddHom fun i₂ ↦ (sumAddHom fun i₁ ↦ h i₁ i₂) f₁) f₂ =
    (sumAddHom fun i₁ ↦ (sumAddHom fun i₂ ↦ (h i₁ i₂).flip) f₂) f₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
x : (i : ι) → β i →+ γ
⊢ (fun F i ↦ F.comp (singleAddHom β i)) (sumAddHom x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → AddZeroClass (β₁ i)
inst✝ : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β i ≃+ β₁ i
f₂ : (i : ι) → β₁ i ≃+ β₂ i
⊢ (addEquiv fun i ↦ (f i).trans (f₂ i)) = (addEquiv f).trans (addEquiv f₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
ψ : (Π₀ (i : ι), β i) →+ γ
⊢ sumAddHom ((fun F i ↦ F.comp (singleAddHom β i)) ψ) = ψ

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
F G : (i : ι) → β i →+ γ
⊢ sumAddHom (F + G) = sumAddHom F + sumAddHom G

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
f : (i : ι) → β i →+ γ
i : ι
x : β i
⊢ (liftAddHom f) (single i x) = (f i) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
f : (i : ι) → β i →+ γ
i : ι
⊢ (liftAddHom f).comp (singleAddHom β i) = f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
δ : Type u_1
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : AddCommMonoid γ
inst✝ : AddCommMonoid δ
g : γ →+ δ
f : (i : ι) → β i →+ γ
a : ι
⊢ liftAddHom.symm (g.comp (liftAddHom f)) a = g.comp (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddGroup (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommGroup γ
f g : Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_sub : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ - b₂) = h i b₁ - h i b₂
⊢ (f - g).sum h = f.sum h - g.sum h

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ ∅, (g i).prod h = (∑ i ∈ ∅, g i).prod h

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h → ∏ i ∈ insert a s, (g i).prod h = (∑ i ∈ insert a s, g i).prod h

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
γ : Type w
α : Type x
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
s : Finset α
g : α → Π₀ (i : ι), β i
h : (i : ι) → β i → γ
h_zero : ∀ (i : ι), h i 0 = 1
h_add : ∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ * h i b₂
⊢ ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f.sum single = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ((subtypeDomain p v).prod fun i b ↦ h (↑i) b) = v.prod h

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
⊢ id.dualMap = id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ⇑f
⊢ Function.Injective ⇑f.dualMap

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
⊢ (refl R M₁).dualMap = refl R (Dual R M₁)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ f.dualMap.dualMap ∘ₗ eval R M₁ = eval R M₂ ∘ₗ f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ f 1 * r = f r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : Dual R M₁
⊢ (dualMap f).range = R ∙ f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
⊢ f ((evalEquiv R M).symm g) = g f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
⊢ ↑(evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ eval R M' ∘ₗ f ∘ₗ ↑(evalEquiv R M).symm = f.dualMap.dualMap

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
⊢ f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
⊢ Bijective ⇑(eval R (Dual R M))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
⊢ Dual.eval R N = ↑ed.symm ∘ₗ Dual.eval R M ∘ₗ ↑e.symm

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
⊢ Bijective ⇑(Dual.eval R N)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ (Dual.eval R M) m₁ = (Dual.eval R M) m₂

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, φ w = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Submodule R (Dual R M)
x : M
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, φ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
W : Submodule R M
f : N →ₗ[R] M
⊢ map f.dualMap W.dualAnnihilator ≤ (comap f W).dualAnnihilator

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ GaloisConnection (⇑OrderDual.toDual ∘ dualAnnihilator) (dualCoannihilator ∘ ⇑OrderDual.ofDual)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤.dualAnnihilator = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
U : ι → Submodule R M
⊢ ⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(span R s).dualAnnihilator = {f | s ⊆ ↑f.ker}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
x : M
φ : M →ₗ[R] R
⊢ x ∈ φ.ker ↔ φ ∈ LinearMap.ker ((Dual.eval R M) x)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Dual R M)
⊢ ↑(span R s).dualCoannihilator = {x | ∀ f ∈ s, f x = 0}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ f.dualMap.ker = f.range.dualAnnihilator

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ f.dualMap.range ≤ f.ker.dualAnnihilator

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ f.dualMap.ker = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
B : M →ₗ[R] M' →ₗ[R] R
⊢ B.range.dualCoannihilator = B.flip.ker

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i : ι
⊢ lapply i ∘ₗ lsingle i = LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
i i' : ι
h : i ≠ i'
⊢ lapply i ∘ₗ lsingle i' = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ x✝ : Π₀ (i : ι), M i
⊢ (equivCongrLeft e).toFun (x✝¹ + x✝) = (equivCongrLeft e).toFun x✝¹ + (equivCongrLeft e).toFun x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
e : ι ≃ ι'
x✝¹ : R
x✝ : Π₀ (i : ι), M i
⊢ (equivCongrLeft e).toFun (x✝¹ • x✝) = (RingHom.id R) x✝¹ • (equivCongrLeft e).toFun x✝

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M✝ : ι → Type u_5
N : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M✝ i)
inst✝⁵ : (i : ι) → Module R (M✝ i)
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : DecidableEq ι
α : ι → Type u_7
M : (i : ι) → α i → Type u_8
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (M i j)
inst✝ : (i : ι) → (j : α i) → Module R (M i j)
x✝¹ x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
⊢ __spread✝⁻⁰.toFun (x✝¹ + x✝) = __spread✝⁻⁰.toFun x✝¹ + __spread✝⁻⁰.toFun x✝

Tactic:
by

Goal state after: