mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
h : i ≠ Fin.last n
⊢ ↑((finRotate (n + 1)) i) = ↑i + 1

Tactic:
by
  rw [finRotate_apply]
  have : (i : ℕ) < n := Fin.val_lt_last h
  exact Fin.val_add_one_of_lt this

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

Goal state before:
pp: n : ℕ
i : Fin n.succ
⊢ ↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1

Tactic:
by
  rw [finRotate_apply, Fin.val_add_one i]

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 : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
⊢ f i = (Finsupp.lapply i) (Finsupp.single i (f i))

Tactic:
{

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
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
⊢ f i = (Finsupp.lapply i) (Finsupp.single i (f i))
Module: Mathlib.Data.ENat.Pow

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

Tactic:
top_epow z_0

Goal state after:
case inr.inr.inr.inr.top
x y z : ℕ∞
z_0 : z ≠ 0
x_2 : 1 < x
y_0 : ⊤ ≠ 0
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
h : a ≡ b [PMOD p]
⊢ b ≡ a [PMOD p]

Tactic:
rw [modEq_iff_nsmul] at *

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n, m • p + b = n • p + a
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
hab : a ≡ b [PMOD p]
hbc : b ≡ c [PMOD p]
⊢ a ≡ c [PMOD p]

Tactic:
rw [modEq_iff_nsmul] at *

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
hab : ∃ m n, m • p + a = n • p + b
hbc : ∃ m n, m • p + b = n • p + c
⊢ ∃ m n, m • p + a = n • p + c
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hab : a ≡ b [PMOD p]
hcd : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p]

Tactic:
rw [modEq_iff_nsmul] at *

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b c d p : M
hab : ∃ m n, m • p + a = n • p + b
hcd : ∃ m n, m • p + c = n • p + d
⊢ ∃ m n, m • p + (a + c) = n • p + (b + d)
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
h : a ≡ b [PMOD p]
⊢ n • a ≡ n • b [PMOD n • p]

Tactic:
rw [modEq_iff_nsmul] at *

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n_1, m • n • p + n • a = n_1 • n • p + n • b
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
h : a ≡ b [PMOD p]
⊢ f a ≡ f b [PMOD f p]

Tactic:
rw [modEq_iff_nsmul] at *

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
h : ∃ m n, m • p + a = n • p + b
⊢ ∃ m n, m • f p + f a = n • f p + f b
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : a ≡ b [PMOD p]
hadd : a + c ≡ b + d [PMOD p]
⊢ c ≡ d [PMOD p]

Tactic:
rw [modEq_iff_nsmul] at *

Goal state after:
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : ∃ m n, m • p + a = n • p + b
hadd : ∃ m n, m • p + (a + c) = n • p + (b + d)
⊢ ∃ m n, m • p + c = n • p + d
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι ≃ ι'
f : ι' → M
s : Set ι
⊢ (fun x ↦ f ↑x) ∘ ⇑(e.image s) = fun x ↦ (f ∘ ⇑e) ↑x

Tactic:
by simp [funext_iff]

Goal state after:
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:
modEq_iff_zsmul

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : ∃ m, m • z • p = b - a
⊢ ∃ m, m • p = b - a
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 p]
⊢ z • a ≡ z • b [PMOD z • p]

Tactic:
modEq_iff_zsmul

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
z : ℤ
h : ∃ m, m • p = b - a
⊢ ∃ m, m • z • p = z • b - z • a
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
i : ι
hv : LinearIndepOn R v s
hi : i ∈ s
a : R
ha : a • v i ∈ span R (v '' (s \ {i}))
⊢ a • v ↑⟨i, hi⟩ ∈ span R ((fun x ↦ v ↑x) '' (univ \ {⟨i, hi⟩}))

Tactic:
simpa [← comp_def, image_comp, image_sdiff Subtype.val_injective]

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 < m ^ n, ∑ x, i / m ^ ↑x % m * m ^ ↑x = i
⊢ ↑a / m ^ 0 % m * m ^ 0 + ∑ x, ↑a / m ^ (↑x + 1) % m * m ^ (↑x + 1) = ↑a

Tactic:
pow_zero,

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
⊢ ↑a / 1 % m * 1 + ∑ x, ↑a / m ^ (↑x + 1) % m * m ^ (↑x + 1) = ↑a
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
⊢ s = t

Tactic:
by
  let f : t ↪ s :=
    ⟨fun x => ⟨x.1, h x.2⟩, fun a b hab => Subtype.coe_injective (Subtype.mk.inj hab)⟩
  have h_surj : Surjective f := by
    apply surjective_of_linearIndependent_of_span hs f _
    convert! hst <;> simp [f, comp_def]
  change s = t
  apply Subset.antisymm _ h
  intro x hx
  rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩
  convert! y.mem
  rw [← Subtype.mk.inj hy]

Goal state after:
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)
⊢ ↑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:
have := gcd_eq_gcd_ab n m

Goal state after:
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)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ m * n ∣ (↑b - ↑a).natAbs

Tactic:
exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2

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⟩
  rw [finSigmaFinEquiv]
  unfold finSumFinEquiv
  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def,
    Equiv.trans_apply, finCongr_apply, Fin.val_cast]
  by_cases him : iv < m
  · conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
    simpa using! ih _
  · 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.Algebra.BigOperators.Fin

Goal state before:
pp: n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ ↑(finSigmaFinEquiv ij) = ↑ij.snd

Tactic:
rw [finSigmaFinEquiv_apply, add_eq_right]
  apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty')

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

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

Tactic:
{

Goal state after:
G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i = ∏ i, (g :: h :: L)[i] ^ (-1) ^ ↑i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

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

Tactic:
Sum.elim_inl

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
⊢ card α = ⊤

Tactic:
by
  simp only [card, toENat_eq_top, aleph0_le_mk]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ card (α × β) = card α * card β

Tactic:
simp [ENat.card]

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
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i • i y - g i • a y = 0
⊢ g i = 0

Tactic:
← smul_sub,

Goal state after:
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
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
y : G
hy : i y ≠ a y
h : g i • (i y - a y) = 0
⊢ g i = 0
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ finrank R M < n

Tactic:
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast] at h
  · exact h.trans natCast_lt_aleph0
  · exact natCast_lt_aleph0

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'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ LinearIndependent (ι := ↑(rangeSplitting ⇑f '' s)) R (⇑f.rangeRestrict ∘ fun x ↦ id ↑x)

Tactic:
convert! li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _) using 1

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard + sᶜ.encard = univ.encard

Tactic:
← encard_union_eq disjoint_compl_right,

Goal state after:
α : Type u_1
s : Set α
⊢ (s ∪ sᶜ).encard = univ.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a (s \ {b})).encard = s.encard

Tactic:
rw [encard_insert_of_notMem, encard_sdiff_singleton_add_one hb]

Goal state after:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ∉ s \ {b}
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
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a : α
ha : a ∈ s.toFinset
⊢ f'' a ha ∈ t.toFinset

Tactic:
{

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
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a : α
ha : a ∈ s.toFinset
⊢ f'' a ha ∈ t.toFinset
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
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ s.toFinset.card ≤ t.toFinset.card

Tactic:
{

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
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ s.toFinset.card ≤ t.toFinset.card
Module: Mathlib.Data.Set.Card

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

Tactic:
have hsf := finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm

Goal state after:
α : Type u_1
s : Set α
hs : 1 < s.ncard
a : α
hsf : s.Finite
⊢ ∃ b ∈ s, b ≠ a
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
x : M ⧸ p'
⊢ (factor H) (Quotient.mk (Quotient.out x)) = x

Tactic:
exact Quotient.out_eq x

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₄
⊢ (f.prodMap g).range = f.range.prod g.range

Tactic:
by
  ext ⟨_, _⟩; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι✝ : Type x
ι' : Type x'
inst✝⁸ : Semiring R
φ : ι✝ → Type u_1
ψ : ι✝ → Type u_2
χ : ι✝ → Type u_3
inst✝⁷ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁶ : (i : ι✝) → Module R (φ i)
inst✝⁵ : (i : ι✝) → AddCommMonoid (ψ i)
inst✝⁴ : (i : ι✝) → Module R (ψ i)
inst✝³ : (i : ι✝) → AddCommMonoid (χ i)
inst✝² : (i : ι✝) → Module R (χ i)
ι : Type u_4
M : Option ι → Type u_5
inst✝¹ : (i : Option ι) → AddCommMonoid (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ ∀ (x y : (i : Option ι) → M i),
    Equiv.piOptionEquivProd.toFun (x + y) = Equiv.piOptionEquivProd.toFun x + Equiv.piOptionEquivProd.toFun y

Tactic:
by simp [funext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι✝ : Type x
ι' : Type x'
inst✝⁸ : Semiring R
φ : ι✝ → Type u_1
ψ : ι✝ → Type u_2
χ : ι✝ → Type u_3
inst✝⁷ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁶ : (i : ι✝) → Module R (φ i)
inst✝⁵ : (i : ι✝) → AddCommMonoid (ψ i)
inst✝⁴ : (i : ι✝) → Module R (ψ i)
inst✝³ : (i : ι✝) → AddCommMonoid (χ i)
inst✝² : (i : ι✝) → Module R (χ i)
ι : Type u_4
M : Option ι → Type u_5
inst✝¹ : (i : Option ι) → AddCommMonoid (M i)
inst✝ : (i : Option ι) → Module R (M i)
⊢ ∀ (m : R) (x : (i : Option ι) → M i),
    Equiv.piOptionEquivProd.toFun (m • x) = (RingHom.id R) m • Equiv.piOptionEquivProd.toFun x

Tactic:
by simp [funext_iff]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case succ.hin.refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≠ succ^[n.succ] i

Tactic:
rw [hn_eq]
        exact hn_lt_ne _ (Nat.lt_succ_self n)

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
⊢ ∀ a ∈ Iio i, ((Iic a).sup fun x ↦ disjointed f x) = (partialSups f) a

Tactic:
· simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
      refine fun x hx ↦ ih x ?_
      -- Remains to show `∀ x in Iio i, #(Iio x) ≤ r`.
      rw [← Nat.lt_add_one_iff, ← hn]
      apply lt_of_lt_of_le (b := #(Iic x))
      · simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _
      · refine card_le_card (fun r hr ↦ ?_)
        simp only [mem_Iic, mem_Iio] at hx hr ⊢
        exact hr.trans_lt hx

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

Goal state before:
pp: A✝ : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid A
inst✝³ : PartialOrder A
inst✝² : CanonicallyOrderedMul A
inst✝¹ : LocallyFiniteOrderBot A
inst✝ : DecidableEq A
n : A
a : A × A
⊢ a ∈ {uv ∈ Iic n ×ˢ Iic n | uv.1 * uv.2 = n} ↔ a.1 * a.2 = n

Tactic:
by
    simp only [mem_filter, and_iff_right_iff_imp]
    intro h
    simp [← h]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
⊢ y * x ∈ I ↔ x ∈ I

Tactic:
by
  refine ⟨fun h => ?_, fun h => I.mul_mem_left y h⟩
  obtain ⟨y', hy'⟩ := hy.exists_left_inv
  have := I.mul_mem_left y' h
  rwa [← mul_assoc, hy', one_mul] at this

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a

Tactic:
conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ x ^ n.succ * y ^ (n.succ - n.succ) * ↑0 = x ^ n.succ * y * y ^ (n - n.succ) * ↑0

Tactic:
cast_zero,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
⊢ x ^ n.succ * y ^ (n.succ - n.succ) * 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ (x + y) ^ 0 = ∑ m ∈ range (0 + 1), t 0 m

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = ∑ m ∈ range (0 + 1), t 0 m
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = x ^ 0 * y ^ (0 - 0) * ↑(Nat.choose 0 0)

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * y ^ (0 - 0) * ↑(Nat.choose 0 0)
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * y ^ (0 - 0) * ↑(Nat.choose 0 0)

Tactic:
pow_zero,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * 1 * ↑(Nat.choose 0 0)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * (x + y * z) + b * y = x✝¹
a b : α
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹

Tactic:
by rw [← h]; ring1

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y * z) + (b - a * z) * y = x✝¹

Tactic:
by rw [← h]; ring1

Goal state after: