mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ Pi.cons s a x p₂ a ⋯ = Pi.cons s a y p₃ a ⋯

Tactic:
eq₂,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
x : κ a
a✝² : x ∈ t a
y : κ a
a✝¹ : y ∈ t a
h : x ≠ y
a✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₂ : (a : ι) → a ∈ s → κ a
left✝¹ : p₂ ∈ s.pi t
eq₂ : Pi.cons s a x p₂ = a✝
b✝ : (a' : ι) → a' ∈ insert a s → κ a'
p₃ : (a : ι) → a ∈ s → κ a
left✝ : p₃ ∈ s.pi t
eq₃ : Pi.cons s a y p₃ = b✝
eq : a✝ = b✝
⊢ a✝ a ⋯ = Pi.cons s a y p₃ a ⋯
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 1) = (if x✝ ∈ s then f x✝ else 1) * if x✝ ∈ s then g x✝ else 1

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

case neg
α : Type u_1
M : Type u_4
inst✝ : MulOneClass M
s : Set α
f g : α → M
x✝ : α
h✝ : ¬x✝ ∈ s
⊢ 1 = 1 * 1
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
hf : f.range = ⊤
⊢ map f S = f.range ↔ Codisjoint S f.ker

Tactic:
map_eq_range_iff

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
hf : f.range = ⊤
⊢ Codisjoint S f.ker ↔ Codisjoint S f.ker
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : Type u_1
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
s : Multiset α
hp₁ : {x | x ∈ s ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ s → (p₁ x ↔ p₂ x)
⊢ find? p₁ s hp₁ = find? p₂ s ⋯

Tactic:
induction s using Quotient.ind

Goal state after:
case a
α : Type u_1
p₁ p₂ : α → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
a✝ : List α
hp₁ : {x | x ∈ ⟦a✝⟧ ∧ p₁ x}.Subsingleton
h : ∀ (x : α), x ∈ ⟦a✝⟧ → (p₁ x ↔ p₂ x)
⊢ find? p₁ ⟦a✝⟧ hp₁ = find? p₂ ⟦a✝⟧ ⋯
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
b : β
⊢ (match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
    | some a => v a
    | none => 0) =
    if h : ∃ a, f a = b then v h.choose else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
b : β
h✝ : ∃ a, f a = b
⊢ (match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
    | some a => v a
    | none => 0) =
    v h✝.choose

case neg
α : Type u_1
β : Type u_2
M : Type u_4
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
b : β
h✝ : ¬∃ a, f a = b
⊢ (match Multiset.find? (fun a ↦ f a = b) v.support.val ⋯ with
    | some a => v a
    | none => 0) =
    0
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
i : ι
hi : i ∈ s
⊢ f a * ((g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    (g i * ∏ j ∈ insert a s with j < i, (f j + g j)) * ∏ j ∈ insert a s with i < j, f j

Tactic:
rw [filter_insert, if_neg (ha i hi).not_gt, filter_insert, if_pos (ha i hi), prod_insert,
      mul_left_comm]

Goal state after:
case e_a.e_a
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
i : ι
hi : i ∈ s
⊢ a ∉ {j ∈ s | i < j}
Module: Mathlib.Data.Finsupp.Single

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
b : M
h : a' ≠ a
⊢ (single a b) a' = 0

Tactic:
exact Pi.single_eq_of_ne h _

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
a : α
inst✝ : Subsingleton α
m : M
b : α
⊢ ((uniqueEquiv a).symm m) b = m

Tactic:
by simp [Subsingleton.elim b a]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Indicator

Goal state before:
pp: α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
⊢ (if a ∈ s then f a else 0) ≤ if a ∈ {a | 0 ≤ f a} then f a else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ f a ≤ f a

case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∈ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ f a ≤ 0

case pos
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∈ {a | 0 ≤ f a}
⊢ 0 ≤ f a

case neg
α : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : LinearOrder M
s : Set α
f : α → M
a : α
h✝¹ : a ∉ s
h✝ : a ∉ {a | 0 ≤ f a}
⊢ 0 ≤ 0
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
⊢ (if x✝ ∈ s then f x✝ * g x✝ else 0) = (if x✝ ∈ s then f x✝ else 0) * if x✝ ∈ s then g x✝ else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : x✝ ∈ s
⊢ f x✝ * g x✝ = f x✝ * g x✝

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s : Set ι
f g : ι → M₀
x✝ : ι
h✝ : ¬x✝ ∈ s
⊢ 0 = 0 * 0
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = (if i ∈ s then f i else 0) * g i

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∈ s
⊢ f i * g i = f i * g i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : ¬i ∈ s
⊢ 0 = 0 * g i
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∈ s
⊢ f i * g i = f i * g i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : ¬i ∈ s
⊢ 0 = f i * 0
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (if i ∈ s then if i ∈ t then f i * g i else 0 else 0) = (if i ∈ s then f i else 0) * if i ∈ t then g i else 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : i ∈ s
h✝ : i ∈ t
⊢ f i * g i = f i * g i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : i ∈ s
h✝ : ¬i ∈ t
⊢ 0 = f i * 0

case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : ¬i ∈ s
h✝ : i ∈ t
⊢ 0 = 0 * g i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
h✝¹ : ¬i ∈ s
h✝ : ¬i ∈ t
⊢ 0 = 0 * 0
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
⊢ (f.sum g).support ⊆ f.support.biUnion fun a ↦ (g a (f a)).support

Tactic:
by
  have : ∀ c, (f.sum fun a b => g a b c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0 := fun a₁ h =>
    let ⟨a, ha, ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨a, mem_support_iff.mp ha, ne⟩
  simpa only [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply, exists_prop]

Goal state after:
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∈ s
⊢ r a • f a = r a • f a

case neg
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : ¬a ∈ s
⊢ 0 = r a • 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = (if a ∈ s then r a else 0) • f a

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∈ s
⊢ r a • f a = r a • f a

case neg
α : Type u_1
R : Type u_2
M : Type u_3
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : ¬a ∈ s
⊢ 0 = 0 • f a
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: f : ℕ →₀ ℕ
nhf : 0 ∉ f.support
x✝ : ℕ
hf : x✝ ∈ f.support
H : x✝ = 0
⊢ False

Tactic:
by subst H; exact nhf hf

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
m : Multiset α
a : α
ha : a ∈ m
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedMul α
⊢ a ≤ m.prod

Tactic:
obtain ⟨t, rfl⟩ := exists_cons_of_mem ha
  rw [prod_cons]
  exact _root_.le_mul_right (le_refl a)

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h₂
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s✝ : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ (map f s).prod ≤ (map g s).prod

Tactic:
apply prod_map_le_prod_map₀
      · intro i hi
        apply le_of_lt
        apply h0
        simp [hi]
      · intro i hi
        apply le_of_lt
        apply h
        simp [hi]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
have hp_prod : p s.prod := prod_induction_nonempty p hp_mul hs0 hps

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case ha
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 0 ≤ f a

Tactic:
exact le_trans (zero_le_one' β) (h1 a)

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: case hbc
α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : ZeroLEOneClass β
f : α → β
h1 : ∀ (a : α), 1 ≤ f a
a : α
s' : Multiset α
ha : a ∈ a ::ₘ s'
⊢ 1 ≤ (map f s').prod

Tactic:
· simp_all [one_le_prod]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ v₁ a = v₂ a

Tactic:
← mapDomain_apply' S _ hv₁ hf _,

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ (mapDomain f v₁) (f a) = v₂ a

α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
hv₁ : v₁ ∈ {w | ↑w.support ⊆ S}
v₂ : α →₀ M
hv₂ : v₂ ∈ {w | ↑w.support ⊆ S}
eq : mapDomain f v₁ = mapDomain f v₂
a : α
h : a ∈ v₁.support ∪ v₂.support
⊢ a ∈ S
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
x : β →₀ M
⊢ x ∈ Set.range (mapDomain f) ↔ ∀ b ∉ Set.range f, x b = 0

Tactic:
by
  refine ⟨fun ⟨y, hy⟩ x hx ↦ hy ▸ Finsupp.mapDomain_of_notMem_range y x hx, fun h ↦ ?_⟩
  refine ⟨Finsupp.comapDomain f x hf.injOn, Finsupp.mapDomain_comapDomain f hf _ fun i hi ↦ ?_⟩
  by_contra hc
  simp only [Finset.mem_coe, Finsupp.mem_support_iff, ne_eq] at hi
  exact hi (h _ hc)

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ ∀ x ∈ s, f x = g x

Tactic:
← ih

Goal state after:
ι : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ ∏ i ∈ s, f i = ∏ i ∈ s, g i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
simp_rw [← disjoint_finsetSum_left, ← disjoint_finsetSum_right, disjoint_comm, ← and_assoc,
      and_self_iff]

Goal state after:
case cons
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ x ∈ i, x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (if h : HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down) then ∏ i ∈ Finite.toFinset h, f i.down else 1)

Tactic:
split_ifs

Goal state after:
case pos
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down)
⊢ p (∏ i ∈ Finite.toFinset h✝, f i.down)

case neg
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : ¬HasFiniteMulSupport ((fun i ↦ f i) ∘ PLift.down)
⊢ p 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
s : Set α
f : α → M
g : M →* N
h₀ : (s ∩ mulSupport f).Finite
⊢ HasFiniteMulSupport fun j ↦ ∏ᶠ (_ : j ∈ s), f j

Tactic:
· simpa only [finprod_eq_mulIndicator_apply, HasFiniteMulSupport, mulSupport_mulIndicator]

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

Goal state before:
pp: M' : Type u_7
inst✝⁸ : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module R M'
S : Type u_14
inst✝³ : Semiring S
inst✝² : Module S M'
inst✝¹ : SMulCommClass R S M'
inst✝ : Fintype ι
b : Basis ι R M
f : ι → M'
x : M
⊢ ((b.constr S) f) x = ∑ i, b.equivFun x i • f i

Tactic:
simp [b.constr_apply, b.equivFun_apply, Finsupp.sum_fintype]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case refine_2
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Set α
x✝ : ∃ t, ↑t ⊆ s ∧ ∃ c, ∑ i, c i • v ↑i = x
t : Finset α
ht : ↑t ⊆ s
c : ↥t → R
hx : ∑ i, c i • v ↑i = x
⊢ x ∈ span R (v '' s)

Tactic:
· rw [← hx]
    exact sum_smul_mem (span R (v '' s)) c fun a _ ↦ subset_span <| by aesop

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i

Tactic:
←
    finprod_mem_inter_mulSupport f (s ∩ t)

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t ∩ mulSupport f), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∩ (t ∩ mulSupport f)), f i
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}) = (if p 0 then 1 else 0) + #{x | p x.succ}

Tactic:
split_ifs

Goal state after:
case pos
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : p 0
⊢ #{x | p x.succ} + 1 = 1 + #{x | p x.succ}

case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h✝ : ¬p 0
⊢ #{x | p x.succ} = 0 + #{x | p x.succ}
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
⊢ ↑j < #{i | p i} ↔ p j

Tactic:
refine ⟨by grind, fun h ↦ ?_⟩

Goal state after:
n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
⊢ ↑j < #{i | p i}
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg.succ
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : ℕ
hi : i + 1 < o + 1
h✝ : ¬↑⟨i + 1, hi⟩ < m + 1
h : m ≤ i
⊢ v ⟨↑⟨i + 1, hi⟩ - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨i + 1, hi⟩

Tactic:
simp [not_lt.2 h]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ¬↑i < m + 1
⊢ v ⟨↑i - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) i

Tactic:
rcases i with ⟨⟨⟩ | i, hi⟩
    · simp at h
    · rw [not_lt, Fin.val_mk, Nat.add_le_add_iff_right] at h
      simp [not_lt.2 h]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ x ∈ ↑Finset.univ, ↑(t x)), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a

Tactic:
← Finset.coe_biUnion,

Goal state after:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ↑(Finset.univ.biUnion t)), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin (n + 1)
⊢ ¬k - 1 < k ↔ ¬0 < k

Tactic:
simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (finRotate n) i = i + 1

Tactic:
match n with
  | 0 => exact i.elim0
  | 1 => exact @Subsingleton.elim (Fin 1) _ _ _
  | n + 2 =>
    obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
    · simp [finRotate_last]
    · cases i
      simp only [Fin.lt_def, Fin.val_last] at h
      simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
rw [finprod_mem_finset_product']

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (abc : α × β × γ) (_ : abc ∈ s), f abc = ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)

Tactic:
rw [finprod_mem_finset_product']

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
γ : Type u_7
s : Finset (α × β × γ)
f : α × β × γ → M
⊢ ∏ᶠ (a : α) (b : β × γ) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b) =
    ∏ᶠ (a : α) (b : β) (c : γ) (_ : (a, b, c) ∈ s), f (a, b, c)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (⇑b '' s)
⊢ ↑(b.repr m).support ⊆ s

Tactic:
rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
l : ι →₀ R
hl : l ∈ supported R R s
hm : (linearCombination R ⇑b) l ∈ span R (⇑b '' s)
⊢ ↑(b.repr ((linearCombination R ⇑b) l)).support ⊆ s