mathlib-initiative/mathlib-tactics huggingface dataset:
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 (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), f (g x)

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,
    finprod_eq_prod_plift_of_mulSupport_subset, _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)
⊢ mulSupport ((fun x ↦ f (g x)) ∘ PLift.down) ⊆ ↑(Finite.toFinset h)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.IsTorsionFree R M
c : R
f : ι → M
hc : c ≠ 0
⊢ c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i

Tactic:
exact (smulAddHom R M c).map_finsum_of_injective (smul_right_injective M hc) _

Goal state after:
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:
by
  rw [← preimage_natAdd_Ioc_natAdd, image_preimage_eq_of_subset]
  exact Ioc_subset_Ioi_self.trans <| image_natAdd_Ioi m i ▸ image_subset_range _ _

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 : ↑(range ⇑b)
⊢ b.reindexRange x = ↑x

Tactic:
by
  rcases x with ⟨bi, ⟨i, rfl⟩⟩
  exact b.reindexRange_self i

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport fun x ↦ f (g x)).Finite
⊢ (g '' s ∩ mulSupport f).Infinite

Tactic:
image_inter_mulSupport_eq,

Goal state after:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬(s ∩ mulSupport fun x ↦ f (g x)).Finite
⊢ (g '' (s ∩ mulSupport (f ∘ g))).Infinite
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ ¬∏ b ∈ s, f x b ≠ 1

Tactic:
not_not,

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
x : α
hx : ∀ i ∈ s, f x i = 1
⊢ ∏ b ∈ s, f x b = 1
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:
rw [finRotate_apply, Fin.val_add_one i]

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
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ Finite.toFinset hf), f a = f a
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
finprod_mem_finset_product,

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
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ Finite.toFinset hf), f a
⊢ ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ Finite.toFinset hf), f (a, b) = ∏ᶠ (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
⊢ w ⊆ range ⇑b

Tactic:
intro x p

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
⊢ x ∈ range ⇑b
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top
x : ℕ∞
⊢ x ^ ⊤ = if ⊤ < ⊤ then x ^ ⊤.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
| top =>

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

Goal state before:
pp: case top
y : ℕ∞
h : ⊤ ≠ 0
⊢ 0 ^ ⊤ = 0

Tactic:
| top =>

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

Goal state before:
pp: case top
y : ℕ∞
⊢ 1 ^ ⊤ = 1

Tactic:
| top =>

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

Goal state before:
pp: case top
y : ℕ∞
h : ⊤ ≠ 0
⊢ ⊤ ^ ⊤ = ⊤

Tactic:
| top =>

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
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i

Tactic:
convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i

Goal state after:
case e'_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = if i ∈ s then f i else 0

case e'_3
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1.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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s t : Finset ι
f : ι → R
h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
hst : Disjoint s t
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm

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

Goal state before:
pp: case succ.succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n✝¹ : Fin (m + 1) → ℕ
f✝ : (i : Fin (m + 1)) → Fin (n✝¹ i)
n : Fin m → ℕ
f : (i : Fin m) → Fin (n i)
n✝ : ℕ
fn : Fin (n✝ + 1)
⊢ ∏ i, n i + n✝ * ∏ j, n j = (∏ i, n i) * (n✝ + 1)

Tactic:
rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]

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

Goal state before:
pp: a b c : ℕ
hca : c ∣ a
h : ¬c = 0
⊢ a % c + b % c < c

Tactic:
rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
        exact Nat.mod_lt _ (zero_lt_of_ne_zero h)

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) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ↑(finSigmaFinEquiv ⟨⟨iv, hi⟩, j⟩) = ∑ i, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd

Tactic:
finSigmaFinEquiv

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⟩)
⊢ ↑((Trans.trans
          (Trans.trans
            (Trans.trans
              (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm
                (Equiv.sumSigmaDistrib fun a ↦ Fin (n (finSumFinEquiv a))))
              (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i ↦ Fin (n (finSumFinEquiv (Sum.inr i))))))
            finSumFinEquiv)
          (finCongr ⋯))
        ⟨⟨iv, hi⟩, j⟩) =
    ∑ i, n (Fin.castLE ⋯ i) + ↑⟨⟨iv, hi⟩, j⟩.snd
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
⊢ (a + b) / c ≤ a / c + b / c + 1

Tactic:
by_cases h : c = 0

Goal state after:
case pos
a b c : ℕ
h : c = 0
⊢ (a + b) / c ≤ a / c + b / c + 1

case neg
a b c : ℕ
h : ¬c = 0
⊢ (a + b) / c ≤ a / c + b / c + 1
Module: Mathlib.Data.ZMod.Defs

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

Tactic:
Int.emod_eq_zero_of_dvd h,

Goal state after:
case isFalse.isTrue
n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ↑n ∣ x
⊢ 0 = toNat 0
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_3
⊢ 1 < card α ↔ 1 < #α

Tactic:
conv_rhs => rw [← Nat.cast_one]

Goal state after:
α : Type u_3
⊢ 1 < card α ↔ ↑1 < #α
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h✝ : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
s : Set M
hs : LinearIndepOn R id s
h : c' < #↑↑⟨s, hs⟩
t : Set M
hst : t ⊆ ↑⟨s, hs⟩
ht : #↑t = c'
⊢ lift.{w, v} #↑t = lift.{v, w} c

Tactic:
by simp [ht, hcc']

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

Goal state before:
pp: case refine_2
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : R →ₗ[R] M
hf : Injective ⇑f
⊢ ∃ f, Injective ⇑f

Tactic:
· exact ⟨f ∘ₗ _, hf.comp (LinearEquiv.piUnique R ..).injective⟩

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective ⇑j
hc : ∀ (r : R') (m : M), j (i r • m) = r • j m
⊢ ⨆ i, lift.{v', v} #↑↑i ≤ ⨆ i, lift.{v, v'} #↑↑i

Tactic:
exact ciSup_mono_of_forall_exists' bddAbove_of_small fun ⟨s, h⟩ ↦ ⟨⟨j '' s,
    LinearIndepOn.id_image (h.linearIndependent.map_of_injective_injectiveₛ i j hi hj hc)⟩,
    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 0 < s.encard ↔ s.Nonempty

Tactic:
by
  rw [pos_iff_ne_zero, encard_ne_zero]

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

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R ≃+* R'
j : S ≃+* S'
hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)
r : R
x✝ : S
this : (algebraMap R' S') (i r) = j ((algebraMap R S) r)
⊢ ↑j (r • x✝) = i r • ↑j x✝

Tactic:
simp only [smul_def, RingEquiv.coe_toAddEquiv, map_mul, this]

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

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

Tactic:
← zero_add (a := encard s),

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hst : s ⊆ t
hts : t.encard ≤ 0 + s.encard
⊢ s = t
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ LinearIndependent R (-v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, LinearIndependent.neg⟩

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : LinearIndependent R (-v)
⊢ LinearIndependent R v
Module: Mathlib.Data.Set.Card

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

Tactic:
not_not,

Goal state after:
α : Type u_1
s : Set α
⊢ s.encard = 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ x, s = {x}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.encard = 4
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ s.encard = 4

Tactic:
· 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), (by exact rfl : (4 : ℕ∞) = 3 + 1),
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left, encard_eq_three] at h
    obtain ⟨y, z, w, hyz, hyw, hzw, hs⟩ := h
    refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
    · rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr (Or.inr rfl))).2 rfl
    rw [← hs, insert_sdiff_singleton, insert_eq_of_mem hx]

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ s.encard = 4
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ s.encard = 4

Tactic:
rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton] <;> grind

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

Goal state before:
pp: case top
α : Type u_1
s : Set α
a✝ : ∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : ⊤ ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ⊤

Tactic:
| top =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ (f '' s).encard ≤ t.encard

Tactic:
hf.image_subset

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ t.encard ≤ t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : x ∉ {a}
⊢ f₀ x = Function.update f₀ a b x

Tactic:
by rwa [Function.update_of_ne]

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

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

Tactic:
← ncard_sdiff_add_ncard_of_subset hst ht,

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

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

Tactic:
← ncard_union_eq (disjoint_of_subset_left inter_subset_right disjoint_sdiff_right)
    (hs.inter_of_left _) hs.sdiff,

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Finite ↑s
⊢ 1 < s.ncard ↔ s.Nontrivial

Tactic:
← not_subsingleton_iff,

Goal state after:
α : Type u_1
s : Set α
inst✝ : Finite ↑s
⊢ 1 < s.ncard ↔ ¬s.Subsingleton
Module: Mathlib.LinearAlgebra.Quotient.Basic

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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : p ≤ comap (f ^ k) p
⊢ p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k

Tactic:
induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih =>
    simp only [Module.End.iterate_succ]
    rw [mapQ_comp, ih]
    exact p.le_comap_pow_of_le_comap h k

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (a + 1) b) = Icc a b

Tactic:
simpa [succ_eq_add_one] using insert_Icc_succ_left_eq_Icc h

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

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Icc a (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Icc_pred_right_eq_Ico a b

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
inst✝² : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)

Tactic:
by
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: ι : Type v
inst✝³ : Finite ι
R : Type u_1
inst✝² : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
⊢ motive' ((i : ι) → M i)

Tactic:
by
  cases nonempty_fintype ι
  revert M
  refine Fintype.induction_empty_option
    (fun α β _ e h M _ _ hM ↦ equiv' (LinearEquiv.piCongrLeft R M e) <| h _ fun i ↦ hM _)
    (fun M _ _ _ ↦ equiv default unit) (fun α _ h M _ _ hn ↦ ?_) ι
  exact equiv' (LinearEquiv.piOptionEquivProd R).symm <| prod (hn _) (h _ fun i ↦ hn i)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ fst R M M₂ ⊔ snd R M M₂ = ⊤

Tactic:
rw [eq_top_iff]
  rintro ⟨m, n⟩ -
  rw [show (m, n) = (m, 0) + (0, n) by simp]
  apply Submodule.add_mem (Submodule.fst R M M₂ ⊔ Submodule.snd R M M₂)
  · exact Submodule.mem_sup_left (Submodule.mem_comap.mpr (by simp))
  · exact Submodule.mem_sup_right (Submodule.mem_comap.mpr (by simp))

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : ConditionallyCompleteLattice β
inst✝¹ : Finite ι
inst✝ : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
⊢ g (⨆ i, f i) = ⨆ i, g (f i)

Tactic:
obtain ⟨j, hj⟩ : ∃ j, f j = ⨆ i, f i := exists_eq_ciSup_of_finite
  rw [← hj]
  exact le_antisymm (le_ciSup_of_le j le_rfl) <|
    ciSup_le fun i ↦ hg (hs i) (hs j) (hj ▸ le_ciSup f i)

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b : M
⊢ (fun x ↦ a + x) '' Ici b = Ici (a + b)

Tactic:
simp only [add_comm a, image_add_const_Ici]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ IsIdempotentElem (1 - a)

Tactic:
IsIdempotentElem,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ (1 - a) * (1 - a) = 1 - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ IsIdempotentElem (a + b)

Tactic:
IsIdempotentElem,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ (a + b) * (a + b) = a + b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ IsIdempotentElem (b - a)

Tactic:
IsIdempotentElem,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ (b - a) * (b - a) = b - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : IsIdempotentElem (q - p)
h : p * (q - p) + (q - p) * p = 0
⊢ Commute p q

Tactic:
IsIdempotentElem,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
hqp : (q - p) * (q - p) = q - p
h : p * (q - p) + (q - p) * p = 0
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
x : α
inst✝ : LinearOrder α
⊢ span {|x|} = span {x}

Tactic:
by
  obtain h | h := abs_choice x <;>
  simp [h]

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 + y * z) + b * y = x✝¹
a b : α
h : a * (x + y * z) + b * y = x✝¹
⊢ a * x + (b + a * z) * y = x✝¹

Tactic:
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:
rw [← h]; ring1

Goal state after: