mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr
R : Type u_8
M : Type u_9
inst✝⁴ : Ring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
x : M
u : Rˣ
⊢ R ∙ x = R ∙ u • x

Tactic:
exact (span_singleton_group_smul_eq _ _ _).symm

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : ↑u ⊆ range fun x ↦ f ↑x
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ a ⊓ u.sup id = ⊥

Tactic:
rw [inf_comm, ← disjoint_iff, htu]

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
f : ι → α
s : Set ι
a : α
hs : ∀ t ⊆ s, t.Finite → Disjoint (⨆ i ∈ t, f i) a
u : Finset α
hu : ↑u ⊆ range fun x ↦ f ↑x
t : Set ι
ht : t ⊆ s
ht' : t.Finite
htu : u.sup id = ⨆ i ∈ t, f i
⊢ Disjoint (⨆ i ∈ t, f i) a
Module: Mathlib.Data.Multiset.Antidiagonal

Goal state before:
pp: α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ antidiagonal ⟦l⟧ ↔ x.1 + x.2 = ⟦l⟧

Tactic:
dsimp only [quot_mk_to_coe, antidiagonal_coe]

Goal state after:
α : Type u_1
s : Multiset α
x : Multiset α × Multiset α
l : List α
⊢ x ∈ ↑(powersetAux l).revzip ↔ x.1 + x.2 = ↑l
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsCoatomic ↑(Iic c)
⊢ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
← isAtomic_iff_isCoatomic

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
c : α
hcbot : c ∉ {⊥}
hc : IsCompactElement c
hcb : c ≤ b
hc' : IsAtomic ↑(Iic c)
⊢ ∃ a, IsAtom a ∧ a ≤ b
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
⊢ ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False

Tactic:
intro j' h hj hj' hi

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : One β
s : γ → Set α
f : α → β
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : α
j : γ
hj✝ : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
⊢ False
Module: Mathlib.Algebra.Group.Indicator

Goal state before:
pp: ι : Type u_6
inst✝¹ : DecidableEq ι
M : Type u_7
inst✝ : One M
i : ι
f : ι → M
j : ι
⊢ (if j = i then f j else 1) = if j = i then f i else 1

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ x ∈ f.support, f x = g x
h₁ : f.support = g.support
h₂ : ∀ x ∈ f.support, f x = g x
a : α
⊢ f a = g a

Tactic:
classical
      exact if h : a ∈ f.support then h₂ a h else by
        have hf : f a = 0 := notMem_support_iff.1 h
        have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
        rw [hf, hg]

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

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s : Submodule K V
⊢ s ⩿ K ∙ x ⊔ s

Tactic:
refine ⟨le_sup_right, fun q hpq hqp ↦ hqp.not_ge ?_⟩

Goal state after:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
⊢ K ∙ x ⊔ s ≤ q
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (indicator s f) i = if hi : i ∈ s then f i hi else 0

Tactic:
simp only [indicator, ne_eq, coe_mk]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
inst✝ : DecidableEq ι
⊢ (if H : i ∈ s then f i H else 0) = if hi : i ∈ s then f i hi else 0
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
j : ι
⊢ (if h : j = a then f j ⋯ else 0) = if j = a then f a ⋯ else 0

Tactic:
split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
⊢ f.prod g = ∏ x ∈ s, g x (f x)

Tactic:
refine Finset.prod_subset hs fun x hxs hx => h x hxs ▸ (congr_arg (g x) ?_)

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
s : Finset α
hs : f.support ⊆ s
g : α → M → N
h : ∀ i ∈ s, g i 0 = 1
x : α
hxs : x ∈ s
hx : x ∉ f.support
⊢ f x = 0
Module: Mathlib.Algebra.Module.Basic

Goal state before:
pp: case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ¬↑n = 0
⊢ (↑n)⁻¹ • ↑n • f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

Tactic:
← map_natCast_smul f R S,

Goal state after:
case neg
M : Type u_3
M₂ : Type u_4
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
F : Type u_5
inst✝⁵ : FunLike F M M₂
inst✝⁴ : AddMonoidHomClass F M M₂
f : F
R : Type u_6
S : Type u_7
inst✝³ : DivisionSemiring R
inst✝² : DivisionSemiring S
inst✝¹ : Module R M
inst✝ : Module S M₂
n : ℕ
x : M
hR : ¬↑n = 0
hS : ¬↑n = 0
⊢ (↑n)⁻¹ • f (↑n • (↑n)⁻¹ • x) = (↑n)⁻¹ • f x
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
inst✝⁶ : Semiring R
S : Type u_6
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : IsOrderedRing S
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
⊢ v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial

Tactic:
refine ⟨fun ⟨x, hx₀, hx₁⟩ h ↦ hx₁ <| h.symm ▸ trivial_apply hx₀, fun H ↦ ?_⟩

Goal state after:
R : Type u_5
inst✝⁶ : Semiring R
S : Type u_6
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
inst✝³ : IsOrderedRing S
inst✝² : DecidablePred fun x ↦ x = 0
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial S
v : AbsoluteValue R S
H : v ≠ AbsoluteValue.trivial
⊢ v.IsNontrivial
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : IsOrderedCancelMonoid α
inst✝ : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
hle : ∀ (i : ι), i ∈ s → f i ≤ g i
hlt : ∃ i, i ∈ s ∧ f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
obtain ⟨l⟩ := s

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : IsOrderedCancelMonoid α
inst✝ : MulLeftStrictMono α
s : Multiset ι
f g : ι → α
l : List ι
hle : ∀ (i : ι), i ∈ Quot.mk (⇑(List.isSetoid ι)) l → f i ≤ g i
hlt : ∃ i, i ∈ Quot.mk (⇑(List.isSetoid ι)) l ∧ f i < g i
⊢ (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod < (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
⊢ max (map f s).prod (map g s).prod ≤ (map (fun i ↦ max (f i) (g i)) s).prod

Tactic:
obtain ⟨l⟩ := s

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ max (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map (fun i ↦ max (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
⊢ (map (fun i ↦ min (f i) (g i)) s).prod ≤ min (map f s).prod (map g s).prod

Tactic:
obtain ⟨l⟩ := s

Goal state after:
case mk
ι : Type u_1
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map (fun i ↦ min (f i) (g i)) (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    min (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
m : Multiset α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f m.prod ≤ (map f m).sum

Tactic:
by
  induction m using Quotient.inductionOn with
  | h l => simp [l.apply_prod_le_sum_map _ h_one h_mul]

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

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
m : M
f : α →₀ M
⊢ f a = m ∧ m ≠ 0 → ∃ a_2, f a_2 ≠ 0 ∧ { toFun := fun a ↦ (a, f a), inj' := ⋯ } a_2 = (a, m)

Tactic:
· rintro ⟨rfl, ha⟩
    exact ⟨a, ha, rfl⟩

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

Goal state before:
pp: 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
hs : [] ≠ []
h0 : ∀ (i : ι), i ∈ [] → 0 < f i
h : ∀ (i : ι), i ∈ [] → f i < g i
⊢ (map f []).prod < (map g []).prod

Tactic:
contradiction

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_3
s : Multiset ι
hs : s ≠ 0
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 < f i
h : ∀ (i : ι), i ∈ s → f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
cases s using Quotient.ind
  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe, ne_eq, coe_eq_zero] at *
  apply List.prod_map_lt_prod_map hs f g h0 h

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

pp: case c0
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
⊢ 0 < (map f s).prod

pp: case b0
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
⊢ 0 ≤ g a

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:
case c0
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
⊢ 0 < (map f s).prod

case b0
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
⊢ 0 ≤ g a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
a✝ : β
⊢ single (g a✝) 0 = 0

Tactic:
exact single_zero _

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
x✝¹ : α
x✝ : x✝¹ ∈ v.support
⊢ single (g (f x✝¹)) 0 = 0

Tactic:
exact single_zero _

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
S : Set α
f : α → β
hf : Set.InjOn f S
v₁ : α →₀ M
⊢ v₁ ∈ {w | ↑w.support ⊆ S} → ∀ ⦃x₂ : α →₀ M⦄, x₂ ∈ {w | ↑w.support ⊆ S} → mapDomain f v₁ = mapDomain f x₂ → v₁ = x₂

Tactic:
hv₁

Goal state after:
α : 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}
⊢ ∀ ⦃x₂ : α →₀ M⦄, x₂ ∈ {w | ↑w.support ⊆ S} → mapDomain f v₁ = mapDomain f x₂ → v₁ = x₂
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
x : α
hx : x ∈ (filter p f).support
⊢ g x ((filter p f) x) = g x (f x)

Tactic:
rw [support_filter, Finset.mem_filter] at hx

Goal state after:
α : 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
x : α
hx : x ∈ f.support ∧ p x
⊢ g x ((filter p f) x) = g x (f x)
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✝ : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < ∏ j ∈ t, f j

Tactic:
calc
    ∏ j ∈ s, f j < ∏ j ∈ insert i s, f j := by
      rw [prod_insert hs]
      exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
    _ ≤ ∏ j ∈ t, f j := by
      apply prod_le_prod_of_subset_of_one_le'
      · simp [Finset.insert_subset_iff, h, ht]
      · intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
αs : ι → Type u_12
inst✝¹ : Zero M
l : (i : ι) × αs i →₀ M
inst✝ : Zero N
g : (i : ι) → (αs i →₀ M) → N
hg : ∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0
⊢ ∀ (a : ι), a ∈ l.splitSupport ↔ g a (l.split a) ≠ 0

Tactic:
intro i
    rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]

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

Goal state before:
pp: ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a),
    ⟨a, b⟩ ∈ l.support ↔ ⟨a, b⟩ ∈ (image Sigma.fst l.support).sigma fun i ↦ l.support.preimage (Sigma.mk i) ⋯

Tactic:
mem_sigma,

Goal state after:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a), ⟨a, b⟩ ∈ l.support ↔ a ∈ image Sigma.fst l.support ∧ b ∈ l.support.preimage (Sigma.mk a) ⋯
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
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

Tactic:
rw [← mul_lt_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
    ← prod_union, inter_comm, sdiff_union_inter]

Goal state after:
ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)
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, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
simp +contextual only [this, not_false_iff, true_imp_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 ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
⊢ l = 0

Tactic:
ext; simp_all [mem_supported']

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

Goal state before:
pp: α : Type u_1
M✝ : Type u_2
N✝ : Type u_3
P : Type u_4
R✝ : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S✝ : Type u_8
inst✝¹⁷ : Semiring R✝
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring S✝
inst✝¹³ : AddCommMonoid M✝
inst✝¹² : Module R✝ M✝
inst✝¹¹ : AddCommMonoid N✝
inst✝¹⁰ : Module R₂ N✝
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R₃ P
σ : R✝ →+* R₂
σ_inv : R₂ →+* R✝
R : Type u_9
S : Type u_10
M : Type u_11
N : Type u_12
ι : Type u_13
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module S M
inst✝³ : Module S N
inst✝² : SMulZeroClass R M
inst✝¹ : DistribSMul R N
inst✝ : CompatibleSMul M N R S
f : (ι →₀ M) →ₗ[S] N
r : R
m : ι →₀ M
⊢ f (r • m) = r • f m

Tactic:
by
    conv_rhs => rw [← sum_single m, map_finsuppSum, smul_sum]
    erw [← sum_single (r • m), sum_mapRange_index single_zero, map_finsuppSum]
    congr; ext i m; exact (f.comp <| lsingle i).map_smul_of_tower r m

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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
    intro x
    contrapose
    simpa [PLift.eq_up_iff_down_eq] using ha x.down

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ ∏ᶠ (x : α), f x = f a
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case mpr
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
⊢ x ∈ span R (Set.range v) → x ∈ (linearCombination R v).range

Tactic:
apply span_le.2
    intro x hx
    rcases hx with ⟨i, hi⟩
    rw [SetLike.mem_coe, LinearMap.mem_range]
    use single i 1
    simp [hi]

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

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
α : Type u_7
F : Type u_8
inst✝² : Fintype α
inst✝¹ : EquivLike F M N
inst✝ : MulEquivClass F M N
f : F
g : α → M
⊢ f (∏ i, g i) = ∏ i, f (g i)

Tactic:
by
  simp [← finprod_eq_prod_of_fintype, MulEquivClass.map_finprod]

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

Goal state before:
pp: case mpr
m n : ℕ
i : Fin (m + n)
⊢ i ∈ {i | m ≤ ↑i} → i ∈ range (natAdd m)

Tactic:
· refine fun (hi : m ≤ i) ↦ ⟨⟨i - m, by lia⟩, ?_⟩
    ext
    simp [hi]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' Ico i j = Ico (i.addNat m) (j.addNat m)

Tactic:
by
  rw [← preimage_addNat_Ico_addNat, image_preimage_eq_of_subset]
  exact Ico_subset_Ici_self.trans <| image_addNat_Ici m i ▸ image_subset_range _ _

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R s → ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x

Tactic:
by
    rw [← s.image_id, mem_span_image_iff_linearCombination]
    rintro ⟨l, hl, rfl⟩
    exact ⟨l, l.support, by simpa [linearCombination, Finsupp.sum] using! hl⟩

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 α
hst : s ⊆ t
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
rw [← finprod_mem_inter_mul_sdiff' _ ht, inter_eq_self_of_subset_right hst]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finite.toFinset hf \ {a}

Tactic:
Finset.mem_sdiff,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
x : α
hx : f x ≠ 1
⊢ x ≠ a ↔ x ∈ Finite.toFinset hf ∧ x ∉ {a}
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?s, ∏ y ∈ s with f y = i, g y = ∏ k ∈ s, g k

Tactic:
rw [Finset.prod_image']
    exact fun _ _ ↦ rfl

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inr.inr
y x z : ℕ∞
x_z : x ≤ z
x_2 : 1 < x
⊢ x ^ ⊤ ≤ z ^ ⊤

Tactic:
· rw [epow_top (x_2.trans_le x_z)]; exact le_top

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case refine_2
x y : ℕ∞
h : 1 = 0
y_0 : y = 0
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : 0 = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1

Tactic:
contradiction

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

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

Tactic:
← nsmul_add,

Goal state after:
case h
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n k l : ℕ
h : k • p + a = l • p + b
⊢ n • (k • p + a) = l • n • p + n • b
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case refine_1
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x ∣ n * m

pp: case refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x

Tactic:
refine h ▸ Nat.mul_dvd_mul ?_ ?_ <;> exact x.gcd_dvd_right _

Goal state after:
case refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case inr
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc✝ : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
hc : c = 0
right✝ : d = 0
⊢ i = j

Tactic:
contradiction

Goal state after:
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:
by
  unfold ModEq at *; rw [mul_mod_mul_left, mul_mod_mul_left, h]

Goal state after: