mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
f : Fin n ≃ ULift.{?u.25, 0} (Fin n) := Equiv.ulift.symm
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
let e : G ≃ ULift (Fin n) := e.trans f

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.25, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.25, 0} (Fin n) := e✝.trans f
⊢ ∃ G' x x_1, Nonempty (G ≃* G')
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: k : ℕ
hk : 0 < k
a b : ℕ
x✝ : 1 ≤ b
⊢ a / k ≤ b ↔ a ≤ k * b + (k - 1)

Tactic:
rw [Nat.div_le_iff_le_mul_add_pred hk]

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ¬IsCofinal s

Tactic:
rw [not_isCofinal_iff]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ∃ x, ∀ y ∈ s, y < x
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
hc' : b ≤ c
⊢ False

Tactic:
exact hb' c (hb.trans hc') hc

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ IsCofinal {t}

Tactic:
rwa [isCofinal_singleton_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
⊢ ℵ₀ ≤ cof α ↔ 1 < cof α

Tactic:
by
  simp [← not_lt]

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = ⨆ a ∈ t, sp a
⊢ s.FG

Tactic:
supr_rw,

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = ⨆ x ∈ ↑t, sp x
⊢ s.FG
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
⊢ DirSupClosedOn D (⋂₀ (Compl.compl '' s))

Tactic:
apply DirSupClosedOn.sInter

Goal state after:
α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
⊢ ∀ x ∈ Compl.compl '' s, DirSupClosedOn D x
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
hd₂

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≤ a
⊢ (b + if h : b ≤ a then Classical.choose ⋯ else 0) = a

Tactic:
dif_pos h

Goal state after:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + Classical.choose ⋯ = a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ (o.brange fun x x_1 ↦ c) = {c}

Tactic:
rw [← range_familyOfBFamily]

Goal state after:
α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ range (o.familyOfBFamily fun x x_1 ↦ c) = {c}
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ∈ range (enumOrd s)

Tactic:
refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩

Goal state after:
case mpr.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ ∀ b < sInf t, enumOrd s b < a

case mpr.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ≤ enumOrd s (sInf t)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case inr
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f < lsub f
⊢ iSup f = lsub f ∨ succ (iSup f) = lsub f

Tactic:
· exact Or.inr ((succ_le_of_lt h).antisymm (lsub_le_succ_iSup f))

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: b c : Ordinal.{u_4}
h : c ≠ 0
⊢ 0 < b / c ↔ c ≤ b

Tactic:
simp [lt_div h]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a / 1 = a

Tactic:
by
  simpa only [one_mul] using mul_div_cancel a one_ne_zero

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
← mul_le_iff_le_div hn',

Goal state after:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑n * ↑(m / n) ≤ ↑m
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
⊢ ∃ o, derivFamily f o = a

Tactic:
rcases le_or_gt a (derivFamily f o) with h | h

Goal state after:
case add_one.inl
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a

case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u}
⊢ ∀ (b : Ordinal.{u}), deriv (fun x ↦ a + x) b = a * ω + b

Tactic:
← funext_iff,

Goal state after:
a : Ordinal.{u}
⊢ (deriv fun x ↦ a + x) = HAdd.hAdd (a * ω)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u}
ha : 0 < a
⊢ ∀ (b : Ordinal.{u}), deriv (fun x ↦ a * x) b = a ^ ω * b

Tactic:
← funext_iff,

Goal state after:
a : Ordinal.{u}
ha : 0 < a
⊢ (deriv fun x ↦ a * x) = HMul.hMul (a ^ ω)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Order.cof α = 1 ↔ typeLT α ∈ range succ

Tactic:
Order.cof_eq_one_iff,

Goal state after:
case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) ↔ typeLT α ∈ range succ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ 1 < o.cof

Tactic:
by
  simp [← not_lt]

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

Goal state before:
pp: a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ a * b

Tactic:
by
  rw [mul_comm]
  exact le_mul_left h

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

Goal state before:
pp: case refine_2.inl
a b : Cardinal.{u_1}
hb : b ≠ 0
ha : ℵ₀ ≤ a
hab : b ≤ a
⊢ a * b = a

Tactic:
rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
by
  rw [max_le_iff]
  refine ⟨fun h => ?_, ?_⟩
  · rcases le_or_gt ℵ₀ a with ha | ha
    · have : a ≠ 0 := by
        rintro rfl
        exact ha.not_gt aleph0_pos
      left
      rw [and_assoc]
      use ha
      constructor
      · rw [← not_lt]
        exact fun hb => ne_of_gt (hb.trans_le (le_mul_left this)) h
      · rintro rfl
        apply this
        rw [mul_zero] at h
        exact h.symm
    right
    by_cases h2a : a = 0
    · exact Or.inr h2a
    have hb : b ≠ 0 := by
      rintro rfl
      apply h2a
      rw [mul_zero] at h
      exact h.symm
    left
    rw [← h, mul_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with (rfl | rfl | ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩)
    · contradiction
    · contradiction
    rw [← Ne] at h2a
    rw [← Cardinal.one_le_iff_ne_zero] at h2a hb
    norm_cast at h2a hb h ⊢
    apply le_antisymm _ hb
    rw [← not_lt]
    apply fun h2b => ne_of_gt _ h
    conv_rhs => left; rw [← mul_one n]
    rw [Nat.mul_lt_mul_left]
    · exact id
    apply Nat.lt_of_succ_le h2a
  · rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
    · rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
    all_goals simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr.inr
a : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) a)
ho₂ : 2 < (fun x ↦ ω ^ x) a
⊢ (fun x ↦ ω ^ x) a ≤ 2 ∨ (fun x ↦ ω ^ x) a ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)

Goal state after:
case refine_1.inr.inr.inl
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) 0)
ho₂ : 2 < (fun x ↦ ω ^ x) 0
⊢ (fun x ↦ ω ^ x) 0 ≤ 2 ∨ (fun x ↦ ω ^ x) 0 ∈ Set.range fun x ↦ ω ^ ω ^ x

case refine_1.inr.inr.inr
b : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b))
ho₂ : 2 < (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b)
⊢ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ≤ 2 ∨ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ∈ Set.range fun x ↦ ω ^ ω ^ x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ ℶ_ ↑n ↔ c ≤ ℶ_ ↑n

Tactic:
simpa using lift_le (b := ℶ_ n)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
i : α
h : (#α).ord = typeLT α
hα : ℵ₀ ≤ #α
⊢ #↑(Iic i) < #α

Tactic:
rw [← Iio_insert, mk_insert self_notMem_Iio]
  exact add_one_lt_of_lt hα (mk_Iio_lt i h)

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

Goal state before:
pp: case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ℵ₀ ≤ a.card

Tactic:
aleph0_le_card

Goal state after:
case add_one.h
a : Ordinal.{u_1}
ha : ω ≤ a
b : Ordinal.{u_1}
IH : (a ^ b).card ≤ max a.card b.card
⊢ ω ≤ a
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case pos
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∀ (j : ι), r j i → f j < f i
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'

Tactic:
refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩

Goal state after:
case pos
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∀ (j : ι), r j i → f j < f i
⊢ f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) ((typein r').toRelEmbedding ⟨i, h⟩) ⋯
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card

Tactic:
aleph0_le_card

Goal state after:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ω ≤ o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
i : α
⊢ #↑(𝒫 {j | r j i}) ≤ #α

Tactic:
mk_powerset

Goal state after:
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
this : {s | Bounded r s} = ⋃ i, 𝒫 {j | r j i}
i : α
⊢ 2 ^ #↑{j | r j i} ≤ #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case add_one
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
⊢ b + 1 < c.ord → derivFamily f (b + 1) < c.ord

Tactic:
| add_one b hb =>

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
w₁ : #ι ≤ #↑(range Φ)
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ

Tactic:
have w₂ : Cardinal.lift.{w'} #(Set.range Φ) ≤ Cardinal.lift.{w} #κ := Cardinal.mk_range_le_lift

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
w₁ : #ι ≤ #↑(range Φ)
w₂ : Cardinal.lift.{w', w} #↑(range Φ) ≤ Cardinal.lift.{w, w'} #κ
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #↑sᶜ = #↑tᶜ

Tactic:
rw [← lift_inj.{u, u}]

Goal state after:
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift.{u, u} #↑sᶜ = lift.{u, u} #↑tᶜ
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ p { toFun := f, support' := Trunc.mk s }

Tactic:
obtain ⟨s, H⟩ := s

Goal state after:
case h
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
f : (i : ι) → β i
s : Multiset ι
H : ∀ (i : ι), i ∈ s ∨ f i = 0
⊢ p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
⊢ (f + g).sigmaCurry = f.sigmaCurry + g.sigmaCurry

Tactic:
ext (i j)
  rfl

Goal state after:
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
⊢ (r • f).sigmaCurry = r • f.sigmaCurry

Tactic:
ext (i j)
  rfl

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
this : (single ⟨i, a⟩ n) ⟨j, b⟩ = 0
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b

Tactic:
simp [split_apply, dif_neg h, this]

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

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
i : ι
h' : x i ≠ 0
u : β₁ i
hu : f i u = x i
⊢ ∃ u, f i u = x i ∧ (x i = 0 → u = 0)

Tactic:
exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk.mk.e_a.refine_1
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ sf.toFinset ⊆ (sf + sg).toFinset

Tactic:
intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inl

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ t = 0

Tactic:
simpa using congr($h 1)

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R✝ : Type u_1
R₂✝ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴⁶ : Semiring R✝
inst✝⁴⁵ : Semiring R₂✝
inst✝⁴⁴ : Semiring S
inst✝⁴³ : Semiring S₂
M✝ : Type u_5
M₂ : Type u_6
N✝ : Type u_7
N₂ : Type u_8
P✝ : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝⁴² : AddCommMonoid M✝
inst✝⁴¹ : AddCommMonoid M₂
inst✝⁴⁰ : AddCommMonoid N✝
inst✝³⁹ : AddCommMonoid N₂
inst✝³⁸ : AddCommMonoid P✝
inst✝³⁷ : AddCommMonoid P₂
inst✝³⁶ : AddCommMonoid Pₗ
inst✝³⁵ : Module R✝ M✝
inst✝³⁴ : Module R✝ M₂
inst✝³³ : Module S N✝
inst✝³² : Module S N₂
inst✝³¹ : Module R₂✝ P✝
inst✝³⁰ : Module S₂ P✝
inst✝²⁹ : Module R✝ P₂
inst✝²⁸ : Module S₂ P₂
inst✝²⁷ : Module R✝ Pₗ
inst✝²⁶ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²⁵ : AddCommGroup M'
inst✝²⁴ : AddCommGroup P'
inst✝²³ : Module R✝ M'
inst✝²² : Module R₂✝ P'
inst✝²¹ : Module S₂ P'
inst✝²⁰ : SMulCommClass S₂ R₂✝ P✝
inst✝¹⁹ : SMulCommClass S R✝ Pₗ
inst✝¹⁸ : SMulCommClass S₂ R₂✝ P'
inst✝¹⁷ : SMulCommClass S₂ R✝ P₂
ρ₁₂ : R✝ →+* R₂✝
σ₁₂✝ : S →+* S₂
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₄ : Type u_17
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
Q : Type u_22
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
inst✝¹³ : Semiring R₄
inst✝¹² : Semiring R₅
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ N
inst✝⁵ : Module R₃ P
inst✝⁴ : Module R₄ Q
inst✝³ : Module R₅ P
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
inst✝ : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
g : Q →ₛₗ[σ₄₂] N
x✝¹ : R
x✝ : M
⊢ (lcompₛₗ R₅ P σ₂₃ g) (h (x✝¹ • x✝)) = σ₁₅ x✝¹ • (lcompₛₗ R₅ P σ₂₃ g) (h x✝)

Tactic:
by
    simp [map_smulₛₗ, lcompₛₗ]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
i : ι
x : N
hx : x ∈ p i
⊢ x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0

Tactic:
hsup

Goal state after:
case mpr
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
i : ι
x : N
hx : x ∈ p i
hsup : x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
⊢ x = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + l₂'.eval = l.eval

Tactic:
← h₂,

Goal state after:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + l₂.eval = l.eval
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ (a • s + c • t) • x + (b • s + d • t) • y = 0

Tactic:
simp only [← hst, smul_add, add_smul,
    smul_assoc, smul_comm a s, smul_comm c t, smul_comm b s, smul_comm d t]

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
h' : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
⊢ s • a • x + t • c • x + (s • b • y + t • d • y) = s • a • x + s • b • y + (t • c • x + t • d • y)