mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: α : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ : R →+* R₂
v : α →₀ M
c : R
h : α → M →ₛₗ[σ] M₂
i : α
⊢ (h i) 0 = 0

Tactic:
exact (h i).map_zero

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

Goal state before:
pp: M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ f (∏ i ∈ Finite.toFinset h, g i.down) = ∏ i ∈ ?m.38, f (g i.down)

pp: M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ mulSupport ((fun x ↦ f (g x)) ∘ PLift.down) ⊆ ↑?m.38

pp: M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ Finset (PLift α)

Tactic:
_root_.map_prod

Goal state after:
M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ ∏ x ∈ Finite.toFinset h, f (g x.down) = ∏ i ∈ ?m.38, f (g i.down)

M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ mulSupport ((fun x ↦ f (g x)) ∘ PLift.down) ⊆ ↑?m.38

M : Type u_2
N : Type u_3
α : Sort u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : HasFiniteMulSupport (g ∘ PLift.down)
⊢ Finset (PLift α)
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
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i

Tactic:
have : mulSupport (f ∘ PLift.down) ⊆ s.map Equiv.plift.symm.toEmbedding := by
    rw [A, Finset.coe_map]
    exact image_mono h

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Finset α
h : mulSupport f ⊆ ↑s
A : mulSupport (f ∘ PLift.down) = ⇑Equiv.plift.symm '' mulSupport f
this : mulSupport (f ∘ PLift.down) ⊆ ↑(Finset.map Equiv.plift.symm.toEmbedding s)
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i
Module: Mathlib.Data.Finset.Fin

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

Tactic:
coe_attachFin,

Goal state after:
n : ℕ
s : Finset ℕ
h : ∀ m ∈ s, m < n
⊢ Fin.val '' Fin.val ⁻¹' ↑s = ↑s
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:
rw [← preimage_natAdd_Ioc_natAdd, image_preimage_eq_of_subset]

Goal state after:
n m : ℕ
i j : Fin n
⊢ Ioc (natAdd m i) (natAdd m j) ⊆ range (natAdd m)
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
s : Set α
⊢ linearCombination R (s.domRestrict v) =
    (span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm

Tactic:
by
  ext; simp [linearCombinationOn]

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 : ι
⊢ (b.repr x) i = f x i

Tactic:
by
  let f_i : M →ₗ[R] R :=
    { toFun x := f x i
      map_add' _ _ := by rw [hadd, Pi.add_apply]
      map_smul' _ _ := by simp [hsmul, Pi.smul_apply] }
  have : Finsupp.lapply i ∘ₗ ↑b.repr = f_i := by
    refine b.ext fun j => ?_
    change b.repr (b j) i = f (b j) i
    rw [b.repr_self, f_eq]
  calc
    b.repr x i = f_i x := by
      { rw [← this]
        rfl }
    _ = f x i := rfl

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ b.reindexRange (((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i

Tactic:
reindexRange_apply

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
i : ι
h : b i ∈ Finset.image (⇑b) Finset.univ
⊢ ↑(((Equiv.refl M).subtypeEquiv ⋯).symm ⟨b i, h⟩) = b i
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
inst✝¹ : Fintype ι
inst✝ : DecidableEq M
x : ↥(Finset.image (⇑b) Finset.univ)
⊢ b.reindexFinsetRange x = ↑x

Tactic:
rcases x with ⟨bi, hbi⟩
  rcases Finset.mem_image.mp hbi with ⟨i, -, rfl⟩
  exact b.reindexFinsetRange_self i

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 t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
← finprod_mem_inter_mulSupport f s,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
← finprod_mem_inter_mulSupport f s,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (q * ↑n + ↑r) / ↑n = q ∧ ↑(Fin.ofNat n ((q * ↑n + ↑r).natMod ↑n)) = r

Tactic:
obtain ⟨h1, h2⟩ := Int.natCast_nonneg r, Int.ofNat_lt.2 hrn

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ (q * ↑n + ↑r) / ↑n = q ∧ ↑(Fin.ofNat n ((q * ↑n + ↑r).natMod ↑n)) = r
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

pp: case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
· apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a - b ≤ a ↔ b ≤ a

Tactic:
← not_iff_not,

Goal state after:
n : ℕ
a b : Fin n
⊢ ¬a - b ≤ a ↔ ¬b ≤ a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: N : Type u_6
inst✝ : CommMonoid N
α : Type u_7
ι : Type u_8
f : ι → α → N
hf : HasFiniteMulSupport f
a : α
⊢ (∏ᶠ (i : ι), f i) a = ∏ᶠ (i : ι), f i a

Tactic:
by
  classical
  have hf' : HasFiniteMulSupport fun i ↦ f i a := by fun_prop (disch := simp)
  simp only [finprod_def, dif_pos, hf, hf', Finset.prod_apply]
  symm
  apply Finset.prod_subset <;> aesop

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
f : α × β → M
hf : HasFiniteMulSupport f
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
have h₁ : ∀ a, ∏ᶠ _ : a ∈ hf.toFinset, f a = f a := by simp

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : HasFiniteMulSupport f
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)
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
⊢ range ⇑b = w

Tactic:
by
  -- If `w` is strictly bigger than `range b`,
  apply le_antisymm h
  -- then choose some `x ∈ w \ range b`,
  intro x p
  by_contra q
  -- and write it in terms of the basis.
  have e := b.linearCombination_repr x
  -- This then expresses `x` as a linear combination
  -- of elements of `w` which are in the range of `b`,
  let u : ι ↪ w :=
    ⟨fun i => ⟨b i, h ⟨i, rfl⟩⟩, fun i i' r =>
      b.injective (by simpa only [Subtype.mk_eq_mk] using r)⟩
  simp_rw [Finsupp.linearCombination_apply] at e
  change ((b.repr x).sum fun (i : ι) (a : R) ↦ a • (u i : M)) = ((⟨x, p⟩ : w) : M) at e
  rw [← Finsupp.sum_embDomain (f := u) (g := fun x r ↦ r • (x : M)),
      ← Finsupp.linearCombination_apply] at e
  -- Now we can contradict the linear independence of `hi`
  refine hi.linearCombination_ne_of_notMem_support _ ?_ e
  simp only [Finset.mem_map, Finsupp.support_embDomain]
  rintro ⟨j, -, W⟩
  simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
  apply q ⟨j, W⟩

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inr.inr
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_2 : 1 < x
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
· induction y
    · rw [top_mul z_0, epow_top x_2, top_epow z_0]
    induction z
    · rw [mul_top y_0, epow_top x_2, epow_top]
      apply (epow_right_mono x_2.ne_zero (Order.one_le_iff_ne_zero.2 y_0)).trans_lt'
      simp [x_2]
    · simp only [← Nat.cast_mul, epow_natCast, pow_mul x]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
f : M →ₗ[R] M'
hs : LinearIndepOn R id s
hf_inj : InjOn ⇑f ↑(span R s)
⊢ InjOn ⇑f ↑(span R (id '' s))

Tactic:
simpa using hf_inj

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

Goal state before:
pp: n a b : ℕ
h : n ≤ a
⊢ a - n ≡ b [MOD n] ↔ a ≡ b [MOD n]

Tactic:
rw [← add_modulus_modEq_iff, Nat.sub_add_cancel h]

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

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ (i : ℕ) (h : i < m ^ n), ⟨∑ x, i / m ^ ↑x % m * m ^ ↑x, ⋯⟩ = ⟨i, h⟩
⊢ ⟨∑ i, ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = a

Tactic:
Fin.ext_iff

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m n : ℕ
a : Fin (m ^ (n + 1))
ih : ∀ i < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ⟨∑ i, ↑a / m ^ ↑i % m * m ^ ↑i, ⋯⟩ = a
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
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]

Tactic:
by
      rw [hm, gcd_zero_right] at h; constructor
      · exact h.symm
      · rfl

Goal state after:
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 : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • Fin.cons x v 0 + ∑ i, g i.succ • Fin.cons x v i.succ = 0
⊢ g j = 0

Tactic:
Fin.cons_zero,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), ∑ i, g i • v i = 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R), ∀ y ∈ span R (range v), c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ i, g i.succ • Fin.cons x v i.succ = 0
⊢ g j = 0
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 : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ (i : ℕ) (h : i < ∏ i, xs i), ⟨∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j), ⋯⟩ = ⟨i, h⟩
⊢ ⟨∑ i, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs i * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j), ⋯⟩ = a

Tactic:
Fin.ext_iff

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ⟨∑ i, (↑a / ∏ j, Fin.cons x xs (Fin.castLE ⋯ j)) % Fin.cons x xs i * ∏ j, Fin.cons x xs (Fin.castLE ⋯ j), ⋯⟩ = a
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
⊢ (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      a [MOD n] ∧
    (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      b [MOD m]

Tactic:
rw [xgcd_val]
        dsimp
        rw [modEq_iff_dvd, modEq_iff_dvd,
          Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))]
        have hnonzero : (gcd n m : ℤ) ≠ 0 := by
          norm_cast
          rw [Nat.gcd_eq_zero_iff, not_and]
          exact fun _ => hm
        have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _
        have := gcd_eq_gcd_ab n m
        constructor <;> rw [Int.emod_def, ← sub_add] <;>
            refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _) <;>
          try norm_cast
        · rw [← sub_eq_iff_eq_add'] at this
          rw [← this, Int.sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← Int.mul_sub,
            Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left _ hnonzero,
            Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, Int.dvd_neg, mul_assoc]
          · exact dvd_mul_right _ _
          norm_cast
          exact dvd_mul_right _ _
        · exact dvd_lcm_left n m
        · rw [← sub_eq_iff_eq_add] at this
          rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
            zero_add, mul_assoc]
          · exact dvd_mul_right _ _
          · exact hcoedvd _
        · exact dvd_lcm_right n m

Goal state after:
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 : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % Fin.cons x xs 0 +
      ∑ x_1, (↑a / ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2)) % xs x_1 * ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2) =
    ↑a

Tactic:
Fin.cons_zero,

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x + ∑ x_1, (↑a / ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2)) % xs x_1 * ∏ x_2, Fin.cons x xs (Fin.castLE ⋯ x_2) = ↑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 : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      ∑ x_1,
        ↑a / (Fin.cons x xs 0 * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) % xs x_1 *
          (Fin.cons x xs 0 * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) =
    ↑a

Tactic:
Fin.cons_zero,

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
m : ℕ
n✝ : Fin m → ℕ
n x : ℕ
xs : Fin n → ℕ
a : Fin (∏ i, Fin.cons x xs i)
ih : ∀ i < ∏ i, xs i, ∑ x, (i / ∏ j, xs (Fin.castLE ⋯ j)) % xs x * ∏ j, xs (Fin.castLE ⋯ j) = i
⊢ ↑a % x +
      ∑ x_1,
        ↑a / (x * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) % xs x_1 * (x * ∏ i, Fin.cons x xs (Fin.castLE ⋯ i.succ)) =
    ↑a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case neg
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : ¬iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

Tactic:
· replace him := Nat.eq_of_lt_succ_of_not_lt hi him
    subst him
    conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
    simp
    rfl

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

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝ : Fintype α
⊢ toNat (∏ i, #(β i)) = ∏ a, toNat #(β a)

Tactic:
_root_.map_prod

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

Goal state before:
pp: R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R M₁ ≤ Module.rank R M

Tactic:
rw [← rank_range_of_surjective f h]
  apply rank_range_le

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

Goal state before:
pp: case refine_2
α : Type u_1
a : α
t : Set α
h : a ∉ t
⊢ (insert a t).encard = t.encard + 1

Tactic:
rw [encard_insert_of_notMem h]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x}

Tactic:
by
  rw [le_iff_lt_or_eq, lt_iff_not_ge, Order.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 1 + 1
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}

Tactic:
(ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left,

Goal state after:
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard = 1
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 2 + 1
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
(ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left,

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard = 2
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 3 + 1
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
(ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left,

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard = 3
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
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

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

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
x✝ : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ (↑n₀).toNat ≤ k

Tactic:
ENat.toNat_natCast

Goal state after:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
x✝ : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ n₀ ≤ k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
to_encard_tac

Goal state after:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ ↑s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard + 1 = s.ncard

Tactic:
to_encard_tac

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ ↑(s \ {a}).ncard + 1 = ↑s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).ncard ≤ s.ncard

Tactic:
to_encard_tac

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ ↑(f '' s).ncard ≤ ↑s.ncard
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
hle : s.encard ≤ t.encard
⊢ s.ncard ≤ t.ncard

Tactic:
to_encard_tac

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 t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard

Tactic:
to_encard_tac

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = ↑s.ncard + ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
to_encard_tac

Goal state after:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ ↑(s ∪ t).ncard ≤ ↑s.ncard + ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard = s.ncard + t.ncard

Tactic:
to_encard_tac

Goal state after:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard = ↑s.ncard + ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ (t \ s).ncard + s.ncard = t.ncard

Tactic:
to_encard_tac

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard + ↑s.ncard = ↑t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

Tactic:
to_encard_tac

Goal state after:
case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ ↑s.ncard ≤ ↑(s \ t).ncard + ↑t.ncard
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:
ncard_eq_toFinset_card _ hu,

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : s.Finite
⊢ s.Nontrivial ∧ s.Finite

Tactic:
← Set.finite_coe_iff

Goal state after:
case refine_1
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : Finite ↑s
⊢ s.Nontrivial ∧ s.Finite