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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
⊢ x ≤ x ∧ z ⊓ y ≤ x

Tactic:
and_iff_right rfl.le,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
hxy : x ≤ y
hinf : y ⊓ z ≤ x
hsup : x ⊔ z ⊓ y = y
⊢ z ⊓ y ≤ x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
⊢ ∀ x ∈ ↑p ∪ ↑p', ∃ y ∈ p, ∃ z ∈ p', y + z = x

Tactic:
rintro y (h | h)

Goal state after:
case refine_1.inl
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p
⊢ ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y

case refine_1.inr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a x : α
h : IsAtom a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a

Tactic:
by rw [le_iff_lt_or_eq, h.lt_iff]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
⊢ ∀ (a b : ↑s), a < b → ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
by
    rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd
    obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le
    exact ⟨⟨x, h.out' hc hd ⟨hcx.le, hxd⟩⟩,
      ⟨by simpa
        using! hcx.lt, fun y hy hy' ↦ hcx.2 (by simpa using! hy) (by simpa using! hy')⟩, hxd⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomistic α
b : αᵒᵈ
⊢ ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
by apply h.isLUB_atoms

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : IsAtomistic αᵒᵈ
b : α
⊢ ∃ s, IsGLB s b ∧ ∀ a ∈ s, IsCoatom a

Tactic:
by apply h.isLUB_atoms

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : DistribLattice α
s : Set α
hs : s.Finite
⊢ (_root_.latticeClosure s).Finite

Tactic:
rw [← supClosure_infClosure]; exact hs.infClosure.supClosure

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ ⨆ j, ⨆ (_ : j ≠ i), t j = ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j

Tactic:
iSup_split _ (fun j ↦ t j = ⊥),

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i ≠ ⊥
this : ∀ (j : ι), ⨆ (_ : t j = ⊥), t j = ⊥
⊢ (⨆ i_1, ⨆ (_ : t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1) ⊔ ⨆ i_1, ⨆ (_ : ¬t i_1 = ⊥), ⨆ (_ : i_1 ≠ i), t i_1 =
    ⨆ j, ⨆ (_ : j ≠ ⟨i, hi⟩), t ↑j
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
by_cases a ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

case neg
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : ¬a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b
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} ⊆ {⊥}
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
rcases Set.not_subset.1 h with ⟨c, ⟨hc, hcb⟩, hcbot⟩

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
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ ↑(-span R s)

Tactic:
coe_set_neg,

Goal state after:
case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ -↑(span R s)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(-span R (-s))

Tactic:
coe_set_neg,

Goal state after:
case a
R : Type u_8
M : Type u_9
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ -↑(span R (-s))
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: case insert
ι : 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 ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
⊢ ∑ i ∈ t a, f a i * ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯) =
    ∑ p ∈ (t a).biUnion fun b ↦ image (Pi.cons s a b) (s.pi t), ∏ x ∈ (insert a s).attach, f (↑x) (p ↑x ⋯)

Tactic:
sum_biUnion h₁

Goal state after:
case insert
ι : 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 ⋯)
h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y → Disjoint (image (Pi.cons s a x) (s.pi t)) (image (Pi.cons s a y) (s.pi t))
⊢ ∑ i ∈ t a, f a i * ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯) =
    ∑ x ∈ t a, ∑ i ∈ image (Pi.cons s a x) (s.pi t), ∏ x ∈ (insert a s).attach, f (↑x) (i ↑x ⋯)
Module: Mathlib.Data.Multiset.Find

Goal state before:
pp: α : 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)
x : α
hx : x ∈ a✝
⊢ decide (p₁ x) = decide (p₂ x)

Tactic:
by simp [h x (by simpa using hx)]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
f : α → M
hf : (Function.support f).Finite
a✝ : α
⊢ a✝ ∈ (ofSupportFinite f hf).support ↔ a✝ ∈ hf.toFinset

Tactic:
simp [ofSupportFinite_coe]

Goal state after:
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
a : β
h : a ∉ Set.range ⇑f
⊢ (embDomain f v) a = 0

Tactic:
by grind [embDomain]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
G : Type u_7
H✝ : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero O
f : M → N → O
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
a : α
H : f (g₁ a) (g₂ a) ≠ 0
⊢ a ∈ g₁.support ∪ g₂.support

Tactic:
by
      classical
      grind

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f 1 * f 1 = f 1 ↔ IsIdempotentElem f

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
⊢ f 1 • f 1 = f 1 ↔ IsIdempotentElem f
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : Module.End R R
h : f (f 1) = f 1
r : R
⊢ f (f (r * 1)) = f (r * 1)

Tactic:
← smul_eq_mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : Module.End R R
h : f (f 1) = f 1
r : R
⊢ f (f (r • 1)) = f (r • 1)
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
G : Type u_6
inst✝ : AddGroup G
f : ι →₀ G
a : ι
⊢ erase a f = f - single a (f a)

Tactic:
ext a'
  rcases eq_or_ne a' a with (rfl | h)
  · simp
  · simp [h]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Indicator

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : One R
inst✝ : AddGroup R
f : ι → R
⊢ mulSupport (1 - f) = support f

Tactic:
rw [sub_eq_add_neg, mulSupport_one_add', support_neg]

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✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = (∏ x ∈ f.support ∪ g.support, h x (f x)) * ∏ x ∈ f.support ∪ g.support, h x (g x)

Tactic:
←
    Finset.prod_mul_distrib,

Goal state after:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : DecidableEq α
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = ∏ x ∈ f.support ∪ g.support, h x (f x) * h x (g x)
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ abv b - abv a ≤ abv (a - b)

Tactic:
rw [abv.map_sub]; apply abv.le_sub

Goal state after:
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✝ : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
⊢ (mapDomain f s).prod h = s.prod fun a b ↦ h (f a) b

Tactic:
rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]

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

Goal state before:
pp: ι : 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)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
by
  rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
  · simp [h_one]
  · exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs

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 ι
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t \ s ∪ t ∩ s, f x ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
sdiff_union_inter

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 ι
⊢ ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)
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
⊢ ∏ x ∈ s, f x < ∏ x ∈ t \ s ∪ t ∩ s, f x ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

pp: ι : 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)

Tactic:
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
⊢ ∏ x ∈ s, f x < ∏ x ∈ t, f x ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i

ι : 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.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case inr.refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
⊢ (lmapDomain M R f) ((lmapDomain M R (Function.invFunOn f s)) l) = l

Tactic:
· rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a ↦ single (f a)) (f x) = 0
⊢ l x = 0 x

Tactic:
Finsupp.sum_apply,

Goal state after:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
H : ∀ a ∈ s, ∀ b ∈ s, f a = f b → a = b
l : α →₀ M
h₁ : l ∈ ↑(supported M R s)
h₂ : (l.sum fun a ↦ single (f a)) = 0
x : α
this✝ : DecidablePred fun x ↦ x ∈ s
xs : x ∈ s
this : (l.sum fun a₁ b ↦ (single (f a₁) b) (f x)) = 0
⊢ l x = 0 x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : 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✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
⊢ b.reindexFinsetRange.repr (b i) = single ⟨b i, ⋯⟩ 1

Tactic:
ext ⟨bi, hbi⟩
  rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self]
  simp [Finsupp.single_apply]

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 : Finset α
x✝ : ∃ c, ∑ i ∈ s, c i • v i = x
c : α → R
hc : ∑ i ∈ s, c i • v i = x
⊢ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
refine ⟨fun i ↦ c i, ?_⟩
    rw [← hc, ← Finset.sum_coe_sort (s := s)]

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

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ (fun p ↦ p.1 * ↑n + ↑↑p.2) ((fun a ↦ (a / ↑n, Fin.ofNat n (a.natMod ↑n))) a) = a

Tactic:
simp_rw [Fin.val_ofNat, natCast_mod, natMod,
      toNat_of_nonneg (emod_nonneg _ <| natCast_eq_zero.not.2 (NeZero.ne n)), emod_emod,
      ediv_mul_add_emod]

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.rev < (a + b).rev ↔ b.rev < a

Tactic:
Iff.comm,

Goal state after:
n : ℕ
a b : Fin n
⊢ b.rev < a ↔ a.rev < (a + b).rev
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:
classical
    rw [finprod_mem_finset_product']
    simp_rw [finprod_mem_finset_product']
    simp

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
γ : Type u_7
f : α × β × γ → M
h : HasFiniteMulSupport f
⊢ ∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)

Tactic:
by
  rw [finprod_curry f h]
  congr
  ext a
  rw [finprod_curry]
  simp [h]

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
p : Submodule R M
⊢ p = ⊤ ↔ ∀ (i : ι), b i ∈ p

Tactic:
refine ⟨fun h ↦ by simp [h], fun h ↦ ?_⟩

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
p : Submodule R M
h : ∀ (i : ι), b i ∈ p
⊢ p = ⊤
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Tactic:
intro x
    simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]

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

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

Tactic:
simp [sub_eq_add_neg, h]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
n : ℕ
f : Fin (n + 1) → M
i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (init f) i.castSucc = partialProd f i.castSucc.castSucc
⊢ partialProd (init f) i.succ = partialProd f i.succ.castSucc

Tactic:
simp_all [init, partialProd_succ]

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

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) = f x.succ

Tactic:
hx,

Goal state after:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f x.castSucc * ((f x.castSucc)⁻¹ * f x.succ) = f x.succ
Module: Mathlib.Data.Nat.GCD.Basic

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

Tactic:
by
  rw [Coprime, Coprime, gcd_mul_right_add_left]

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

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

Tactic:
add_mul_modulus_modEq_iff

Goal state after:
n a b c : ℕ
⊢ a ≡ c [MOD n] ↔ a ≡ c [MOD n]
Module: Mathlib.Data.Nat.ModEq

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

Tactic:
rw [mul_two]
            exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))

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

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

Tactic:
intro a; revert a; dsimp only [Fin.val_mk]
      refine Fin.consInduction ?_ ?_ n
      · intro a
        have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
          (finCongr <| prod_empty).subsingleton
        subsingleton
      · intro n x xs ih a
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
        have := fun i : Fin n =>
          Fintype.prod_equiv (finCongr <| Fin.val_succ i)
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
            fun j => rfl
        simp_rw [this]
        clear this
        simp_rw [Fin.val_zero, Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero,
          Fin.prod_univ_succ, Fin.castLE_zero, Fin.cons_zero, ← Nat.div_div_eq_div_mul,
          mul_left_comm (_ % _ : ℕ), ← mul_sum]
        convert! Nat.mod_add_div _ _
        exact ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _))

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
· have := hs.to_subtype
    have := (hs.image hf).to_subtype
    simp [Nat.card_eq_zero_of_infinite]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Nat.card ↑(graphOn f s) = Nat.card ↑s

Tactic:
rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]

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

Goal state before:
pp: case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0

Tactic:
obtain ⟨_⟩ := (unique_iff_subsingleton_and_nonempty (α := ι)).2 ⟨by assumption, he⟩

Goal state after:
case inr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Subsingleton ι
f : ι → M
he : Nonempty ι
val✝ : Unique ι
⊢ LinearIndependent R f ↔ ∀ (i : ι), f i ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
simp_rw [Module.rank, lift_iSup bddAbove_of_small]

Goal state after:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')

Tactic:
simp_rw [Module.rank, lift_iSup bddAbove_of_small]

Goal state after:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s \ t ∪ s ∩ t).encard = s.encard

Tactic:
sdiff_union_inter

Goal state after:
α : Type u_1
s t : Set α
⊢ s.encard = s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Tactic:
← encard_union_add_encard_inter

Goal state after:
α : Type u_1
s t : Set α
⊢ (s ∪ t).encard ≤ (s ∪ t).encard + (s ∩ t).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : ∃ x, s = {x}
x : α
hx : s = {x}
⊢ s.encard = 1

Tactic:
hx,

Goal state after:
α : Type u_1
s : Set α
x✝ : ∃ x, s = {x}
x : α
hx : s = {x}
⊢ {x}.encard = 1