mathlib-initiative/mathlib-tactics huggingface dataset:
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))
b : κ a
x✝ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
⊢ ∑ i ∈ s.pi t, f a b * ∏ x ∈ s.attach, f (↑x) (i ↑x ⋯) =
    ∑ x ∈ s.pi t, ∏ x_1 ∈ (insert a s).attach, f (↑x_1) (Pi.cons s a b x ↑x_1 ⋯)

Tactic:
refine sum_congr rfl fun g _ => ?_

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))
b : κ a
x✝¹ : b ∈ t a
h₂ : ∀ p₁ ∈ s.pi t, ∀ p₂ ∈ s.pi t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂
g : (a : ι) → a ∈ s → κ a
x✝ : g ∈ s.pi t
⊢ f a b * ∏ x ∈ s.attach, f (↑x) (g ↑x ⋯) = ∏ x ∈ (insert a s).attach, f (↑x) (Pi.cons s a b g ↑x ⋯)
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ Disjoint (map f p) (map f q)

Tactic:
disjoint_iff,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p q : Submodule R M
hpq : Disjoint p q
hker : f.ker ≤ q
⊢ map f p ⊓ map f q = ⊥
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
h : sSup {a | IsAtom a} = ⊤
b : α
⊢ ∃ s, sSupIndep s ∧ IsCompl b (sSup s) ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a

Tactic:
by
  simpa [isCompl_iff, codisjoint_iff, and_assoc]
    using exists_sSupIndep_disjoint_sSup_atoms b ⊤ le_top <| by simpa using h

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

Goal state before:
pp: case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ ComplementedLattice α → IsAtomistic α

Tactic:
intros

Goal state after:
case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
⊢ IsAtomistic α → ComplementedLattice α

Tactic:
intros

Goal state after:
case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : ComplementedLattice α
⊢ IsAtomistic α

pp: case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α

Tactic:
· exact isAtomistic_of_complementedLattice

Goal state after:
case mpr
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
a✝ : IsAtomistic α
⊢ ComplementedLattice α
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Goal state after:
case inl
ι : Type u_5
s : Finset ι
f : ι → ℤ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

case inr
ι : Type u_5
s : Finset ι
f : ι → ℤ
n : ℤ
hf : ∀ i ∈ s, n ∣ f i
hn : n ≠ 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
Module: Mathlib.Data.Finsupp.Indicator

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Zero α
a : ι
f : (j : ι) → j ∈ {a} → α
⊢ indicator {a} f = single a (f a ⋯)

Tactic:
classical
  ext j
  simp only [single_apply, indicator_apply, mem_singleton, @eq_comm _ a j]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : Zero M
a x : α
b : M
⊢ (single a b) x = 0 ↔ x = a → b = 0

Tactic:
by
  classical simp [single_apply, eq_comm]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: case neg
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ abv (-a) = abv a

Tactic:
refine
    (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right ?_

Goal state after:
case neg
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing S
inst✝³ : PartialOrder S
inst✝² : IsOrderedRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
a : R
ha : ¬a = 0
⊢ ¬abv (-a) = -abv a
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:
by rw [abv.map_sub]; apply abv.le_sub

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support

Tactic:
by
  classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

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

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (∏ x ∈ f.support with p x, g x (f x)) * ∏ x ∈ f.support with ¬p x, g x (f x) = f.prod g

Tactic:
Finset.prod_filter_mul_prod_filter_not,

Goal state after:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ ∏ x ∈ f.support, g x (f x) = f.prod g
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝¹ : Zero γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
⊢ ∀ (x y : α ⊕ β →₀ M),
    sumFinsuppEquivProdFinsupp.toFun (x + y) = sumFinsuppEquivProdFinsupp.toFun x + sumFinsuppEquivProdFinsupp.toFun y

Tactic:
intros

Goal state after:
α✝ : 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 γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
⊢ sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝) = sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
⊢ mapDomain f x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
h : mapDomain f x = 0
i : α
⊢ x i = 0 i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : f ≤ 1
⊢ ∏ i, f i < 1 ↔ f < 1

Tactic:
obtain rfl | hf := hf.eq_or_lt <;> simp [*, prod_lt_one]

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
s : Set α
p q : α →₀ M
hp : p ∈ {p | ↑p.support ⊆ s}
hq : q ∈ {p | ↑p.support ⊆ s}
⊢ p + q ∈ {p | ↑p.support ⊆ s}

Tactic:
by
    classical
    refine Subset.trans (Subset.trans (Finset.coe_subset.2 support_add) ?_) (union_subset hp hq)
    rw [Finset.coe_union]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
X : Type u_9
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
⊢ ∀ (m : S) (x : X → M), (lift M R X).toFun (m • x) = (RingHom.id S) m • (lift M R X).toFun x

Tactic:
intros

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
R₂ : Type u_6
R₃ : Type u_7
S : Type u_8
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R₂ N
inst✝³ : AddCommMonoid P
inst✝² : Module R₃ P
σ : R →+* R₂
σ_inv : R₂ →+* R
X : Type u_9
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
m✝ : S
x✝ : X → M
⊢ (lift M R X).toFun (m✝ • x✝) = (RingHom.id S) m✝ • (lift M R X).toFun x✝
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
this : DecidablePred fun x ↦ x ∈ s
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)

Tactic:
haveI := Classical.decPred fun x => x ∈ t

Goal state after:
α : 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
this✝ : DecidablePred fun x ↦ x ∈ s
this : DecidablePred fun x ↦ x ∈ t
⊢ ↥(supported M R s) ≃ₗ[R] ↥(supported M R t)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ x ∈ ↑(map (linearCombination R v) (supported R R s))

Tactic:
apply Exists.elim hx

Goal state after:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
x : M
hx : ∃ x_1 ∈ s, v x_1 = x
⊢ ∀ (a : α), a ∈ s ∧ v a = x → x ∈ ↑(map (linearCombination R v) (supported R R s))
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : (s ∩ mulSupport (f ∘ g)).Finite
hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y
this : ∏ᶠ (i : β) (_ : i ∈ s), f (g i) = ∏ i ∈ hs.toFinset, f (g i)
⊢ g '' s ∩ mulSupport f = ↑(Finset.image g hs.toFinset) ∩ mulSupport f

Tactic:
rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]

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

Goal state before:
pp: n : ℕ
x : { x // x ≠ Fin.last n }
⊢ (finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯

Tactic:
by
  rw [← Option.some_inj]
  simp [finSuccAboveEquiv]

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

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

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

Tactic:
· rcases i with ⟨⟨⟩ | i, hi⟩
    · simp
    · simp only [Nat.add_lt_add_iff_right] at h
      simp [h]

Goal state after:
case neg
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ¬↑i < m + 1
⊢ v ⟨↑i - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) i
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ #(Iic b) = ↑b + 1

Tactic:
by rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑(Finset.image f s)

Tactic:
intro x hx
    rw [mem_mulSupport] at hx
    obtain ⟨a, h, -⟩ := Finset.exists_ne_one_of_prod_ne_one hx
    simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢
    exact ⟨a, 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
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
e : (linearCombination R Subtype.val) (embDomain u (b.repr x)) = ↑⟨x, p⟩
⊢ ⟨x, p⟩ ∉ (embDomain u (b.repr x)).support

Tactic:
simp only [Finset.mem_map, Finsupp.support_embDomain]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
u : ι ↪ ↑w := { toFun := fun i ↦ ⟨b i, ⋯⟩, inj' := ⋯ }
e : (linearCombination R Subtype.val) (embDomain u (b.repr x)) = ↑⟨x, p⟩
⊢ ¬∃ a ∈ (b.repr x).support, u a = ⟨x, p⟩
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ m • f p + f a = n • f p + f b

Tactic:
simpa using congr(f $h)

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ∀ (s : Finset ι) (f g : ι → R'), ∑ i ∈ s, f i • (⇑j ∘ v) i = ∑ i ∈ s, g i • (⇑j ∘ v) i → ∀ i ∈ s, f i = g i

Tactic:
intro S

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
R' : Type u_6
M' : Type u_7
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
⊢ ∀ (f g : ι → R'), ∑ i ∈ S, f i • (⇑j ∘ v) i = ∑ i ∈ S, g i • (⇑j ∘ v) i → ∀ i ∈ S, f i = g i
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
a b : Fin n
⊢ ∏ i ∈ uIcc a.castSucc b.castSucc, f i = ∏ i ∈ uIcc a b, f i.castSucc

Tactic:
by
  simp [← map_castSuccEmb_uIcc]

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

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

Tactic:
by simp [modEq_iff_zsmul, neg_add_eq_sub]

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

Goal state before:
pp: case refine_3.h_zero
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ (b : ι), 0 • v b = 0

Tactic:
intros

Goal state after:
case refine_3.h_zero
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
b✝ : ι
⊢ 0 • v b✝ = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_3.h_add
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ (b : ι) (m₁ m₂ : R), (m₁ + m₂) • v b = m₁ • v b + m₂ • v b

Tactic:
intros

Goal state after:
case refine_3.h_add
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
b✝ : ι
m₁✝ m₂✝ : R
⊢ (m₁✝ + m₂✝) • v b✝ = m₁✝ • v b✝ + m₂✝ • v b✝
Module: Mathlib.Data.Nat.GCD.Basic

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

Tactic:
rw [Coprime, Coprime, gcd_add_self_left]

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

Goal state before:
pp: case inl
n a b : ℕ
h : a ≡ b [MOD n]
h0 : a ≤ b
⊢ n ∣ b - a

pp: case inr
n a b : ℕ
h : a ≡ b [MOD n]
h0 : b ≤ a
⊢ n ∣ b - a

Tactic:
· exact (modEq_iff_dvd' h0).mp h

Goal state after:
case inr
n a b : ℕ
h : a ≡ b [MOD n]
h0 : b ≤ a
⊢ n ∣ b - a
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ∀ (s : Finset ι) (g : ι → R'), ∑ i ∈ s, g i • (⇑j ∘ v) i = 0 → ∀ i ∈ s, g i = 0

Tactic:
intro S

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
R' : Type u_6
M' : Type u_7
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
hv : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
i : R' → R
j : M →+ M'
hi : ∀ (r : R'), i r = 0 → r = 0
hj : ∀ (m : M), j m = 0 → m = 0
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
S : Finset ι
⊢ ∀ (g : ι → R'), ∑ i ∈ S, g i • (⇑j ∘ v) i = 0 → ∀ i ∈ S, g i = 0
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 ∣ ↑a - (↑(n.gcd m) * ↑a + ↑n * n.gcdA m * (↑b - ↑a)) / ↑(n.gcd m)

Tactic:
Int.add_ediv_of_dvd_left,

Goal state after:
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 ∣ ↑a - (↑(n.gcd m) * ↑a / ↑(n.gcd m) + ↑n * n.gcdA m * (↑b - ↑a) / ↑(n.gcd m))

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
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (n * (a / n) + a % n - b) % n

Tactic:
rw [Nat.add_sub_assoc h, mul_add_mod]

Goal state after:
case inr
a b n : ℕ
h : b ≤ a % n
hn : n > 0
⊢ a % n - b = (a % n - b) % n
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Injective f ∧ Surjective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
and_congr_right_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Injective f → (Surjective f ↔ Nat.card α = Nat.card β)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case inl
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj✝ : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
hli : LinearIndependent R (Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x)
hdj : Disjoint s t
x : ι
hx : x ∈ s
⊢ v ↑⟨x, ⋯⟩ = ((Sum.elim (fun x ↦ v ↑x) fun x ↦ v ↑x) ∘ ⇑(Equiv.Set.union hdj)) ⟨x, ⋯⟩

Tactic:
rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 0 < Nat.card ↑s ↔ s.Nonempty

Tactic:
simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, nonempty_iff_ne_empty]

Goal state after: