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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
h1 : (mk s x) ↑i = (mk s y) ↑i
⊢ x i = y i

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
⊢ (single i b) i = b

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
h : i' ≠ i
⊢ (single i b) i' = 0

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : (if p i then single i x else 0) j = if p i then (single i x) j else 0
⊢ (filter p (single i x)) j = (if p i then single i x else 0) j

Tactic:
grind

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

Goal state before:
pp: case refl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = single i xi

Tactic:
rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : (i : ι) → Zero (β i)
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
i : ι
b₁ : β₁ i
b₂ : β₂ i
⊢ zipWith f hf (single i b₁) (single i b₂) = single i (f i b₁ b₂)

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x ↦ x ≠ i) f = erase i f

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x ↦ i ≠ x) f = erase i f

Tactic:
grind

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

Goal state before:
pp: case pos
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (c • x) ⟨i, h✝⟩ = c • x ⟨i, h✝⟩

Tactic:
rfl

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

Goal state before:
pp: case pos.refl
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
i : ι
c : γ
x : β i
⊢ ⋯ ▸ (c • x) = c • ⋯ ▸ x

Tactic:
rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : ¬i = i'
⊢ (erase i f + single i (f i)) i' = f i'

Tactic:
simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), add_zero]

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
⊢ ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0

Tactic:
grind

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

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ ((f + g).sigmaCurry i) j = ((f.sigmaCurry + g.sigmaCurry) i) j

Tactic:
rfl

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

Goal state before:
pp: ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ ((r • f).sigmaCurry i) j = ((r • f.sigmaCurry) i) j

Tactic:
rfl

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

Goal state before:
pp: case h.cons.inr
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : ¬f i = 0
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
grind

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (x + y) ⟨i, h✝⟩ = x ⟨i, h✝⟩ + y ⟨i, h✝⟩

Tactic:
rfl

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
h✝ : i ∈ s
⊢ 0 ⟨i, h✝⟩ = 0 i

Tactic:
rfl

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
h✝ : i ∉ s
⊢ 0 = 0 i

Tactic:
rfl

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (-x) ⟨i, h✝⟩ = -x ⟨i, h✝⟩

Tactic:
rfl

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
h✝ : i ∈ s
⊢ (x - y) ⟨i, h✝⟩ = x ⟨i, h✝⟩ - y ⟨i, h✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ({
            toFun := fun a ↦
              Quotient.hrecOn (motive := fun x ↦
                (∀ (i : ι), i ∈ x) → Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l)) (↑a)
                (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
            invFun := fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ ⟦fun x1 x2 ↦ a x1⟧) ⋯ =
    ⟦a⟧

Tactic:
rfl

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

Goal state before:
pp: case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ ↑s ∧ f i ≠ 0 ↔ f i ≠ 0

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
f : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x ↦ ⟦a x⟧

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
a : (i : ι) → α i
f : ((i : ι) → α i) → β
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a = f b
⊢ ⟦a⟧.liftOn f h = f a

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
a : (i : ι) → α i
⊢ ⟦a⟧.eval = fun x ↦ ⟦a x⟧

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
⊢ (finChoice q).eval = q

Tactic:
by
    refine induction_on_fintype_pi q (fun a ↦ ?_)
    rw [finChoice_eq]
    rfl

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
f : (a : (i : ι) → α i) → C fun x ↦ ⟦a x⟧
h : ∀ (a b : (i : ι) → α i), (∀ (i : ι), a i ≈ b i) → f a ≍ f b
⊢ Quotient.hrecOn ⟦a⟧ f h ≍ f a

Tactic:
rfl

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
s : { s // ∀ (i : ι), i ∈ s ∨ toFun 0 i = 0 }
i✝ : ι
a✝ : i✝ ∈ ↑s
⊢ 0 i✝ = 0

Tactic:
rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
⊢ (single i b).support = {i}

Tactic:
grind

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

Goal state before:
pp: case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
i : ι
b : β i
h✝ : (i : ι) → β i → γ
h_zero : h✝ i 0 = 1
h : b = 0
⊢ prod 0 h✝ = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (f + g)) i✝) a✝ = ((sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g) i✝) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (r • f)) i✝) a✝ = ((r • sigmaFinsuppEquivDFinsupp f) i✝) a✝

Tactic:
rfl

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

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
⊢ zipWith f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) fun i ↦ f (↑i) (g₁ ↑i) (g₂ ↑i)

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁶ : DecidableEq ι
inst✝⁵ : (i : ι) → Zero (β i)
inst✝⁴ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
g₁ : Π₀ (i : ι), β₁ i
g₂ : Π₀ (i : ι), β₂ i
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
⊢ erase i f = mk (f.support.erase i) fun j ↦ f ↑j

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ filter p f = mk (Finset.filter p f.support) fun i ↦ f ↑i

Tactic:
grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ (filter p f).support = {x ∈ f.support | p x}

Tactic:
grind

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

Goal state before:
pp: case refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
i : ι
a✝ : i ∈ sx.toFinset ∩ sy.toFinset
⊢ (φ i) (f i) = (φ i) (f i)

Tactic:
rfl

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

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

Tactic:
by
  ext
  rw [zero_apply, comapDomain'_apply, zero_apply]

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:
grind

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) γ
⊢ Trunc.lift (fun s ↦ 0) ⋯ (support' 0) = 0

Tactic:
rfl

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
i : ι
⊢ f (h.symm (h i)) ≍ f i

Tactic:
h.symm_apply_apply

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ f i ≍ f i
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i ↦ Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)

Tactic:
rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i✝ : Fin (n + 1)
i : Fin n
⊢ Matrix.vecTail f i (Matrix.vecTail v i) = f i.succ (v i.succ)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P finZeroElim

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0 ↔ P finZeroElim

Tactic:
rfl

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

Goal state before:
pp: case pos
ι : 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
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
s : Multiset ι
hf : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
a✝ : i ∈ s.toFinset
h : { toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i ≠ 0
⊢ (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i) =
    (φ i) ({ toFun := f, support' := Quot.mk ⇑trueSetoid ⟨s, hf⟩ } i)

Tactic:
rfl

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₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ (id.dualMap x✝¹) x✝ = (id x✝¹) x✝

Tactic:
rfl

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₁
x✝¹ : Dual R M₁
x✝ : M₁
⊢ ((refl R M₁).dualMap x✝¹) x✝ = ((refl R (Dual R M₁)) x✝¹) x✝

Tactic:
rfl

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:
rfl

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:
conv_rhs => rw [← mul_one r, ← smul_eq_mul]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : Dual R R
r : R
⊢ f 1 * r = f (r • 1)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: case toDual
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Dual R M)
⊢ (∀ ⦃x : Dual R M⦄, x ∈ a✝ → ∀ w ∈ a, x w = 0) ↔ ∀ ⦃x : M⦄, x ∈ a → ∀ φ ∈ a✝, φ x = 0

Tactic:
grind

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
i✝ : ι'
⊢ ((equivCongrLeft e).toFun (x✝¹ + x✝)) i✝ = ((equivCongrLeft e).toFun x✝¹ + (equivCongrLeft e).toFun x✝) i✝

Tactic:
rfl

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
i✝ : ι'
⊢ ((equivCongrLeft e).toFun (x✝¹ • x✝)) i✝ = ((RingHom.id R) x✝¹ • (equivCongrLeft e).toFun x✝) i✝

Tactic:
rfl

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
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ + x✝)) i✝¹) i✝ = ((__spread✝⁻⁰.toFun x✝¹ + __spread✝⁻⁰.toFun x✝) i✝¹) i✝

Tactic:
rfl

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✝¹ : R
x✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd
i✝¹ : ι
i✝ : α i✝¹
⊢ ((__spread✝⁻⁰.toFun (x✝¹ • x✝)) i✝¹) i✝ = (((RingHom.id R) x✝¹ • __spread✝⁻⁰.toFun x✝) i✝¹) i✝

Tactic:
rfl

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 ι
inst✝ : Fintype ι
x✝² x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² + x✝¹) x✝ = (equivFunOnFintype.toFun x✝² + equivFunOnFintype.toFun x✝¹) x✝

Tactic:
rfl

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 ι
inst✝ : Fintype ι
x✝² : R
x✝¹ : Π₀ (i : ι), M i
x✝ : ι
⊢ equivFunOnFintype.toFun (x✝² • x✝¹) x✝ = ((RingHom.id R) x✝² • equivFunOnFintype.toFun x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (FinVec.Forall fun x_1 ↦
      FinVec.Forall fun x_2 ↦ x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
    ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).1

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑s
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inl val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inl val✝)).2

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inr.fst
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).1 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).1

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inr.snd
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) := ⋯
val✝ : ↑t
⊢ (((fun x ↦ ↑x) ∘ ⇑e) (Sum.inr val✝)).2 =
    (Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x) (Sum.inr val✝)).2

Tactic:
rfl

Goal state after: