mathlib-initiative/mathlib-tactics huggingface dataset:
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✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0

Tactic:
rw [linearIndependent_iffₒₛ]

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
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
    ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : 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 ι
s : Finset ι
h : ∀ (t : Finset ↑↑s) (f : ↑↑s → R), ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i → ∀ (i : ↑↑s), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
⊢ (∑ i ∈ s, if i ∈ t then f i • v i else 0) = ∑ i ∈ s, if i ∉ t then f i • v i else 0

Tactic:
simpa [Finset.inter_eq_right.2 ht, Finset.sum_ite, Finset.filter_notMem_eq_sdiff]

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

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
⊢ s.encard = ⊤

Tactic:
have := h.to_subtype
  rw [encard, ENat.card_eq_top_of_infinite]

Goal state after:
Module: Mathlib.Algebra.EuclideanDomain.Int

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs

Tactic:
← Int.natAbs_pos

Goal state after:
a b : ℤ
b0 : 0 < b.natAbs
⊢ a.natAbs * 1 ≤ a.natAbs * b.natAbs
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s.encard - {x}.encard ≤ (s \ {x}).encard

Tactic:
apply tsub_encard_le_encard_sdiff

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton

Tactic:
encard_le_one_iff,

Goal state after:
α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ s.Subsingleton
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : x ∉ {a}
⊢ f₀ x = Function.update f₀ a b x

Tactic:
Function.update_of_ne

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : x ∉ {a}
⊢ f₀ x = f₀ x

case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : x ∉ {a}
⊢ x ≠ a
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H

Tactic:
have : j ≠ i := fun h => h ▸ hnotMem <| hj

Goal state after:
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
P : α → Prop
s : Set α
⊢ {x | ↑x ∈ s}.ncard = (s ∩ ofPred P).ncard

Tactic:
convert! (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm
  ext x
  simp [← and_assoc, exists_eq_right]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ ((∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z =
    (∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ((∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z)

Tactic:
Finset.sum_mul

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
c d : A
⊢ (∑ i ∈ (b.repr c).support, (b.repr c) i • b i * ∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z =
    (∑ a ∈ (b.repr c).support, (b.repr c) a • b a) * ((∑ a ∈ (b.repr d).support, (b.repr d) a • b a) * z)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s

Tactic:
intro h
    apply (h y).mpr
    rw [inv_mul_cancel]
    exact s.one_mem

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

Goal state before:
pp: case convert_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ ∀ (a : α) (ha : a ∈ s.toFinset), f'' a ha ∈ t.toFinset

Tactic:
simp [f'', hf]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ (leftRel (H.subgroupOf s)) a b → (leftRel (H.subgroupOf t)) ((inclusion h) a) ((inclusion h) b)

Tactic:
by
      simp_rw [leftRel_eq]
      exact id

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

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

Tactic:
rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ sSup S = ringConGen fun x y ↦ ∃ c ∈ S, c x y

Tactic:
sSup_def

Goal state after:
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ ringConGen (sSup (DFunLike.coe '' S)) = ringConGen fun x y ↦ ∃ c ∈ S, c x y
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0

Tactic:
exact hb _ ((hIJ.top_le trivial).resolve_left hiI)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ comap (p.liftQ f h) q ≤ map p.mkQ (comap f q)

Tactic:
by rintro ⟨x⟩ hx; exact ⟨_, hx, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
a b : α
⊢ ↑(Ico (succ a) b) = ↑(Ioo a b)

Tactic:
by simpa using Set.Ico_succ_left_eq_Ioo _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (m, 0) + (0, n) ∈ fst R M M₂ ⊔ snd R M M₂

Tactic:
apply Submodule.add_mem (Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂)

Goal state after:
case h₁
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (m, 0) ∈ fst R M M₂ ⊔ snd R M M₂

case h₂
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
m : M
n : M₂
⊢ (0, n) ∈ fst R M M₂ ⊔ snd R M M₂
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ (Iic i).sup' ⋯ f ≤ ⨆ i_1, f ↑i_1

pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f

Tactic:
· exact sup'_le _ _ fun j hj ↦ Finite.le_ciSup_of_le
      ⟨j, by simpa only [Set.mem_Iic, mem_Iic] using hj⟩ le_rfl

Goal state after:
case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
⊢ y - x ∈ f.ker ⊔ g.ker

Tactic:
simp only [h, mem_top]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ ((Iio i).sup fun i_1 ↦ f i ⊓ f i_1) = ⊥

Tactic:
sup_congr rfl <| fun j hj ↦ disjoint_iff.mp <| (hf _ (mem_Iio.mp hj)).symm

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ ((Iio i).sup fun j ↦ ⊥) = ⊥
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i = j
⊢ ∃ n, succ^[n] i = j

Tactic:
refine ⟨0, ?_⟩
      simpa only [Function.iterate_zero, id] using hij

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups f) n

Tactic:
← partialSups_disjointed,

Goal state after:
ι : Type u_2
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
α : Type u_3
f : ι → Set α
n : ι
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups (disjointed f)) n
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (partialSups t) n

Tactic:
← partialSups_disjointed,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : DecidableEq α
n : ι
t : ι → Finset α
⊢ (Iic n).disjiUnion (disjointed t) ⋯ = (partialSups (disjointed t)) n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ (if 0 ≤ toZ hι.some i then succ^[(toZ hι.some i).toNat] hι.some else pred^[(-toZ hι.some i).toNat] hι.some) = i

Tactic:
if_pos h_nonneg

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ succ^[(toZ hι.some i).toNat] hι.some = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
simp_rw [if_pos h_nonneg]

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : hι.some ≤ i
h_nonneg : 0 ≤ toZ hι.some i
⊢ succ^[(toZ hι.some i).toNat] hι.some = i
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: case right
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ b * b = b

Tactic:
· conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + b * a + (a * b + b) = a + b

Tactic:
add_add_add_comm,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + a * b + (b * a + b) = a + b
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * 2 ^ (n - 1)

Tactic:
by_cases h : n = 0
  · simp [h]
  apply (mul_right_inj' two_ne_zero).1
  calc
    2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]

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

Goal state before:
pp: M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (mapDomain f (∑ a, Finsupp.single a (s a))) y = ∑ x with f x = y, equivFunOnFinite s x

Tactic:
rw [Finsupp.mapDomain_finsetSum]

Goal state after:
M : Type u_5
inst✝³ : AddCommMonoid M
X : Type u_6
Y : Type u_7
inst✝² : Fintype X
inst✝¹ : Finite Y
inst✝ : DecidableEq Y
f : X → Y
y : Y
s : X →₀ M
⊢ equivFunOnFinite (∑ i, mapDomain f (Finsupp.single i (s i))) y = ∑ x with f x = y, equivFunOnFinite s x
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ kernImage m s ∪ t = t

Tactic:
union_eq_right.mpr hst

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s✝ : Set α
t✝ : Set β
m : α → β
f : Filter α
t : Set β
s : Set α
hs : s ∈ f.sets
hst : kernImage m s ⊆ t
⊢ t = t
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ map f₁ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂

Tactic:
map_congr hl

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
l₁ : Filter α
l₂ : Filter β
hl : f₁ =ᶠ[l₁] f₂
⊢ map f₂ l₁ ≤ l₂ ↔ map f₂ l₁ ≤ l₂
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter (α ⊕ β)
m₁ : α → γ
m₂ : β → γ
⊢ map (Sum.elim m₁ m₂) l = map m₁ (comap inl l) ⊔ map m₂ (comap inr l)

Tactic:
← map_comap_inl_sup_map_comap_inr l

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter (α ⊕ β)
m₁ : α → γ
m₂ : β → γ
⊢ map (Sum.elim m₁ m₂) (map inl (comap inl l) ⊔ map inr (comap inr l)) =
    map m₁ (comap inl (map inl (comap inl l) ⊔ map inr (comap inr l))) ⊔
      map m₂ (comap inr (map inl (comap inl l) ⊔ map inr (comap inr l)))
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
⊢ (∀ B ∈ F, f x ∈ B) → ∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A

Tactic:
· intro h V U U_in f_U_V
    exact f_U_V (h U U_in)

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) = map f F ⊓ G

Tactic:
by
  apply le_antisymm
  · calc
      map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
      _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le
  · rintro U ⟨V, V_in, W, ⟨Z, Z_in, hZ⟩, h⟩
    apply mem_inf_of_inter (image_mem_map V_in) Z_in
    calc
      f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
H : Filter β
hHG : H ≤ G
⊢ map m ((fun x ↦ F ⊓ comap m x) H) = H

Tactic:
by simpa [Filter.push_pull] using hHG.trans hm

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
let f : Fin n ≃ ULift (Fin n) := Equiv.ulift.symm

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
f : Fin n ≃ ULift.{?u.25, 0} (Fin n) := Equiv.ulift.symm
⊢ ∃ G' x x_1, Nonempty (G ≃* G')
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ map Subtype.val atTop = atTop

Tactic:
have : IsDirectedOrder s := by
    rw [directedOn_iff_directed] at this
    rwa [IsDirectedOrder, ← directed_id_iff]

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
this : IsDirectedOrder ↑s
⊢ map Subtype.val atTop = atTop
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupClosedOn univ sᶜ ↔ DirSupInacc s

Tactic:
dirSupClosedOn_compl,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupInaccOn univ s ↔ DirSupInacc s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
hM : Module.Finite R M
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
⊢ Module.Finite S P

Tactic:
by
  rw [Module.finite_def, Submodule.fg_def] at hM ⊢
  obtain ⟨s, hsfin, hs⟩ := hM
  refine ⟨f '' s, hsfin.image f, eq_top_iff.mpr fun p _ ↦ ?_⟩
  exact image_span_subset_span f s (by simpa [hs] using hf p)

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d ⊆ {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
⊢ b ∈ {a}

Tactic:
rw [hdn.subset_singleton_iff] at hda

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
d : Set α
hda : d = {a}
hdn : d.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
b : α
hb : IsLUB d b
⊢ b ∈ {a}
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ IsLUB (f '' s) (f a)

Tactic:
by
  refine ⟨?_, fun b hb ↦ ?_⟩
  · simpa [mem_upperBounds, hf.strictMono.le_iff_le] using hs.1
  · by_cases ha : a ∈ s
    · simp_all [mem_upperBounds]
    · have ha' := hs.isSuccLimit_of_notMem hs' ha
      rw [le_iff_forall_le hf ha']
      intro c hc
      obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc
      simp_rw [mem_upperBounds, forall_mem_image] at hb
      exact (hf.strictMono hcd).le.trans (hb hd)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ typeLT ↑s = typeLT α

Tactic:
by
  apply (RelEmbedding.ofMonotone Subtype.val (by simp)).ordinal_type_le.antisymm
  rw [← ord_cardinalMk, ord_le, card_type, ← cof_eq_cardinalMk]
  exact cof_le hs

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_2
inst✝² : ConditionallyCompleteLinearOrderBot α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ ↑((enum s hs) ⊥) = sInf s

Tactic:
by
  let : Bot s := ⟨⟨sInf s, csInf_mem hs.nonempty⟩⟩
  let : OrderBot s := .mk fun a ↦ csInf_le' a.2
  rw [OrderIso.map_bot]
  rfl

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≃r s)
f : r ≃r s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≃r ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
· exact (RelIso.preimage Equiv.ulift r).trans <| f.trans (RelIso.preimage Equiv.ulift s).symm

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit b
⊢ a * b ≤ c ↔ ∀ b' < b, a * b' ≤ c

Tactic:
refine ⟨fun h _ l ↦ (mul_le_mul_right l.le _).trans h, fun H ↦ le_of_not_gt ?_⟩

Goal state after:
a b c : Ordinal.{u_4}
h : IsSuccLimit b
H : ∀ b' < b, a * b' ≤ c
⊢ ¬c < a * b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : (#α).ord ≤ type s
⊢ #α ≤ (type s).card

Tactic:
rw [e] at h

Goal state after:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : type r ≤ type s
⊢ #α ≤ (type s).card