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

Goal state before:
pp: case inr
R : Type u_4
inst✝ : CommRing R
n k : ℕ
hnk : n ∈ range k
⊢ ∏ i ∈ range k, (↑n - ↑i) = ∏ i ∈ range k, ↑(n - i)

Tactic:
rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

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

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
M : Type u_3
inst✝¹ : CompleteLattice M
inst✝ : One M
h1 : ⊥ = 1
s : ι → Set α
f : α → M
x : α
hx : x ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator f x = ⨆ i, (s i).mulIndicator f x

Tactic:
rw [mulIndicator_of_mem hx]
    rw [mem_iUnion] at hx
    refine le_antisymm ?_ (iSup_le fun i ↦ mulIndicator_le_self' (fun x _ ↦ h1 ▸ bot_le) x)
    rcases hx with ⟨i, hi⟩
    exact le_iSup_of_le i (ge_of_eq <| mulIndicator_of_mem hi _)

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

Goal state before:
pp: case pos
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a

Tactic:
obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha

Goal state after:
case pos
α : Type u_2
M : Type u_3
inst✝³ : CompleteLattice M
inst✝² : One M
ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : ⊥ = 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∈ ⋃ i, s i
i : ι
hi : a ∈ s i
⊢ (⋃ i, s i).mulIndicator (⨆ i, f i) a ≤ (⨆ i, (s i).mulIndicator (f i)) a
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = (if i ∈ s then 1 i else 0) * if j ∈ t then 1 j else 0

Tactic:
split_ifs with h₀

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 1 (i, j) = 1 i * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 1 (i, j) = 1 i * 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 1 (i, j) = 0 * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : i ∈ s ∧ j ∈ t
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 1 (i, j) = 0 * 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : j ∈ t
⊢ 0 = 1 i * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : i ∈ s
h✝ : ¬j ∈ t
⊢ 0 = 1 i * 0

case pos
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : ¬i ∈ s
h✝ : j ∈ t
⊢ 0 = 0 * 1 j

case neg
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
h₀ : ¬(i ∈ s ∧ j ∈ t)
h✝¹ : ¬i ∈ s
h✝ : ¬j ∈ t
⊢ 0 = 0 * 0
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
ι : Type u_3
inst✝ : Finite α
f : ι → α → M
hf : ∀ (a : α), (mulSupport fun x ↦ f x a).Finite
i : ι
hi : i ∈ mulSupport f
⊢ i ∈ ⋃ i, mulSupport fun x ↦ f x i

Tactic:
simp only [mem_mulSupport, Set.mem_iUnion] at hi ⊢

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : One M
ι : Type u_3
inst✝ : Finite α
f : ι → α → M
hf : ∀ (a : α), (mulSupport fun x ↦ f x a).Finite
i : ι
hi : f i ≠ 1
⊢ ∃ i_1, f i i_1 ≠ 1
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport (f ∘ g)

Tactic:
refine Set.Finite.of_injOn ?_ (Set.injOn_of_injective hg) hf
  grind [Set.mapsTo_iff_subset_preimage, Function.mulSupport]

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

Goal state before:
pp: case inr.succ
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
h✝ : Nontrivial R
n : ℕ
ih : abv ↑n ≤ ↑n
⊢ abv ↑(n + 1) ≤ ↑(n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
⊢ (if x * y = 0 then 0 else 1) = (if x = 0 then 0 else 1) * if y = 0 then 0 else 1

Tactic:
by
    rcases eq_or_ne x 0 with rfl | hx
    · simp
    rcases eq_or_ne y 0 with rfl | hy
    · simp
    simp [hx, hy]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : Preorder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
⊢ ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
  classical
  calc
    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
    _ ≤ ∏ i ∈ s, f i :=
      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))

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

Goal state before:
pp: case mk
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
fst✝ : α
snd✝ : M
⊢ (fst✝, snd✝) ∈ f.graph ↔ f (fst✝, snd✝).1 = (fst✝, snd✝).2 ∧ (fst✝, snd✝).2 ≠ 0

Tactic:
exact mk_mem_graph_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
a : α
h : ¬(mapDomain (⇑f) x) (f a) = 0
⊢ ¬x a = 0 ∧ f a = f a

Tactic:
by simpa [f.injective] using h

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

Goal state before:
pp: case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : IsOrderedMonoid N
f : M → N
p : M → Prop
h_one : f 1 ≤ 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ i ∈ s, p (g i)
hs_nonempty : s.Nonempty
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
· exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
⊢ filter p f = f ↔ ∀ (x : α), f x ≠ 0 → p x

Tactic:
by
  simp only [DFunLike.ext_iff, filter_eq_indicator, Set.indicator_apply_eq_self, Set.mem_ofPred_eq,
    not_imp_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), #({b ∈ B | a ∈ b}) = n
⊢ ∑ s ∈ B, #s = Fintype.card α * n

Tactic:
simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]

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
h : ∀ i ∈ s, f i ≤ g i
⊢ ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i

