mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ t, k ≤ t.sup s

Tactic:
rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
    constructor
    · intro H ι s hs
      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
      choose f hf using this
      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
      rw [Finset.sup_le_iff]
      intro b hb
      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
    · intro H s hs
      obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])
      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
      rw [Finset.sup_le_iff]
      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ ↑(s \ {⊥}) := Infinite.natEmbedding ↑(s \ {⊥})
a : ℕ → α := fun n ↦ ⨆ i, ⨆ (_ : i ≥ n), ↑(e i)
sup_le : ∀ (n : ℕ), ↑(e n) ⊔ a (n + 1) ≤ a n
n i : ℕ
hi : i ≥ n + 1
⊢ ↑(e i) ∈ s \ {↑(e n)}

Tactic:
exact ⟨(e i).2.1, fun h ↦ n.lt_succ_self.not_ge <| hi.trans_eq <| e.2 <| Subtype.val_injective h⟩

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

Goal state before:
pp: ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
R : Type u_8
inst✝ : NonAssocSemiring R
x : ι → R
⊢ x = ∑ i, x i • fun j ↦ if i = j then 1 else 0

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
⊢ (∃ (hx : x ∈ ⨆ i, p i), motive x hx) →
    (∃ (hx : y ∈ ⨆ i, p i), motive y hx) → ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩

Goal state after:
case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_8
p : ι → Submodule R M
motive : (x : M) → x ∈ ⨆ i, p i → Prop
mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯
zero : motive 0 ⋯
add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), motive x hx → motive y hy → motive (x + y) ⋯
x✝ : M
hx : x✝ ∈ ⨆ i, p i
x y : M
w✝¹ : x ∈ ⨆ i, p i
Cx : motive x w✝¹
w✝ : y ∈ ⨆ i, p i
Cy : motive y w✝
⊢ ∃ (hx : x + y ∈ ⨆ i, p i), motive (x + y) hx
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s t : Multiset α
⊢ (s + t).antidiagonal = s.antidiagonal.bind fun p ↦ map (fun q ↦ (p.1 + q.1, p.2 + q.2)) t.antidiagonal

Tactic:
induction s using Multiset.induction_on with
  | empty => simp
  | cons a s ih =>
    simp_rw [cons_add, antidiagonal_cons, ih, add_bind, bind_map, map_bind, map_map]
    congr! <;> simp

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

Goal state before:
pp: R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P'
x : M
y : N
hx : x ∈ span R s
hy : y ∈ span R t
⊢ (B x) y ∈ P'

Tactic:
induction hx, hy using span_induction₂ with
  | mem_mem u v hu hv => exact hB u hu v hv
  | zero_left v hv => simp
  | zero_right u hu => simp
  | add_left u₁ u₂ v hu₁ hu₂ hv huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | add_right u v₁ v₂ hu hv₁ hv₂ huv₁ huv₂ => simpa using add_mem huv₁ huv₂
  | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
  | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toSpanSingleton R M 0 = 0

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
| e

Tactic:
← one_mul e,

Goal state after:
R : Type u_1
inst✝ : Semiring R
e : R
h : ∀ (x : R), x * (e * e) = x * e
| 1 * e
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_5
R : Type u_7
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
f : ι → R
n : ℕ
⊢ (∑ a, f a) ^ n = ∑ p, ∏ i, f (p i)

Tactic:
simp [sum_pow']

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f : ι →₀ M
zero : motive 0
add_single : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + single a b)
⊢ motive f

Tactic:
refine f.induction_on_max zero ?_
  convert! add_single using 7 with _ _ _ H
  have := fun c hc ↦ (H c hc).ne
  apply (addCommute_of_disjoint _).eq
  simp_all [not_imp_not]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ some 0 = 0

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddZeroClass M
f g : Option α →₀ M
⊢ (f + g).some = f.some + g.some

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
m : M
⊢ (single none m).some = 0

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
y : M
f : α →₀ M
⊢ (optionElim y f).some = f

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
M : Type u_8
inst✝ : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ (Multiset.map (single a) (Multiset.map (fun b ↦ f b) s.val)).sum = ∑ b ∈ s, single a (f b)

Tactic:
· rw [Multiset.map_map]
    rfl

Goal state after:
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✝¹ : Zero M
inst✝ : CommMonoid N
v : α →₀ M
f : α ↪ β
g : β → M → N
⊢ ∏ x ∈ v.support, g (f x) ((embDomain f v) (f x)) = ∏ a ∈ v.support, g (f a) (v a)

Tactic:
embDomain_apply_self

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image (Prod.fst ∘ fun a ↦ (a, f a)) f.support = f.support

Tactic:
Function.comp_def,

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image (fun x ↦ x) f.support = f.support
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : PartialOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
m : Multiset R
⊢ 0 < m.prod ↔ ∀ (x : R), x ∈ m → 0 < x

Tactic:
rcases m with ⟨l⟩
  rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]
  exact CanonicallyOrderedAdd.list_prod_pos

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
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = v a

Tactic:
embDomain_apply_self

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
v : α →₀ M
a : α
⊢ v a = v a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid N
f : α → β
g : M →+ N
⊢ (addMonoidHom f).comp (mapRange.addMonoidHom g) = (mapRange.addMonoidHom g).comp (addMonoidHom f)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + (single i a).sum g + g i (f i) = (erase i f + single i (f i)).sum g + g i a

Tactic:
sum_add_index' hg hgg,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : AddZeroClass α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (j : ι) (a₁ a₂ : α), g j (a₁ + a₂) = g j a₁ + g j a₂
⊢ (erase i f).sum g + (single i a).sum g + g i (f i) = (erase i f).sum g + (single i (f i)).sum g + g i a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
g : β →₀ M
hg : ↑g.support ⊆ Set.range ⇑f
⊢ embDomain f (comapDomain (⇑f) g ⋯) = g

Tactic:
by
  ext b
  by_cases hb : b ∈ Set.range f
  · obtain ⟨a, rfl⟩ := hb
    rw [embDomain_apply_self, comapDomain_apply]
  · replace hg : g b = 0 := notMem_support_iff.mp <| mt (hg ·) hb
    rw [embDomain_of_notMem_range _ _ _ hb, hg]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ ↑((single (f a) m).support.preimage f hif) ⊆ ↑{a} ∧ (single (f a) m) (f a) = m

Tactic:
coe_preimage,

Goal state after:
case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α → β
a : α
m : M
hif : Set.InjOn f (f ⁻¹' ↑(single (f a) m).support)
hm : m ≠ 0
⊢ f ⁻¹' ↑(single (f a) m).support ⊆ ↑{a} ∧ (single (f a) m) (f a) = m
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
⊢ comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂

Tactic:
by
  ext
  simp

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

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ f a * ∏ x ∈ s, f x = 1 ↔ ∀ i ∈ insert a s, f i = 1

Tactic:
mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),

Goal state after:
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : PartialOrder N
f : ι → N
s✝ : Finset ι
inst✝ : MulLeftMono N
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
H : ∀ i ∈ insert a s, 1 ≤ f i
this : ∀ i ∈ s, 1 ≤ f i
⊢ f a = 1 ∧ ∏ i ∈ s, f i = 1 ↔ ∀ i ∈ insert a s, f i = 1
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g * (filter (fun a ↦ ¬p a) f).prod g = f.prod g

Tactic:
simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not, Finsupp.prod]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)

Tactic:
refine (Multiset.apply_prod_le_sum_map _ _ h_one h_mul).trans_eq ?_

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ (Multiset.map g (Multiset.map (fun x ↦ f x) s.val)).sum = ∑ x ∈ s, g (f x)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ (Multiset.map (g ∘ fun x ↦ f x) s.val).sum = ∑ x ∈ s, g (f x)

Tactic:
Function.comp_def,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
s : Finset ι
f : ι → α
g : α → β
h_one : g 1 ≤ 0
h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b
⊢ (Multiset.map (fun x ↦ g (f x)) s.val).sum = ∑ x ∈ s, g (f x)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
G : Type u_9
inst✝² : AddCommGroup G
inst✝¹ : LinearOrder G
inst✝ : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
⊢ |∑ i ∈ s, f i| = ∑ i ∈ s, f i

Tactic:
abs_of_nonneg (Finset.sum_nonneg' hf)

Goal state after:
ι : Type u_1
G : Type u_9
inst✝² : AddCommGroup G
inst✝¹ : LinearOrder G
inst✝ : AddLeftMono G
f : ι → G
s : Finset ι
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
x : α
y : β
⊢ (single a (single b m)).uncurry (x, y) = (single (a, b) m) (x, y)

Tactic:
rcases eq_or_ne a x with rfl | hne

Goal state after:
case inl
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
y : β
⊢ (single a (single b m)).uncurry (a, y) = (single (a, b) m) (a, y)

case inr
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
a : α
b : β
m : M
x : α
y : β
hne : a ≠ x
⊢ (single a (single b m)).uncurry (x, y) = (single (a, b) m) (x, y)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s).PairwiseDisjoint f
hf : ∀ i ∈ s, (f i).Nonempty
⊢ #s ≤ #(s.biUnion f)

Tactic:
rw [card_biUnion hs, card_eq_sum_ones]
  exact sum_le_sum fun i hi ↦ (hf i hi).card_pos

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

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ ∏ x ∈ S.erase d ∪ {d'}, f x = (∏ x ∈ S.erase d, f x) * f d'

Tactic:
Finset.prod_union (Finset.disjoint_singleton_right.mpr
            (fun h ↦ hd'S (Finset.mem_of_mem_erase h))),

Goal state after:
ι : Type u_9
M : Type u_10
inst✝⁴ : DecidableEq ι
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : CanonicallyOrderedMul M
inst✝ : MulLeftStrictMono M
S S' : Finset ι
f : ι → M
d d' : ι
hd_mem : d ∈ S
hS' : S' ⊆ S.erase d ∪ {d'}
hlt : f d' < f d
hd_not : d ∉ S'
hd'S : d' ∉ S
⊢ (∏ x ∈ S.erase d, f x) * ∏ x ∈ {d'}, f x = (∏ x ∈ S.erase d, f x) * f d'
Module: Mathlib.Data.Finsupp.SMulWithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
a : R
⊢ a • 0 = 0

Tactic:
by
    ext
    apply smul_zero

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

Goal state before:
pp: case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
⊢ l.sum single ∈ span R ((fun i ↦ single i 1) '' s)

Tactic:
refine sum_mem fun i il => ?_

Goal state after:
case refine_2
α : Type u_1
R : Type u_5
inst✝ : Semiring R
s : Set α
l : α →₀ R
hl : l ∈ supported R R s
i : α
il : i ∈ l.support
⊢ single i (l i) ∈ span R ((fun i ↦ single i 1) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = linearCombination R (v' ∘ f)

Tactic:
by
  ext
  simp

Goal state after:
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
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ False

Tactic:
have : univ.filter q = univ.filter p :=
    eq_of_subset_of_card_le (by grind) (by rw [card_filter_val_lt]; grind)

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
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
this : filter q univ = filter p univ
⊢ False
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ 0 + q = q ∧ ↑(Fin.ofNat n r) = r

Tactic:
exact ⟨q.zero_add, Fin.val_cast_of_lt hrn⟩

Goal state after:
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 : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f i) = ∑ i ∈ s, Finsupp.single i (g i)
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j)) i
⊢ f i = g i

Tactic:
this f,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f i) = ∑ i ∈ s, Finsupp.single i (g i)
this : ∀ (f : ι → R), f i = (∑ j ∈ s, Finsupp.single j (f j)) i
⊢ (∑ j ∈ s, Finsupp.single j (f j)) i = g i
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
⊢ x = 1

Tactic:
have := epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)

Goal state after:
case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : (fun y ↦ x ^ y) 1 ≤ (fun y ↦ x ^ y) y
⊢ x = 1
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
⊢ b ≡ a [PMOD -p] ↔ a ≡ b [PMOD p]

Tactic:
by simp [modEq_iff_zsmul, neg_eq_iff_eq_neg]

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

Goal state before:
pp: m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m → d ∣ n → IsUnit d

Tactic:
← and_imp,

Goal state after:
m n : ℕ
⊢ m.gcd n = 1 ↔ ∀ ⦃d : ℕ⦄, d ∣ m ∧ d ∣ n → IsUnit d
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
unfold ModEq at *; rw [mul_mod_mul_left, mul_mod_mul_left, h]

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

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

Tactic:
rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ Fintype.card ((i : Fin m) → Fin (n i)) = Fintype.card (Fin (∏ i, n i))

Tactic:
simp_rw [Fintype.card_pi, Fintype.card_fin]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
a : Fin (∏ i, n i)
⊢ (fun f ↦ ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩) ((fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) a) = a

Tactic:
revert a

Goal state after:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i, n i)),
    (fun f ↦ ⟨∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩) ((fun a b ↦ ⟨(↑a / ∏ j, n (Fin.castLE ⋯ j)) % n b, ⋯⟩) a) = a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case pos
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
⊢ (a % c + b % c) % c + c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)

Tactic:
add_comm _ c,

Goal state after:
case pos
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
h2 : (a % c + b % c) / c < 2
h0 : 0 < (a % c + b % c) / c
⊢ c + (a % c + b % c) % c + c * ((a % c + b % c) / c) = a % c + b % c + c * ((a % c + b % c) / c)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0

Tactic:
specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ i ∈ t₁ᶜ, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_2 : 1 < card β
⊢ card (α → β) = card β ^ ⊤

Tactic:
· rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ toNat (lift.{v, w} (Module.rank R N)) = toNat (Module.rank R N)

Tactic:
Cardinal.toNat_lift

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ toNat (Module.rank R N) = toNat (Module.rank R N)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ LinearIndependent R (-v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, LinearIndependent.neg⟩
  simpa using h.neg

Goal state after: