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

Goal state before:
pp: ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
⊢ ((fun φ i ↦ φ.comp (MonoidHom.mulSingle M i)) ((fun φ ↦ ∏ i, (φ i).comp (evalMonoidHom M i)) φ) i) m = (φ i) m

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.mulSingle_apply,
      MonoidHom.finsetProd_apply, evalMonoidHom_apply, ]

Goal state after:
ι✝ : Type u_1
κ : Type u_2
M✝ : Type u_3
N : Type u_4
R : Type u_5
α : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
M : ι → Type u_8
inst✝¹ : (i : ι) → CommMonoid (M i)
M' : Type u_9
inst✝ : CommMonoid M'
φ : (i : ι) → M i →* M'
i : ι
m : M i
⊢ ∏ x, (φ x) (mulSingle i m x) = (φ i) m
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
ι : Sort u_8
p : ι → Submodule R M
motive : M → Prop
x : M
hx : x ∈ ⨆ i, p i
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
← mem_toAddSubmonoid,

Goal state after:
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 : M → Prop
x : M
hx : x ∈ (⨆ i, p i).toAddSubmonoid
mem : ∀ (i : ι), ∀ x ∈ p i, motive x
zero : motive 0
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive x
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup (s ∪ {a}))

Tactic:
sSup_union,

Goal state after:
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
⊢ Disjoint b (sSup s ⊔ sSup {a})
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h✝ : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup (s \ {x} ∪ {a}))

Tactic:
sSup_union,

Goal state after:
case inr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
b c : α
hbc : b ≤ c
h✝ : sSup {a | a ≤ c ∧ IsAtom a} = c
s : Set α
s_max : ∀ ⦃t : Set α⦄, t ∈ {s | sSupIndep s ∧ Disjoint b (sSup s) ∧ ∀ a ∈ s, IsAtom a ∧ a ≤ c} → s ⊆ t → s = t
s_ind : sSupIndep s
b_inf_Sup_s : Disjoint b (sSup s)
s_atoms : ∀ a ∈ s, IsAtom a ∧ a ≤ c
a : α
ha : a ∈ {a | a ≤ c ∧ IsAtom a}
con : Disjoint a (b ⊔ sSup s)
a_dis_Sup_s : Disjoint a (sSup s)
x : α
hx : x ∈ s ∨ x = a
xa : x ≠ a
h : (s ∪ {a}) \ {x} = s \ {x} ∪ {a}
⊢ Disjoint x (sSup (s \ {x}) ⊔ sSup {a})
Module: Mathlib.Data.Finsupp.Defs

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝ : Zero M
x✝ : α →₀ M
a✝ : α
⊢ (embDomain (Embedding.refl α) x✝) a✝ = (id x✝) a✝

Tactic:
simp [embDomain_apply]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
x✝ : ∃ b, f = single a b
b : M
hb : f = single a b
⊢ f.support ⊆ {a}

Tactic:
hb,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
x✝ : ∃ b, f = single a b
b : M
hb : f = single a b
⊢ (single a b).support ⊆ {a}
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 : α
i : ι
hi : x ∈ s i
⊢ f x ≤ ⨆ i, (s i).mulIndicator f x

Tactic:
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 hf
α : 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
i : ι
i✝ : α
⊢ 1 i✝ ≤ f i i✝

Tactic:
simp [← h1]

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

Goal state before:
pp: case pos
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : b = a
⊢ d b = (single a 1) b

Tactic:
hb,

Goal state after:
case pos
α : Type u_1
d : α →₀ ℕ
h1 : (d.sum fun x n ↦ n) = 1
hd0 : d ≠ 0
a : α
ha : d a ≠ 0 a
hda : d a = 1
hda' : ∀ (i : α), i ≠ a → d i = 0
b : α
hb : b = a
⊢ d a = (single a 1) a
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ f s.prod ≤ (map f s).prod

Tactic:
by
  induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_nonempty_of_submultiplicative f h_mul (by simpa using hs_nonempty)]

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 ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i

Tactic:
by
  have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
  classical
  calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]

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

Goal state before:
pp: case c0
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∀ (i : ι), i ∈ s → f i ≤ g i) → (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ (map f s).prod

Tactic:
grind [prod_nonneg]

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

Goal state before:
pp: α : Type u_12
M : Type u_13
inst✝ : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f = g

Tactic:
have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
    refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
    exact mk_mem_graph _ (hsup ▸ hx)

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

Goal state before:
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

Tactic:
apply prod_pos

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
⊢ ∀ (a : R), a ∈ map f s → 0 < a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α →₀ γ
val✝ : α
⊢ (embDomain Embedding.inl a) (Sum.inl val✝) = (a.sumElim 0) (Sum.inl val✝)

Tactic:
simp [embDomain_apply]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
a : α →₀ γ
val✝ : β
⊢ (embDomain Embedding.inl a) (Sum.inr val✝) = (a.sumElim 0) (Sum.inr val✝)

Tactic:
simp [embDomain_apply]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β →₀ γ
val✝ : α
⊢ (embDomain Embedding.inr b) (Sum.inl val✝) = (sumElim 0 b) (Sum.inl val✝)

Tactic:
simp [embDomain_apply]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Zero γ
b : β →₀ γ
val✝ : β
⊢ (embDomain Embedding.inr b) (Sum.inr val✝) = (sumElim 0 b) (Sum.inr val✝)

Tactic:
simp [embDomain_apply]

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 : Finset ι
inst✝ : MulLeftStrictMono M
i j : ι
hij : j ≠ i
hi : i ∈ s
hj : j ∈ s
hlt : 1 < f j
hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k
⊢ f i = ∏ k ∈ {i}, f k

Tactic:
rw [prod_singleton]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) = (map (fun k ↦ powersetCard k x) (range (x.card + 1))).sum

Tactic:
← Finset.range_val,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) =
    (map (fun k ↦ powersetCard k x) (Finset.range (x.card + 1)).val).sum
Module: Mathlib.Algebra.BigOperators.Finprod

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

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

Tactic:
exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
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
α' : Type u_7
s : Set α
t : Set α'
e : ↑s ≃ ↑t
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

Tactic:
haveI := Classical.decPred fun x => x ∈ s
  haveI := Classical.decPred fun x => x ∈ t
  exact Finsupp.supportedEquivFinsupp s ≪≫ₗ
    (Finsupp.domLCongr e ≪≫ₗ (Finsupp.supportedEquivFinsupp t).symm)

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ (mulSupport fun i ↦ f i * g i) ⊆ ↑(Finite.toFinset hf ∪ Finite.toFinset hg)

Tactic:
simp only [Finset.coe_union, Finite.coe_toFinset, mulSupport_subset_iff,
      mem_union, mem_mulSupport]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
hf : HasFiniteMulSupport f
hg : HasFiniteMulSupport g
⊢ ∀ (x : α), f x * g x ≠ 1 → f x ≠ 1 ∨ g x ≠ 1
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 : ι
hbi : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexFinsetRange ⟨b i, hbi⟩ = ↑⟨b i, hbi⟩

Tactic:
exact b.reindexFinsetRange_self i

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

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

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

Tactic:
· simp only [g.map_finprod_Prop]

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

Goal state before:
pp: α : Type u
x : α
u : Fin 0 → α
⊢ ∀ (i : Fin 1), vecCons x u i = x

Tactic:
rw [Fin.forall_fin_one]
  rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝² : AddCommMonoid M
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Module R M
b : Basis ι R M
⊢ LinearIndependent R b.coord

Tactic:
refine linearIndependent_iff'ₛ.mpr fun s l₁ l₂ h j hj ↦ ?_

Goal state after:
ι : Type u_1
M : Type u_5
inst✝² : AddCommMonoid M
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Module R M
b : Basis ι R M
s : Finset ι
l₁ l₂ : ι → R
h : ∑ i ∈ s, l₁ i • b.coord i = ∑ i ∈ s, l₂ i • b.coord i
j : ι
hj : j ∈ s
⊢ l₁ j = l₂ j
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
inst✝ : Fintype ι
⊢ (∀ ⦃a₁ a₂ : ι → R⦄, ∑ i, a₁ i • v i = ∑ i, a₂ i • v i → a₁ = a₂) ↔
    ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i

Tactic:
funext_iff

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
hf : ∀ (j : Fin b), f (natAdd a j) = 1
⊢ ∏ i, f i = ∏ i, f (castAdd b i)

Tactic:
rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : LinearIndependent R v
w : ι → G
⊢ LinearIndependent R (w • v)

Tactic:
rw [linearIndependent_iff''ₛ] at hv ⊢
  intro s g₁ g₂ hgs hsum i
  refine (Group.isUnit (w i)).smul_left_cancel.mp ?_
  refine hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i
  · simp_rw [hgs i hi]
  · simpa only [smul_assoc, smul_comm] using! hsum

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

Goal state before:
pp: G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a : Fin (n + 1)
⊢ partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) = partialProd g ∘ a.succ.succAbove

Tactic:
ext i
  refine inductionOn i ?_ ?_
  · simp
  · intro i hi
    simp only [Function.comp_apply, succ_succAbove_succ] at *
    rw [partialProd_succ, partialProd_succ, hi]
    rcases lt_trichotomy (i : ℕ) a with (h | h | h)
    · rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h,
        succAbove_of_castSucc_lt] <;>
      simp only [lt_def, val_castSucc, val_succ] <;>
      lia
    · rw [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h,
        succAbove_of_le_castSucc, castSucc_succ, partialProd_succ, mul_assoc] <;>
      simp only [castSucc_lt_succ_iff, le_def, val_castSucc] <;>
      lia
    · rw [succAbove_of_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h,
        castSucc_succ] <;>
      simp only [le_def, val_succ, val_castSucc] <;>
      lia

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

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
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : (Finsupp.linearCombination R v) l₂ = (Finsupp.linearCombination R v) l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0

Tactic:
rw [hv.finsuppLinearCombination_injective.eq_iff] at H

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 : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : l₂ = l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)

Tactic:
rw [mul_mod_mul_left, mul_mod_mul_left, h]

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:
exact h.mul_left' c

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

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

Tactic:
induction n with
      | zero => subsingleton [(finCongr <| pow_zero _).subsingleton]
      | succ n ih =>
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
          mul_one, pow_succ', ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
        rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]

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

Goal state before:
pp: case neg
a b c : ℕ
h : ¬c = 0
⊢ (a + b) / c ≤ a / c + b / c + 1

Tactic:
rw [Nat.add_div (Nat.pos_of_ne_zero h), Nat.add_le_add_iff_left]

Goal state after:
case neg
a b c : ℕ
h : ¬c = 0
⊢ (if c ≤ a % c + b % c then 1 else 0) ≤ 1
Module: Mathlib.SetTheory.Cardinal.Finite

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

Tactic:
by
  simp only [← not_le, Cardinal.natCast_le_toENat]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard + (s ∩ t).encard = (t \ s).encard + (s ∩ t).encard ↔ (s \ t).encard = (t \ s).encard

Tactic:
(ENat.addLECancellable_of_lt_top h.encard_lt_top).inj_left

Goal state after:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ (s \ t).encard = (t \ s).encard ↔ (s \ t).encard = (t \ s).encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ (insert a t).encard = t.encard + 1

Tactic:
encard_insert_of_notMem h

Goal state after:
case refine_2
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ t.encard + 1 = t.encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < s.encard

Tactic:
← encard_sdiff_singleton_add_one ha

Goal state after:
α : Type u_1
s : Set α
x✝ : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard < (s \ {a}).encard + 1
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
inst✝ : Fintype ι
H : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∀ i ∉ s, g i = 0
hs : ∑ i ∈ s, g i • v i = 0
i✝ i : ι
x✝ : i ∈ Finset.univ
hi : i ∉ s
⊢ g i • v i = 0

Tactic:
rw [hg i hi, zero_smul]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ ?_⟩
  · obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
    rw [← insert_eq_of_mem hx, ← insert_sdiff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (3 : ℕ∞) = 2 + 1),
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left, encard_eq_two] at h
    obtain ⟨y, z, hne, hs⟩ := h
    refine ⟨x, y, z, ?_, ?_, hne, ?_⟩
    · rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr rfl)).2 rfl
    rw [← hs, insert_sdiff_singleton, insert_eq_of_mem hx]
  rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton] <;> aesop

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ ∃ m v, LinearIndependent R (Subtype.val ∘ v) ∧ m ≠ 0

Tactic:
refine ⟨1, fun _ => ⟨x, hx⟩, ?_, one_ne_zero⟩

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ LinearIndependent R (Subtype.val ∘ fun x_1 ↦ ⟨x, hx⟩)
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.toENat (Cardinal.mk α)

Tactic:
rw [Cardinal.natCast_eq_toENat]

Goal state after:
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
⊢ s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k

Tactic:
encard_le_coe_iff,

Goal state after:
α : Type u_1
s : Set α
k : ℕ
⊢ (s.Finite ∧ ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k) ↔ s.Finite ∧ s.ncard ≤ k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).encard = s.encard + 1

Tactic:
encard_insert_of_notMem h

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ s.encard + 1 = s.encard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard = Nat.card α - s.ncard

Tactic:
by
  rw [← ncard_add_ncard_compl s hs hsc, Nat.add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (∃ a, s = {a}) → s.ncard = 1

Tactic:
by rintro ⟨a, rfl⟩; rw [ncard_singleton]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
d : Con N
e : M ≃* N
h : c = comap ⇑e ⋯ d
⊢ ∀ (a₁ a₂ : M), c.toSetoid a₁ a₂ ↔ d.toSetoid (↑e a₁) (↑e a₂)

Tactic:
by apply Con.ext_iff.mp h

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

Goal state before:
pp: case refl
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 x : N
a b : M
fa : f a = x
fb : f b = x
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
rw [f.injective (fa.trans fb.symm)]
    exact ConGen.Rel.refl _

Goal state after: