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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ (f a + g a) * (∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    f a * ∏ x ∈ s, f x +
      (g a * (∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
          ∏ j ∈ insert a s with a < j, f j +
        ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)

Tactic:
add_mul,

Goal state after:
ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : LinearOrder ι
f g : ι → R
a : ι
s : Finset ι
ha : ∀ x ∈ s, x < a
ihs : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j
ha' : a ∉ s
⊢ f a * (∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) +
      g a * (∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) =
    f a * ∏ x ∈ s, f x +
      (g a * (∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < j, f j) *
          ∏ j ∈ insert a s with a < j, f j +
        ∑ x ∈ s, (g x * ∏ j ∈ insert a s with j < x, (f j + g j)) * ∏ j ∈ insert a s with x < j, f j)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s t : Finset ι
ht : t ∈ s.powerset
⊢ a ^ #t * b ^ (#s - #t) = a ^ #t * b ^ #(s \ t)

Tactic:
← card_sdiff_of_subset (mem_powerset.1 ht)

Goal state after:
ι : Type u_1
R : Type u_4
inst✝ : CommSemiring R
a b : R
s t : Finset ι
ht : t ∈ s.powerset
⊢ a ^ #t * b ^ #(s \ t) = a ^ #t * b ^ #(s \ t)
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_5
R : Type u_7
inst✝¹ : Fintype ι
inst✝ : CommSemiring R
f : ι → R
n : ℕ
⊢ (∑ a, f a) ^ n = ∑ p, ∏ i, f (p i)

Tactic:
by
  simp [sum_pow']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
s : Finset α
f : α → M
g : α → M → N
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
hg : ∀ (a : α), g a 0 = 1
⊢ ∀ x ∈ s, x ∉ (onFinset s f hf).support → g x ((onFinset s f hf) x) = 1

Tactic:
by simp +contextual [*]

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

Goal state before:
pp: case inr.succ
R : Type u_5
S : Type u_6
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : PartialOrder S
abv : AbsoluteValue R S
inst✝¹ : IsDomain S
inst✝ : IsOrderedRing S
h✝ : Nontrivial R
n : ℕ
ih : abv ↑n ≤ ↑n
⊢ abv ↑(n + 1) ≤ ↑(n + 1)

Tactic:
grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih]

Goal state after:
Module: Mathlib.Algebra.BigOperators.GroupWithZero.Action

Goal state before:
pp: N : Type u_2
inst✝³ : CommMonoid N
G : Type u_4
inst✝² : Group G
inst✝¹ : MulDistribMulAction G N
inst✝ : Finite G
b : N
g : G
⊢ g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b

Tactic:
cases nonempty_fintype G
  simp only [finprod_eq_prod_of_fintype, Finset.smul_prod_perm]

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

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ ∑ a ∈ m.toFinset, count a m ≤ m.toFinset.card + 1 ↔ ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2

Tactic:
m.toFinset.card_eq_sum_ones,

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
m : Multiset α
⊢ ∑ a ∈ m.toFinset, count a m ≤ ∑ x ∈ m.toFinset, 1 + 1 ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
⊢ single a 1 ∈ span R ((fun x ↦ single x 1) '' s) ↔ a ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem _ h⟩

Goal state after:
α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : single a 1 ∈ span R ((fun x ↦ single x 1) '' s)
⊢ a ∈ 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 α'
l : α →₀ M
hl : ↑(Finset.image f l.support) ⊆ s
⊢ ↑(mapDomain f l).support ⊆ s

Tactic:
exact Set.Subset.trans mapDomain_support hl

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
⊢ (lmapDomain M R f) ((lmapDomain M R (Function.invFunOn f s)) l) = l

Tactic:
rw [← LinearMap.comp_apply, ← lmapDomain_comp]
    refine (mapDomain_congr fun c hc => ?_).trans mapDomain_id
    exact Function.invFunOn_eq (by simpa using hl hc)

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

Goal state before:
pp: case ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : Basis ι R M
repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g

Tactic:
cases g

Goal state after:
case ofRepr.ofRepr
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
repr✝¹ repr✝ : M ≃ₗ[R] ι →₀ R
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
b : Basis ι R M
R₁ : Type u_13
inst✝² : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), f₁ (b i) = f₂ (b i)
⊢ f₁ = f₂

Tactic:
ext x
  rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
  simp only [map_sum, map_smulₛₗ, h]

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

Tactic:
ext x
  rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
  simp only [map_sum, map_smulₛₗ, h]

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

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

Tactic:
← preimage_addNat_Ioc_addNat,

Goal state after:
n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' (fun x ↦ x.addNat ?m) ⁻¹' Ioc (i.addNat ?m) (j.addNat ?m) = Ioc (i.addNat m) (j.addNat m)

case m
n m : ℕ
i j : Fin n
⊢ ℕ
Module: Mathlib.Order.Interval.Set.Fin

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

Tactic:
by
  rw [← preimage_addNat_Ioo_addNat, image_preimage_eq_of_subset]
  exact Ioo_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

Goal state after:
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
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0

Tactic:
intro x _ h

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
x : α
a✝ : x ∈ s
h : f x • g x ≠ 0
⊢ f x ≠ 0
Module: Mathlib.LinearAlgebra.Basis.Basic

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✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
⊢ span R (⇑(span R (range v)).subtype '' range fun i ↦ ⟨v i, ⋯⟩) = span R (range v)

Tactic:
Submodule.coe_subtype,

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✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
⊢ span R (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = span R (range v)
Module: Mathlib.Data.ENat.Pow

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

Tactic:
zero_epow (mul_ne_zero y_0 z_0)

Goal state after:
case inr.inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
⊢ (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y → x = y

Tactic:
hxy

Goal state after:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
⊢ x = y
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ (m + l) • p + (c + a) = (n + k) • p + d + a

Tactic:
add_comm c,

Goal state after:
case h
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
k l : ℕ
h : k • p + a = l • p + b
m n : ℕ
hadd : m • p + (a + c) = n • p + (b + d)
⊢ (m + l) • p + (a + c) = (n + k) • p + d + a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]

Tactic:
by
  simpa using (modEq_refl a).add_iff_left (d := 0)

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : MulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩
  convert! h.group_smul (fun i ↦ (w i)⁻¹)
  simp [funext_iff]

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

Goal state before:
pp: case inr
a b c : ℕ
hb : c % b < b
⊢ (a ^ (c % b) - 1).gcd (a ^ b - 1) = a ^ b.gcd c - 1

Tactic:
pow_sub_one_gcd_pow_sub_one,

Goal state after:
case inr
a b c : ℕ
hb : c % b < b
⊢ a ^ (c % b).gcd b - 1 = a ^ b.gcd c - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k / n ∣ c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c

Tactic:
rw [Nat.div_dvd_iff_dvd_mul hkn hn] at hnc

Goal state after:
case inr.inr
n m k : ℕ
hkm : m ∣ k
hkn : n ∣ k
c : ℕ
hmc : k ∣ m * c
hnc : k ∣ n * c
hm : m > 0
hn : n > 0
⊢ k / m.gcd n ∣ c
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ (partialProd g k.castSucc.castSucc)⁻¹ * partialProd g k.castSucc.succ = j.contractNth (fun x1 x2 ↦ x1 * x2) g k

pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc < j

pp: case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc.castSucc < j.succ

Tactic:
partialProd_right_inv,

Goal state after:
case inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ g k.castSucc = j.contractNth (fun x1 x2 ↦ x1 * x2) g k

case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc < j

case inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ k.castSucc.castSucc < j.succ
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inr.inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ (partialProd g k.castSucc.castSucc)⁻¹ * partialProd g k.castSucc.succ * g k.succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

pp: case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ k.castSucc

pp: case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ k.castSucc.castSucc < j.succ

Tactic:
partialProd_right_inv,

Goal state after:
case inr.inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ g k.castSucc * g k.succ = j.contractNth (fun x1 x2 ↦ x1 * x2) g k

case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ j ≤ k.castSucc

case inr.inl.h
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k = ↑j
⊢ k.castSucc.castSucc < j.succ
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
l : ι →₀ R
hl : l ∈ Finsupp.supported R R (univ \ {i})
e : (Finsupp.linearCombination R v) l = a • v i
⊢ (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i a)

Tactic:
simp [e]

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

Goal state before:
pp: n a b : ℕ
⊢ a ≡ a + b [MOD n] ↔ n ∣ b

Tactic:
by
  rw [ModEq.comm, add_modEq_left_iff]

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

Goal state before:
pp: case mpr
ι : 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
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
p : Surjective fun i ↦ ⟨v i, ⋯⟩
q : Subtype.val '' (fun i ↦ ⟨v i, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range v = w

Tactic:
image_image

Goal state after:
case mpr
ι : 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
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ⊆ w
p : Surjective fun i ↦ ⟨v i, ⋯⟩
q : (fun x ↦ ↑⟨v x, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range v = w
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m a b : ℕ
h : a ≡ b [MOD m]
⊢ a.gcd m = b.gcd m

Tactic:
by
  have h1 := gcd_dvd_right a m
  have h2 := gcd_dvd_right b m
  exact
    dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1)
      (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)

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

Goal state before:
pp: case succ
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) → ℕ
k : (i : Fin (m + 1)) × Fin (n i)
⊢ ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd

Tactic:
rcases k with ⟨⟨iv, hi⟩, j⟩

Goal state after:
case succ
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⟩)
⊢ ↑(finSigmaFinEquiv ⟨⟨iv, hi⟩, j⟩) = ∑ i, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case isTrue
n : ℕ
inst✝ : NeZero n
x : ℤ
h : 0 ≤ x
⊢ ↑↑x.natAbs = (x % ↑n).toNat

Tactic:
simp [Int.emod_natAbs_of_nonneg h]

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

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

Tactic:
obtain hs | hs := s.finite_or_infinite

Goal state after:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
hs : s.Finite
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

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
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 ι
inst✝ : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ x ∈ t₂, (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x

Tactic:
convert! heq using 2 with i hi i hi <;> simp [hi]

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
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
| s

Tactic:
← s.subtype_map_of_mem (fun x hx => hx),

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✝⁴ : 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
| Finset.map (Embedding.subtype (Membership.mem s)) (Finset.subtype (Membership.mem s) s)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ s.encard = ⊤

Tactic:
rw [encard, ENat.card_eq_top_of_infinite]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ENat.card ↑s = 0 ↔ s = ∅

Tactic:
ENat.card_eq_zero_iff_empty,

Goal state after:
α : Type u_1
s : Set α
⊢ IsEmpty ↑s ↔ s = ∅
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ ∀ (i : { s // LinearIndepOn R id s }), lift.{v, v'} #↑↑i ≤ lift.{v', v} (⨆ ι, #↑↑ι)

Tactic:
rintro ⟨s, li⟩

Goal state after:
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'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} (⨆ ι, #↑↑ι)
Module: Mathlib.LinearAlgebra.Basis.Submodule

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
P : Submodule R M
b : Basis ι R ↥P
x : M
⊢ x ∈ (linearCombination R (⇑P.subtype ∘ ⇑b)).range ↔ ∃ c, x = c.sum fun i x ↦ x • ↑(b i)

Tactic:
simp [@eq_comm _ x, Function.comp, Finsupp.linearCombination_apply]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.encard ≤ t.encard

Tactic:
exact encard_mono hst

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

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

Tactic:
obtain hs | hs := s.finite_or_infinite

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

case inr
α : Type u_1
a : α
s : Set α
hs : s.Infinite
⊢ (insert a s).ncard ≤ s.ncard + 1
Module: Mathlib.Data.Set.Card

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

Tactic:
obtain hs | hs := s.finite_or_infinite

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

case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard ≤ s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
refine ⟨s ∪ s₁, subset_union_left, union_subset hst (hs₁.trans sdiff_subset), ?_⟩

Goal state after:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ (s ∪ s₁).ncard = k
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℕ
a : R
⊢ ↑(n • a) = n • ↑a

Tactic:
mk_nsmul N a n

Goal state after:
R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℕ
a : R
⊢ n • ↑a = n • ↑a
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
⊢ x * y = 1 → x * z = 1 → y = z

Tactic:
hxy

Goal state after:
case hunique
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
⊢ x * z = 1 → y = z
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
⊢ x ∈ comap (single R φ i) (pi I p)

Tactic:
rw [Submodule.mem_comap, Submodule.mem_pi]

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
x : φ i
hx : x ∈ p i
⊢ ∀ i_1 ∈ I, (single R φ i) x i_1 ∈ p i_1
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ⨆ i, map (single R φ i) (p i) = pi Set.univ p

Tactic:
refine iSup_map_single_le.antisymm fun x hx => ?_

Goal state after:
case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type u_1
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x : (i : ι) → φ i
hx : x ∈ pi Set.univ p
⊢ x ∈ ⨆ i, map (single R φ i) (p i)