Tactic:
by
  classical
    revert h
    refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h),
      fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
    specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem
    rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
    exact
      mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a))
        (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
← mul_le_mul_iff_right,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ (∏ i ∈ s \ t, f i) * ?a ≤ (∏ i ∈ t \ s, f i) * ?a ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

case a
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ M
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = span R {x | x ∈ s}

Tactic:
Set.ofPred_mem_eq

Goal state after:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = span R s
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m ⁻¹' uIoc (natAdd m i) (natAdd m j) = uIoc i j

Tactic:
by
  simp [uIoc, ← (strictMono_natAdd m).monotone.map_max, ← (strictMono_natAdd m).monotone.map_min]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' uIoc i j = uIoc (natAdd m i) (natAdd m j)

Tactic:
by
  simp [uIoc, ← (strictMono_natAdd m).monotone.map_max, ← (strictMono_natAdd m).monotone.map_min]

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ ((b'.constr R) (g ∘ ⇑b')) (f (b i)) = LinearMap.id (b i)

Tactic:
← hi',

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι
i' : ι'
hi' : b' i' = f (b i)
⊢ ((b'.constr R) (g ∘ ⇑b')) (b' i') = LinearMap.id (b i)
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ ((b.constr R) (f ∘ ⇑b)) (g (b' i)) = LinearMap.id (b' i)

Tactic:
← hi',

Goal state after:
ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ ((b.constr R) (f ∘ ⇑b)) (b i') = LinearMap.id (b' i)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = ↑(Finset.image g hs.toFinset) ∩ mulSupport f

Tactic:
Finset.coe_image,

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = g '' ↑hs.toFinset ∩ mulSupport f
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j

Tactic:
by
  rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]
  exact finprod_mem_congr rfl he₁

Goal state after:
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
inst✝ : Nontrivial R
i : ι
s : Set ι
⊢ b i ∈ span R (⇑b '' s) ↔ i ∈ s

Tactic:
simp [mem_span_image, Finsupp.support_single]

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + (m • p + a) = (n + l) • p + c

Tactic:
hab,

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
m n : ℕ
hab : m • p + a = n • p + b
k l : ℕ
hbc : k • p + b = l • p + c
⊢ k • p + (n • p + b) = (n + l) • p + c
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ k • p + a + (m • p + c) = (l + n) • p + (b + d)

Tactic:
hab,

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
k l : ℕ
hab : k • p + a = l • p + b
m n : ℕ
hcd : m • p + c = n • p + d
⊢ l • p + b + (m • p + c) = (l + n) • p + (b + d)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a : Fin n
⊢ ∏ i ≤ a.castSucc, f i = ∏ i ≤ a, f i.castSucc

Tactic:
simp [← map_castSuccEmb_Iic]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n k : ℕ
⊢ (m + n * k).gcd n = 1 ↔ m.gcd n = 1

Tactic:
gcd_add_mul_left_left

Goal state after:
m n k : ℕ
⊢ m.gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
p : Finsupp.equivMapDomain (Equiv.ofInjective v ⋯).symm (Span.repr R (range v) x) = hv.repr x
i : ι
⊢ (Span.repr R (range v) x) ⟨v i, ⋯⟩ = (Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)) ⟨v i, ⋯⟩

Tactic:
simp [← p]

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [MOD m]

Tactic:
by convert! h.mul_left' c <;> rwa [Nat.mul_div_cancel']

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
⊢ ∃ a, f a = i

Tactic:
have l_eq : l = _ := hv h_total_eq

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : l = Finsupp.single i 1
⊢ ∃ a, f a = i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
ih : ∀ (f : Fin n → Fin m), ∑ i, ↑(f i) * m ^ ↑i < m ^ n
f : Fin (n + 1) → Fin m
⊢ ∑ i, ↑(f i) * m ^ ↑i < m ^ (n + 1)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
rw [add_comm, add_modulus_mul_modEq_iff]

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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
ih : ∀ (a : Fin (m ^ n)), ⟨∑ i, ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = a
a : Fin (m ^ (n + 1))
⊢ ⟨∑ i, ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = a

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (n * (a / n) + (a % n - b)) % n

Tactic:
mul_add_mod

Goal state after:
case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a % n - b) % n
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case isFalse.isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ n - x.natAbs % n = (x % ↑n).toNat

Tactic:
· rw [Int.emod_natAbs_of_neg (by lia) (NeZero.ne n),
        if_neg (by rwa [← Int.natCast_dvd] at h)]
      have : x % n < n := Int.emod_lt_of_pos x (by have := NeZero.ne n; lia)
      lia

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
inst✝ : IsEmpty α
⊢ Nat.card α = 0

Tactic:
by simp [Nat.card]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ ↑n ≤ toENat c ↔ ↑n ≤ c

Tactic:
by
  rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ w < 1, ∃ i, w < #↑↑i

Tactic:
· intro w hw
    exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Even (insert a s).ncard ↔ Odd s.ncard

Tactic:
rw [ncard_insert_of_notMem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ s

Tactic:
by
  rw [← SetLike.mem_coe, ← ha]; exact mem_own_leftCoset s a

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard

Tactic:
encard_union_add_encard_inter

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.encard + t.encard = s.encard + t.encard
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = i.removeNth (Pi.mulSingle i x)

Tactic:
unfold removeNth; simp [succAbove_ne, Pi.one_def]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ (leftRel φ.ker) a b

Tactic:
rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℕ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
← nsmul_eq_mul,

Goal state after:
R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℕ
a : R
⊢ ↑(n • a) = n • ↑a
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a✝ : R
ha : a✝ ≠ 0
x✝¹ x✝ : R
hb : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
⊢ x✝¹ = x✝

Tactic:
obtain ⟨x, hx⟩ := h.mul_inv_cancel ha
    simpa [← mul_assoc, h.mul_comm, hx] using congr_arg (x * ·) hb

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b

Tactic:
rw [mem_Iic, mem_Iio, le_pred_iff_of_not_isMin hb]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ f.ker ≤ span R (⇑f ⁻¹' s)

Tactic:
ker_le_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
y : M₂ := Classical.choose h₀
hy : y ∈ s
⊢ ∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑(span R (⇑f ⁻¹' s))