mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
x : γ
⊢ (equivMapDomain (f.trans g) l) x = (equivMapDomain g (equivMapDomain f l)) x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
⊢ equivMapDomain (f.trans g) = equivMapDomain g ∘ equivMapDomain f

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
x : α →₀ M
a✝ : γ
⊢ (equivMapDomain (f.trans g) x) a✝ = ((equivMapDomain g ∘ equivMapDomain f) x) a✝
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
⊢ equivMapDomain f (single a b) = single (f a) b

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
x : β
⊢ (equivMapDomain f (single a b)) x = (single (f a) b) x
Module: Mathlib.Algebra.Order.BigOperators.GroupWithZero.List

Goal state before:
pp: case h₂.h0
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
i : ι
hi : i ∈ s
⊢ 0 < f i

Tactic:
apply h0

Goal state after:
case h₂.h0
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
i : ι
hi : i ∈ s
⊢ i ∈ a :: s
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : 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
inst✝ : Zero M
f✝ : α ≃ β
f : α →₀ M
⊢ equivMapDomain f✝.symm (equivMapDomain f✝ f) = f

Tactic:
ext x

Goal state after:
case refine_1
α : 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
inst✝ : Zero M
f✝ : α ≃ β
f : α →₀ M
x : α
⊢ (equivMapDomain f✝.symm (equivMapDomain f✝ f)) x = f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_2
α : 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
inst✝ : Zero M
f✝ : α ≃ β
f : β →₀ M
⊢ equivMapDomain f✝ (equivMapDomain f✝.symm f) = f

Tactic:
ext x

Goal state after:
case refine_2
α : 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
inst✝ : Zero M
f✝ : α ≃ β
f : β →₀ M
x : β
⊢ (equivMapDomain f✝ (equivMapDomain f✝.symm f)) x = f x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_12
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
⊢ equivMapDomain f l = mapDomain (⇑f) l

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_12
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ (equivMapDomain f l) x = (mapDomain (⇑f) l) x
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

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

Tactic:
forall_mem_insert,

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
s : Multiset (α →₀ M)
a : α
h : a ∈ (Multiset.sum 0).support
⊢ False

Tactic:
simp at h

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

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝ : DecidableEq α
f : β → Multiset α
⊢ ∅.sum f = ∅.sup f ↔ ∀ x ∈ ∅, ∀ y ∈ ∅, x ≠ y → Disjoint (f x) (f y)

Tactic:
simp only [Finset.notMem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
      Finset.sup_empty, bot_eq_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
⊢ f ∘ₗ f.splittingOfFinsuppSurjective s = id

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ (((f ∘ₗ f.splittingOfFinsuppSurjective s) ∘ₗ lsingle x) 1) a✝ = ((id ∘ₗ lsingle x) 1) a✝
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
x : PLift α
h : x ∈ mulSupport fun x ↦ (fun x ↦ 1) x.down
⊢ x ∈ ↑∅

Tactic:
simp at h

Goal state after:
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)
c : α'
hc : c ∈ l.support
⊢ (f ∘ Function.invFunOn f s) c = _root_.id c

Tactic:
exact Function.invFunOn_eq (by simpa using hl hc)

Goal state after:
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
α' : 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
⊢ l = 0

Tactic:
ext x

Goal state after:
α : 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 : α
⊢ l x = 0 x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
⊢ ∏ᶠ (_ : f a ≠ 1), f a = f a

Tactic:
rw [← mem_mulSupport, finprod_eq_mulIndicator_apply, mulIndicator_mulSupport]

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 : Finset α
h : mulSupport f ⊆ ↑s
⊢ mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f

Tactic:
rw [mulSupport_comp_eq_preimage]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
⊢ PLift.down ⁻¹' mulSupport f = ⇑Equiv.plift.symm '' mulSupport f
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

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
v : α → M
⊢ (linearCombination R v).range = span R (Set.range v)

Tactic:
ext x

Goal state after:
α : 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 ∈ (linearCombination R v).range ↔ x ∈ span R (Set.range v)
Module: Mathlib.Data.Finset.Fin

Goal state before:
pp: n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ ↑(image Fin.val (s.attachFin h)) = ↑s

Tactic:
coe_image,

Goal state after:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ Fin.val '' ↑(s.attachFin h) = ↑s
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
⊢ range val = Iio n

Tactic:
by ext; simp [Fin.exists_iff]

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' uIcc i j = uIcc ↑i ↑j

Tactic:
simp [uIcc]

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 : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : HasFiniteMulSupport f
⊢ s ∩ mulSupport f = ↑({i ∈ Finite.toFinset hf | i ∈ s}) ∩ mulSupport f

Tactic:
ext x

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : HasFiniteMulSupport f
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ ↑({i ∈ Finite.toFinset hf | i ∈ s}) ∩ mulSupport f
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
R₁ : Type u_13
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
⊢ f₁ = f₂

Tactic:
ext x

Goal state after:
ι : 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
R₁ : Type u_13
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
⊢ s ∩ mulSupport f = t ∩ mulSupport f

Tactic:
ext x

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f
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
R₁ : Type u_13
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
⊢ f₁ = f₂

Tactic:
ext x

Goal state after:
ι : 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
R₁ : Type u_13
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
x : M
⊢ f₁ x = f₂ x
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
ι : 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
e : ι ≃ ι'
⊢ (b.reindex e).sumCoords = b.sumCoords

Tactic:
ext x

Goal state after:
ι' : Type u_2
ι : 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
e : ι ≃ ι'
x : M
⊢ (b.reindex e).sumCoords x = b.sumCoords x
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #{x | p x} = (if p 0 then 1 else 0) + #{x | p x.succ}

Tactic:
by
  rw [card_filter_univ_succ]; split_ifs <;> simp [add_comm]

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg.zero
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
hi : 0 < o + 1
h : ¬↑⟨0, hi⟩ < m + 1
⊢ v ⟨↑⟨0, hi⟩ - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) ⟨0, hi⟩

Tactic:
simp at h

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

Goal state before:
pp: n : ℕ
b : Fin n
⊢ 0 < b → Iic (b - 1) = Iio b

Tactic:
by
  grind [= Fin.val_sub_one_of_ne_zero]

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
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ i ∈ ⋯.toFinset, ∏ b ∈ s, f i b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
Finset.prod_comm

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
⊢ ∏ y ∈ s, ∏ x ∈ ⋯.toFinset, f x y = ∏ b ∈ s, ∏ᶠ (a : α), f a b
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
hU : (mulSupport fun a ↦ ∏ b ∈ s, f a b) ⊆ ↑⋯.toFinset
b : β
hb : b ∈ s
a : α
ha : a ∈ mulSupport fun x ↦ f x b
⊢ ∃ i, ∃ (_ : i ∈ ↑s), a ∈ mulSupport fun a ↦ f a i

Tactic:
exact ⟨b, hb, ha⟩

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

Goal state before:
pp: case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ↑m • p + -(↑n • p) = b - a

Tactic:
← sub_eq_add_neg,

Goal state after:
case h
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
m n : ℕ
h : m • p + a = n • p + b
⊢ ↑m • p - ↑n • p = b - a
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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
⊢ LinearIndependent R' (⇑j ∘ v)

Tactic:
obtain ⟨i', hi'⟩ := hi.hasRightInverse
  refine hv.map_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
  · apply_fun i at h
    rwa [hi', hi'] at h
  rw [hc (i' r) m, hi']

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

Goal state before:
pp: case e'_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : ι → M
h : EqOn v w s
⊢ (fun x ↦ w ↑x) = fun x ↦ v ↑x

Tactic:
ext x

Goal state after:
case e'_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w : ι → M
h : EqOn v w s
x : ↑s
⊢ w ↑x = v ↑x
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ (n - m).gcd n = 1 ↔ m.gcd n = 1

Tactic:
gcd_self_sub_left h

Goal state after:
m n : ℕ
h : m ≤ n
⊢ m.gcd n = 1 ↔ m.gcd n = 1
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
dsimp
      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 left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑n * (n.gcdA m * ((↑b - ↑a) / ↑(n.gcd m)))

Tactic:
exact dvd_mul_right _ _

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

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ n.gcd m ∣ n.gcd m * a

Tactic:
exact dvd_mul_right _ _

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

Goal state before:
pp: case right.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑m * n.gcdB m = ↑n * n.gcdA m
⊢ ↑m ∣ ↑m * (n.gcdB m * ((↑b - ↑a) / ↑(n.gcd m)))

Tactic:
exact dvd_mul_right _ _

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) +
      ∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i) =
    0

Tactic:
rw [Finset.sum_preimage' (g := fun x => g x • v x),
      Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ ∑ x ∈ s with x ∈ range Sum.inl ∨ x ∈ range Sum.inr, g x • v x = 0

ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ Disjoint ({x ∈ s | x ∈ range Sum.inl}) ({x ∈ s | x ∈ range Sum.inr})
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
⊢ [].alternatingProd = ∏ i, [][i] ^ (-1) ^ ↑i

Tactic:
alternatingProd,

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
⊢ 1 = ∏ i, [][i] ^ (-1) ^ ↑i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
⊢ g i • ⇑i = g i • ⇑a

Tactic:
ext x

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x : G
⊢ (g i • ⇑i) x = (g i • ⇑a) x
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ₒₛ]
  refine ⟨fun h t f heq i => ?_, fun h t₁ t₂ f ht₁t₂ heq => ?_⟩
  · specialize h t tᶜ f disjoint_compl_right heq
    by_cases hi : i ∈ t
    · exact h.1 i hi
    · exact h.2 i (Finset.mem_compl.2 hi)
  · specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_
    · rw [← Finset.sum_subset ht₁t₂.le_compl_left]
      · convert! heq using 2 with i hi i hi <;> simp [hi]
      · intro i hi hi'
        simp [Finset.mem_compl.1 hi, hi']
    refine ⟨fun i hi => ?_, fun i hi => ?_⟩ <;> simpa [hi] using h i

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

Goal state before:
pp: α : Type u_1
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
⊢ {x | x ≠ a} ∪ {a} = univ

Tactic:
ext x

Goal state after:
α : Type u_1
a : α
this : {x | x ≠ a}.encard + {a}.encard = ({x | x ≠ a} ∪ {a}).encard
x : α
⊢ x ∈ {x | x ≠ a} ∪ {a} ↔ x ∈ univ
Module: Mathlib.LinearAlgebra.Dimension.Basic

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

Tactic:
apply le_antisymm
  · exact f.toLinearMap.lift_rank_le_of_injective f.injective
  · exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective

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

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

Tactic:
by
  apply le_antisymm
  · exact f.toLinearMap.lift_rank_le_of_injective f.injective
  · exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective

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

Goal state before:
pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w

pp: case refine_1.refine_4
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}

Tactic:
· rintro rfl; exact (hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl

Goal state after:
case refine_1.refine_4
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case succ
α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : ↑n.succ ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ↑n.succ

Tactic:
obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)

Goal state after:
case succ
α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : ↑n.succ ≤ s.encard
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
⊢ ∃ t ⊆ s, t.encard = ↑n.succ