mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ span R (v '' {x})

Tactic:
rw [Set.image_singleton]

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✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ R ∙ v x
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c d : ℕ
h₁ : ↑n ∣ ↑b - ↑a
h₂ : ↑n ∣ ↑b - ↑a + (↑d - ↑c)
⊢ ↑d - ↑c = ↑b - ↑a + (↑d - ↑c) - (↑b - ↑a)

Tactic:
rw [add_sub_cancel_left]

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

Goal state before:
pp: n a b m : ℕ
h : a ≡ b [MOD m * n]
⊢ a ≡ b [MOD n]

Tactic:
rw [modEq_iff_dvd] at *

Goal state after:
n a b m : ℕ
h : ↑(m * n) ∣ ↑b - ↑a
⊢ ↑n ∣ ↑b - ↑a
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
⊢ ∃ a, f a = i

Tactic:
have h_total_l : Finsupp.linearCombination R v l = v i := by
    dsimp only [l]
    rw [Finsupp.linearCombination_mapDomain]
    rw [(hv.comp f f.injective).linearCombination_repr]

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
⊢ ∃ a, f a = i
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
⊢ i.Maximal ↔ ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j

Tactic:
by
  constructor
  · rintro p κ w i' j rfl
    specialize p (range w) i'.linearIndepOn_id (range_comp_subset_range _ _)
    rw [range_comp, ← image_univ (f := w)] at p
    exact range_eq_univ.mp (image_injective.mpr i'.injective p)
  · intro p w i' h
    specialize
      p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
        (by
          ext
          simp)
    have q := congr_arg (fun s => ((↑) : w → M) '' s) p.range_eq
    rw [← image_univ, image_image] at q
    simpa using q

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

Goal state before:
pp: m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]

Tactic:
replace h := h.of_dvd hdm

Goal state after:
m a b d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: 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 * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m) ∧
    ↑m ∣ ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)

Tactic:
constructor <;> rw [Int.emod_def, ← sub_add]

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

case right
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
⊢ ↑m ∣
    ↑b - (↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) +
      ↑(n.lcm m) * ((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) / ↑(n.lcm m))
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
⊢ LinearIndependent R (Fin.cons x v ∘ ⇑(finRotate (m + 1)))

Tactic:
exact (linearIndependent_equiv _).mpr (.finCons' x v hli x_ortho)

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
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (range (v ∘ Sum.inl))) (span R (range (v ∘ Sum.inr)))

Tactic:
rw [range_comp v, range_comp v]

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
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
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
⊢ ∑ x ∈ s with x ∈ range Sum.inl, g x • v x + ∑ x ∈ s with x ∈ range Sum.inr, g x • v x = 0

Tactic:
← Finset.sum_union,

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 ∈ {x ∈ s | x ∈ range Sum.inl} ∪ {x ∈ s | 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.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
hc0 : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
by simp [hc0]

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

Goal state before:
pp: case neg
ι : 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
this✝ : Sub R := ⋯
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ g i ≤ f i

Tactic:
simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩

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

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

Tactic:
have := hs.to_subtype

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Infinite
this : Infinite ↑s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : 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 ι
hdj : Disjoint s t
⊢ LinearIndepOn R v (s ∪ t) ↔ LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (span R (v '' s)) (span R (v '' t))

Tactic:
refine ⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right, ?_⟩,
    fun h ↦ h.1.union h.2.1 h.2.2⟩
  convert! h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _) <;>
  aesop

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
⊢ α ≃ Fin (Nat.card α)

Tactic:
cases fintypeOrInfinite α
  · simpa only [card_eq_fintype_card] using Fintype.equivFin α
  · simp only [card_eq_zero_of_infinite, ne_eq, not_true_eq_false] at h

Goal state after:
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
x y : G
⊢ ∑ i ∈ insert a s, g i * i x * i y - ∑ i ∈ insert a s, g i * a x * i y =
    ∑ i ∈ insert a s, g i * (i x * i y) - ∑ i ∈ insert a s, a x * (g i * i y)

Tactic:
congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_

Goal state after:
case refine_1
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 y : G
i : G →* L
⊢ g i * i x * i y = g i * (i x * i y)

case refine_2
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 y : G
i : G →* L
⊢ g i * a x * i y = a x * (g i * i y)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : IsEmpty β
⊢ card (α → β) = card β ^ ⊤

Tactic:
rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]

Goal state after:
case inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_0 : IsEmpty β
⊢ IsEmpty (α → β)
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
s : Finset (G →* L)
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
i : G →* L
his : i ∈ s
has : i ∉ s
hg : ∑ i ∈ insert i s, g i • ⇑i = 0
h1 : ∀ i_1 ∈ s, g i_1 • ⇑i_1 = g i_1 • ⇑i
hia : ∀ (y : G), i y = i y
⊢ False

Tactic:
contradiction

Goal state after:
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
⊢ LinearIndependent L fun f ↦ ⇑f

Tactic:
by
  let := Classical.decEq (G →* L)
  let : MulAction L L := DistribMulAction.toMulAction
  -- We prove linear independence by showing that only the trivial linear combination vanishes.
  apply linearIndependent_iff'.2
  intro s
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
  intro g hg
  -- Here
  -- * `a` is a new character we will insert into the `Finset` of characters `s`,
  -- * `ih` is the fact that only the trivial linear combination of characters in `s` is zero
  -- * `hg` is the fact that `g` are the coefficients of a linear combination summing to zero
  -- and it remains to prove that `g` vanishes on `insert a s`.
  -- We now make the key calculation:
  -- For any character `i` in the original `Finset`, we have `g i • i = g i • a` as functions
  -- on the monoid `G`.
  have h1 (i) (his : i ∈ s) : (g i • i : G → L) = g i • a := by
    ext x
    rw [← sub_eq_zero]
    apply ih (fun j => g j * j x - g j * a x) _ i his
    ext y
    -- After that, it's just a chase scene.
    calc
      (∑ i ∈ s, (g i * i x - g i * a x) • i : G → L) y =
          (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by simp [sub_mul]
      _ = (∑ i ∈ insert a s, g i * i x * i y) -
            ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
      _ = (∑ i ∈ insert a s, g i * (i x * i y)) -
            ∑ i ∈ insert a s, a x * (g i * i y) := by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]
      _ = (∑ i ∈ insert a s, g i • i : G → L) (x * y) -
            a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by simp [Finset.mul_sum]
      _ = 0 := by rw [hg]; simp
  -- On the other hand, since `a` is not already in `s`, for any character `i ∈ s`
  -- there is some element of the monoid on which it differs from `a`.
  have h2 (i) (his : i ∈ s) : ∃ y, i y ≠ a y := by
    by_contra! hia
    obtain rfl : i = a := MonoidHom.ext hia
    contradiction
  -- From these two facts we deduce that `g` actually vanishes on `s`,
  have h3 (i) (his : i ∈ s) : g i = 0 := by
    let ⟨y, hy⟩ := h2 i his
    have h : g i • i y = g i • a y := congr_fun (h1 i his) y
    rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
    exact h.resolve_right (sub_ne_zero_of_ne hy)
  -- And so, using the fact that the linear combination over `s` and over `insert a s` both
  -- vanish, we deduce that `g a = 0`.
  have h4 : g a = 0 :=
    calc
      g a = g a * 1 := (mul_one _).symm
      _ = (g a • a : G → L) 1 := by rw [← a.map_one]; rfl
      _ = (∑ i ∈ insert a s, g i • i : G → L) 1 := by
        rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
        simp +contextual [h3]
      _ = 0 := by rw [hg]; rfl
  -- Now we're done; the last two facts together imply that `g` vanishes on every element
  -- of `insert a s`.
  exact (Finset.forall_mem_insert ..).2 ⟨h4, h3⟩

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.rank R M ≠ 0
f : R →ₗ[R] M
hf : Injective ⇑f
x y : R
hxy : ∀ (a : M), x • a = y • a
⊢ f x = f y

Tactic:
by simpa [← map_smul] using hxy (f 1)

Goal state after:
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) = ∑ a, if ↑a ∉ t then f ↑a • v ↑a else 0

Tactic:
Finset.sum_coe_sort s fun i => if i ∉ t then f i • v i else 0

Goal state after:
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
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ x ≠ y

Tactic:
rintro rfl; exact (h.symm.subset rfl).2 rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
by
  have := Fintype.ofFinite α
  have := Fintype.ofFinite β
  simp only [Nat.card_eq_fintype_card, Fintype.card_eq]

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

Goal state before:
pp: case mp.right
ι : 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 : z ∈ center A
⊢ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)

Tactic:
intros
      exact ⟨h.2 _ _, h.3 _ _⟩

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

Goal state before:
pp: case inl
α : Type u_1
s : Set α
a : α
hs : s.Finite
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
apply ncard_le_ncard sdiff_subset hs

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (r : R) (x : A × B), ((algebraMap R A).prod (algebraMap R B)) r * x = x * ((algebraMap R A).prod (algebraMap R B)) r

Tactic:
rintro r ⟨a, b⟩
    dsimp
    rw [commutes r a, commutes r b]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Tactic:
have := hs.to_subtype

Goal state after:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
this : Infinite ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
hu : (s ∪ t).Finite
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst

Goal state after:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
ncard_eq_toFinset_card _ hs,

Goal state after:
case inl
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ hs.toFinset.card + 1 = t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
ncard_eq_toFinset_card _ hs,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ hs.toFinset.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
rw [ncard_le_one hs]
  tauto

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
ncard_eq_toFinset_card _ hs,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : s.Finite
⊢ hs.toFinset.card ≤ 1 ↔ ∃ x, s ⊆ {x}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b

Tactic:
ncard_eq_toFinset_card _ hs,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < hs.toFinset.card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
ncard_eq_toFinset_card _ hs,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 2 < hs.toFinset.card ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
ncard_eq_toFinset_card _ hs,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < hs.toFinset.card ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.LinearAlgebra.Quotient.Defs

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
x y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -(x + -y) ∈ p

Tactic:
neg_add,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x y : M
⊢ -x + y ∈ p.toAddSubgroup ↔ -x + - -y ∈ p
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)

Tactic:
simp only [Module.End.iterate_succ]

Goal state after:
case succ
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p.mapQ p ((f ^ k) ∘ₗ f) ⋯ = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b

Tactic:
rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (succ b) = Icc a b

Tactic:
by
  ext x; rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
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₂
x : M × M₂
h : (snd R M M₂) x = 0
⊢ ∃ y, (inl R M M₂) y = x

Tactic:
exact ⟨x.fst, Prod.ext rfl h.symm⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mpr
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₂
x : M × M₂
⊢ (fst R M M₂) x = 0 → ∃ y, (inr R M M₂) y = x

Tactic:
intro h
    exact ⟨x.snd, Prod.ext h.symm rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b

Goal state after: