mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

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

Tactic:
convert bind_powerset_len x

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun k ↦ powersetCard k x) = (range (x.card + 1)).bind fun k ↦ powersetCard k x
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 α'
l : α →₀ M
hl : ↑l.support ⊆ f ⁻¹' s
⊢ ↑(mapDomain f l).support ⊆ s

Tactic:
← Set.image_subset_iff,

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 α'
l : α →₀ M
hl : f '' ↑l.support ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s
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 α'
⊢ supported M R (f ⁻¹' s) ≤ comap (lmapDomain M R f) (supported M R s)

Tactic:
intro l (hl : (l.support : Set α) ⊆ f ⁻¹' s)
  change ↑(mapDomain f l).support ⊆ s
  rw [← Set.image_subset_iff, ← Finset.coe_image] at hl
  exact Set.Subset.trans mapDomain_support hl

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Ici ↑i ∩ Iio n = Ico (↑i) n

Tactic:
Ici_inter_Iio

Goal state after:
n : ℕ
i : Fin n
⊢ Ico (↑i) n = Ico (↑i) n
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ natAdd m '' Ioc i j = Ioc (natAdd m i) (natAdd m j)

Tactic:
← preimage_natAdd_Ioc_natAdd,

Goal state after:
n m : ℕ
i j : Fin n
⊢ natAdd m '' natAdd ?m ⁻¹' Ioc (natAdd ?m i) (natAdd ?m j) = Ioc (natAdd m i) (natAdd m j)

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (a : α), (s ∩ mulSupport f).mulIndicator f a = ∏ᶠ (a : α), s.mulIndicator f a

Tactic:
mulIndicator_inter_mulSupport

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (a : α), s.mulIndicator f a = ∏ᶠ (a : α), s.mulIndicator f a
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' uIoo (i.addNat m) (j.addNat m) = uIoo i j

Tactic:
by
  simp [uIoo, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' uIoo i j = uIoo (i.addNat m) (j.addNat m)

Tactic:
by
  simp [uIoo, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

Goal state after:
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
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f (b i) = ⇑(single i 1)
x : M
i : ι
x✝¹ : R
x✝ : M
⊢ f (x✝¹ • x✝) i = (RingHom.id R) x✝¹ • f x✝ i

Tactic:
by simp [hsmul, Pi.smul_apply]

Goal state after:
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
x : M
i : ι
a✝ : Nontrivial R
c : R
⊢ ∀ (x : M), (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩

Tactic:
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
x✝ : M
i : ι
a✝ : Nontrivial R
c : R
x : M
⊢ (fun i ↦ (b.reindexRange.repr (c • x)) ⟨b i, ⋯⟩) = c • fun i ↦ (b.reindexRange.repr x) ⟨b i, ⋯⟩
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
rcases i.lt_or_ge n with hi | hi
  · simp_rw [finSumNatEquiv_symm_apply_of_lt hi, hi, Sum.isLeft_inl, decide_true]
  · simp_rw [finSumNatEquiv_symm_apply_of_ge hi, hi.not_gt, Sum.isLeft_inr, decide_false]

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

Goal state before:
pp: m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ finAddFlip ⟨k, h₂⟩ = ⟨k - m, ⋯⟩

Tactic:
convert! @finAddFlip_apply_natAdd n ⟨k - m, by lia⟩ m
  simp [Nat.add_sub_cancel' h₁]

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

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ a / ↑n * ↑n + ↑↑(Fin.ofNat n (a.natMod ↑n)) = a

Tactic:
Fin.val_ofNat,

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ a / ↑n * ↑n + ↑(a.natMod ↑n % n) = a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b ↦ ∏ a ∈ s with g a = b, f a
this : {a ∈ s | g a = b}.Nonempty
⊢ b ∈ g '' ↑s

Tactic:
simpa only [fiber_nonempty_iff_mem_image, Finset.mem_image, exists_prop]

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 : ((b.repr x).sum fun i a ↦ a • ↑(u i)) = ↑⟨x, p⟩
⊢ False

Tactic:
rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
      ← Finsupp.linearCombination_apply] at e

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⟩
⊢ False
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
f : ι → M
⊢ LinearIndependent R f ↔ IsEmpty ι

Tactic:
by
  rw [Subsingleton.elim f 0, linearIndependent_zero_iff]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
⊢ LinearIndependent R fun (x : ↑s) ↦ v ↑x

Tactic:
linearIndependent_iff_finset_linearIndependent

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
⊢ ∀ (s_1 : Finset ↑s), LinearIndependent R ((fun x ↦ v ↑x) ∘ Subtype.val)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : a ≡ b [PMOD z • p]
⊢ a ≡ b [PMOD p]

Tactic:
rw [modEq_iff_zsmul] at *
  rcases h with ⟨m, h⟩
  simp [← h, ← mul_zsmul]

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

Goal state before:
pp: n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : (f 0 • partialProd fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ (f 0 • partialProd fun i ↦ (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ

Tactic:
simp only [Pi.smul_apply, smul_eq_mul] at hx ⊢
    rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n a b : ℕ
cop : m.Coprime n
ha : a ≠ 0
hb : b ≠ 0
⊢ a * m + b * n ≠ m * n

Tactic:
intro h
  obtain ⟨x, rfl⟩ : n ∣ a :=
    cop.symm.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
  obtain ⟨y, rfl⟩ : m ∣ b :=
    cop.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
  rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
  refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)
  rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]

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
inst✝ : Nontrivial R
hv : LinearIndependent R v
x : ι
f : ι →₀ R
h : x ∉ f.support
⊢ (Finsupp.linearCombination R v) f ≠ v x

Tactic:
by
  replace h : x ∉ (f.support : Set ι) := h
  intro w
  have p : ∀ x ∈ Finsupp.supported R R f.support,
    Finsupp.linearCombination R v x ≠ f.linearCombination R v := by
    simpa [← w, Finsupp.span_image_eq_map_linearCombination] using hv.notMem_span_image h
  exact p f (f.mem_supported_support R) rfl

Goal state after:
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
hv : LinearIndependent R v
i : ι
a : R
ha : a • v i ∈ span R (v '' (univ \ {i}))
⊢ a = 0

Tactic:
by
  rw [Finsupp.span_image_eq_map_linearCombination, mem_map] at ha
  rcases ha with ⟨l, hl, e⟩
  rw [linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])] at hl
  by_contra hn
  exact (notMem_of_mem_sdiff (hl <| by simp [hn])) (mem_singleton _)

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

Goal state before:
pp: case e'_1
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ m = c * (m / c)

Tactic:
rwa [Nat.mul_div_cancel']

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

Goal state before:
pp: case e'_2
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a = c * (a / c)

Tactic:
rwa [Nat.mul_div_cancel']

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

Goal state before:
pp: case e'_3
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ b = c * (b / c)

Tactic:
rwa [Nat.mul_div_cancel']

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

Goal state before:
pp: case refine_2.specialize_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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (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
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})

Tactic:
simp_rw [Finset.disjoint_left, Finset.mem_filter]

Goal state after:
case refine_2.specialize_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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (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
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∀ ⦃a : ι⦄, a ∈ s ∧ g a ≤ f a → ¬(a ∈ s ∧ f a < g a)
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
dsimp only [Fin.val_mk]

Goal state after:
ι : Type u_1
M : Type u_2
m : ℕ
n : Fin m → ℕ
⊢ ∀ (a : Fin (∏ i, n i)), ⟨∑ i, (↑a / ∏ j, n (Fin.castLE ⋯ j)) % n i * ∏ j, n (Fin.castLE ⋯ j), ⋯⟩ = a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n : ℕ
⊢ ∀ (x₀ : ℕ) (x : Fin n → ℕ),
    (∀ (a : Fin (∏ i, x i)), ⟨∑ i, (↑a / ∏ j, x (Fin.castLE ⋯ j)) % x i * ∏ j, x (Fin.castLE ⋯ j), ⋯⟩ = a) →
      ∀ (a : Fin (∏ i, Fin.cons x₀ x i)),
        ⟨∑ i, (↑a / ∏ j, Fin.cons x₀ x (Fin.castLE ⋯ j)) % Fin.cons x₀ x i * ∏ j, Fin.cons x₀ x (Fin.castLE ⋯ j), ⋯⟩ = a

Tactic:
x

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
⊢ ∀ (x_1 : Fin n → ℕ),
    (∀ (a : Fin (∏ i, x_1 i)), ⟨∑ i, (↑a / ∏ j, x_1 (Fin.castLE ⋯ j)) % x_1 i * ∏ j, x_1 (Fin.castLE ⋯ j), ⋯⟩ = a) →
      ∀ (a : Fin (∏ i, Fin.cons x x_1 i)),
        ⟨∑ i, (↑a / ∏ j, Fin.cons x x_1 (Fin.castLE ⋯ j)) % Fin.cons x x_1 i * ∏ j, Fin.cons x x_1 (Fin.castLE ⋯ j),
            ⋯⟩ =
          a
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.Coprime n

Tactic:
rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]

Goal state after:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 1 ≡ 0 [MOD a.gcd n]
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ ∑ i, n (Fin.castLE ⋯ i) = 0

Tactic:
apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty')

Goal state after:
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: n : ℕ
a b c : Fin n
⊢ c * a + c * b = a * c + b * c

Tactic:
mul_comm _ b,

Goal state after:
n : ℕ
a b c : Fin n
⊢ c * a + b * c = a * c + b * c
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
rw [Fin.prod_univ_succ]

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
g : G
⊢ g = [g][0] ^ (-1) ^ ↑0 * ∏ i, [g][i.succ] ^ (-1) ^ ↑i.succ
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
    rw [Fin.prod_univ_succ]; simp

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

Goal state before:
pp: case zero
⊢ Nat.card (ZMod 0) = 0

Tactic:
exact @Nat.card_eq_zero_of_infinite _ Int.infinite

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

Goal state before:
pp: α : Type u_1
e : α
⊢ {e}.encard = 1

Tactic:
rw [encard, ENat.card_eq_coe_fintype_card, card_singleton, Nat.cast_eq_one]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdB 0 s = 1

Tactic:
unfold gcdB

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : 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 ⊆ s, ∀ (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i → ∀ i ∈ s, f i = 0
t : Finset ↑↑s
f : ↑↑s → R
heq : ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i
i : ↑↑s
⊢ ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t, (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i =
    ∑ i ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) (Finset.univ \ t), (if h : i ∈ s then f ⟨i, h⟩ else 0) • v i

Tactic:
simpa [Embedding.subtype, ← Finset.compl_eq_univ_sdiff]

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

Goal state before:
pp: case a
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:
· exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, y, hne, hs⟩ ↦ by rw [hs, encard_pair hne]⟩
  obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
  rw [← insert_eq_of_mem hx, ← insert_sdiff_singleton, encard_insert_of_notMem (fun h ↦ h.2 rfl),
    ← one_add_one_eq_two, (ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left,
    encard_eq_one] at h
  obtain ⟨y, h⟩ := h
  refine ⟨x, y, by rintro rfl; exact (h.symm.subset rfl).2 rfl, ?_⟩
  rw [← h, insert_sdiff_singleton, insert_eq_of_mem hx]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = 0 ∧ f ≠ 0

Tactic:
simp [linearIndepOn_iff]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
⊢ (x : M) → x ∈ ⊥ → (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → P N

Tactic:
x

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
⊢ x ∈ ⊥ → (∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) → P N
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
⊢ (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'

Tactic:
x

Goal state after:
case succ
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this : DecidableEq M
Pbot : P ⊥
n : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
⊢ x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ ↑1

Tactic:
Nat.cast_one

Goal state after:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
⊢ s.ncard ≤ t.ncard

Tactic:
have hle := encard_le_encard_of_injOn hf f_inj

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ s.ncard ≤ t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
hs : s.Finite
⊢ n ≤ s.ncard

Tactic:
rw [ncard_eq_toFinset_card _ hs]
  apply Finset.le_card_of_inj_on_range <;> simpa

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

Goal state before:
pp: α : 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 ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
intro b hb

Goal state after:
α : 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
⊢ ∃ a, ∃ (ha : a ∈ s), b = f a ha
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ = f a ↔ x✝ ∈ a • ↑f.ker

Tactic:
mem_smul_set_iff_inv_smul_mem,

Goal state after:
α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ = f a ↔ a⁻¹ • x✝ ∈ ↑f.ker
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : Finite ↑s
f : α → β
⊢ s.ncard ≤ (f '' s).ncard + 1 ↔
    ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, ∀ d ∈ s, f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
simpa [Subtype.ext_iff, ← (Set.image_injective.mpr Subtype.val_injective).eq_iff,
     Set.image_insert_eq, Set.image_singleton] using
      (Set.surjective_mapsTo_image_restrict f s).card_le_card_add_one_iff

Goal state after:
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
⊢ Function.Surjective ⇑p.mkQ

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Add R'
inst✝¹ : Mul R'
c✝ d : RingCon R
inst✝ : Subsingleton R
c c' : RingCon R
r r' : R
⊢ c r r' ↔ c' r r'

Tactic:
Subsingleton.elim r' r,

Goal state after:
α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Add R'
inst✝¹ : Mul R'
c✝ d : RingCon R
inst✝ : Subsingleton R
c c' : RingCon R
r r' : R
⊢ c r r ↔ c' r r
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * (x * z) = x * y * z

Tactic:
by rw [← mul_assoc, hf.mul_comm y x]

Goal state after:
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
⊢ ⨅ i ∈ J, (proj i).ker ≤ ⨆ i ∈ ↑I, (single R φ i).range

Tactic:
intro b hb

Goal state after:
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 : b ∈ ⨅ i ∈ J, (proj i).ker
⊢ b ∈ ⨆ i ∈ ↑I, (single R φ i).range