mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : n + 1 ≤ c
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) =
    a ^ (n + 1) * a ^ (c - (n + 1)) * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) + 0

Tactic:
rw [← pow_add, add_zero, add_tsub_cancel_of_le h]

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

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c < n + 1
⊢ ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = 0 * a ^ (n + 1) + z

Tactic:
simp_rw [zero_mul, zero_add]

Goal state after:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c < n + 1
⊢ ∃ z ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset,
    a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) = z
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝ : CommSemiring R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Tactic:
cases subsingleton_or_nontrivial R

Goal state after:
case inl
R : Type u_5
inst✝ : CommSemiring R
h✝ : Subsingleton R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f g : Filter α
⊢ ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f

Tactic:
simp_rw [le_def, not_forall, exists_prop]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: α : Type u_3
inst✝ : LinearOrder α
s : Set α
hs : ¬BddAbove s
⊢ atTop = generate (Ici '' s)

Tactic:
by
  refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_
  obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x
  exact ⟨y, hy, hy'.le⟩

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
⊢ f b ≤ c

Tactic:
obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : Preorder γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
g : α → β
hg : Tendsto g l atTop
c : γ
hc : c ∈ upperBounds (range (f ∘ g))
b : β
a : α
ha : b ≤ g a
⊢ f b ≤ c
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
by
  rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] at h
  exact le_of_smul_le_smul_of_pos_left h <| neg_pos.2 ha

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)

Tactic:
refine fun ab nab ↦ hab.not_gt ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
hab : 0 ≤ a • b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a • b < 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
⊢ iSup f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
refine
    ⟨fun h i => ?_, fun h =>
      le_antisymm (Ordinal.iSup_le fun i => nonpos_iff_eq_zero.2 (h i)) zero_le⟩
  rw [← nonpos_iff_eq_zero, ← h]
  exact Ordinal.le_iSup f i

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ #↑(range f) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι

Tactic:
← Cardinal.lift_id'.{u, max u v + 1} #(range _)

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ Cardinal.lift.{u, max u ((max u v) + 1)} #↑(range f) ≤ Cardinal.lift.{max v (u + 1) (v + 1), u} #ι
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ enumOrd s o ∈ s ∩ {b | ∀ c < o, enumOrd s c < b}

Tactic:
rw [enumOrd]
  exact csInf_mem (enumOrd_nonempty hs o)

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

Goal state before:
pp: s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
⊢ enumOrd t ≤ enumOrd s

Tactic:
intro a
  rw [enumOrd, enumOrd]
  gcongr with b c
  exacts [enumOrd_nonempty hs a, enumOrd_le_of_subset hs hst c]

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

Goal state before:
pp: case a
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * d)

Tactic:
· grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / 0 = c ↔ 0 * c ≤ a ∧ a < 0 * (c + 1)

Tactic:
simp [hc.symm]

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

Goal state before:
pp: case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ log 0 n = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

Tactic:
simp only [log_zero_left, log_one_left]

Goal state after:
case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ 0 = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Tactic:
simp only [log_zero_left, log_one_left]

Goal state after:
case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ 0 = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b

pp: case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
· rw [lt_one_iff] at a0
      rw [a0, zero_opow one_ne_zero]
      exact zero_le

Goal state after:
case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccLimit c.ord

Tactic:
by
  constructor
  · simpa using (aleph0_pos.trans_le hc).ne'
  · simp_rw [isSuccPrelimit_iff_succ_lt, succ_eq_add_one, lt_ord, card_add_one]
    refine fun a ha ↦ ?_
    contrapose! ha
    rwa [add_one_of_aleph0_le] at ha
    rw [← ord_le, ← IsSuccLimit.le_succ_iff, succ_eq_add_one, ord_le, card_add_one]
    · exact hc.trans ha
    · simp

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

Goal state before:
pp: case hx
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0

Tactic:
· exact fun h ↦ mul_ne_zero (opow_ne_zero u (bot_lt_of_lt hb).ne') hv <|
      left_eq_zero_of_add_eq_zero h

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

Goal state before:
pp: case h
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a < ω ^ log ω a * (a / ω ^ log ω a + 1)

Tactic:
exact lt_mul_succ_div a (opow_ne_zero _ omega0_ne_zero)

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

Goal state before:
pp: n : ℕ
⊢ (↑n).IsInitial

Tactic:
rw [IsInitial, card_nat, ord_natCast]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o ↔ ∀ a < o, a + o = o

Tactic:
refine ⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩

Goal state after:
case refine_1
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
⊢ a + o = o

case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
⊢ a + o = o

Tactic:
rcases lt_or_ge 1 o with ho₁ | ho₁
    · exact op_eq_self_of_isPrincipal hao (isNormal_add_right a) ho
        (isSuccLimit_of_isPrincipal_add ho₁ ho)
    · cases le_one_iff.1 ho₁ <;> simp_all

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ < ℵ_ o ↔ 0 < o

Tactic:
← aleph_zero,

Goal state after:
o : Ordinal.{u_1}
⊢ ℵ_ 0 < ℵ_ o ↔ 0 < o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ < ℵ_ o ↔ 0 < o

Tactic:
rw [← aleph_zero, aleph_lt_aleph]

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

Goal state before:
pp: ⊢ succ ℵ₀ = ℵ_ 1

Tactic:
← aleph_zero,

Goal state after:
⊢ succ (ℵ_ 0) = ℵ_ 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
⊢ max a b = a

Tactic:
max_eq_left hb

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
⊢ a = a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ max a b = a

Tactic:
max_eq_left hb

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a = a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ lift.{u, v} (⨆ i, f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)

Tactic:
rw [lift_iSup bddAbove_of_small] at h

Goal state after:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ ⨆ i, lift.{u, v} (f i)
⊢ sum f = lift.{u, v} (⨆ i, f i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
apply lt_of_le_of_lt

Goal state after:
case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₁ + μ₁ ≤ ?inr.b

case inr.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ ?inr.b < κ₂ + μ₂

case inr.b
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ Cardinal.{u_1}
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ℵ₀ < ℵ_ o

Tactic:
← aleph_zero,

Goal state after:
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ℵ_ 0 < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{max v u, u} #ι ^ lift.{max u v, u} #ι = lift.{v, u} (2 ^ #ι)

Tactic:
← lift_power,

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{max u v, u} (#ι ^ #ι) = lift.{v, u} (2 ^ #ι)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: case refine_2
β α : Type u
s : Set β
f : ↑s → α
θ : Cardinal.{u}
hθ : θ ≤ #↑s
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
a : α
ha : θ ≤ #↑(f ⁻¹' {a})
⊢ θ ≤ #↑{x | ∃ (h : x ∈ s), f ⟨x, h⟩ = a}

Tactic:
refine
      ha.trans
        (ge_of_eq <|
          Quotient.sound ⟨Equiv.trans ?_ (Equiv.subtypeSubtypeEquivSubtypeExists _ _).symm⟩)
    simp only [coe_eq_subtype, mem_singleton_iff, mem_preimage, mem_ofPred_eq]
    rfl

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

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s // Bounded r s } = #α

Tactic:
by
  rcases eq_or_ne #α 0 with (ha | ha)
  · rw [ha]
    have := mk_eq_zero_iff.1 ha
    rw [mk_eq_zero_iff]
    constructor
    rintro ⟨s, hs⟩
    exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)
  have h' : IsStrongLimit #α := ⟨ha, @h⟩
  have ha := h'.aleph0_le
  apply le_antisymm
  · have : { s : Set α | Bounded r s } = ⋃ i, 𝒫 { j | r j i } := ofPred_exists _
    rw [← coe_ofPred, this]
    refine mk_iUnion_le_sum_mk.trans ((sum_le_mk_mul_iSup (fun i => #(𝒫 { j | r j i }))).trans
      ((mul_le_max_of_aleph0_le_left ha).trans ?_))
    rw [max_eq_left]
    apply ciSup_le' _
    intro i
    rw [mk_powerset]
    exact (h (card_typein_lt _ hr)).le
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · apply bounded_singleton
      rw [← hr]
      apply isSuccLimit_ord ha
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

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

Goal state before:
pp: α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c

Tactic:
biUnion_eq_iUnion

Goal state after:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ x, t ↑x ⋯) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ω_ Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
by
  simpa using IsInaccessible.univ.omega_ord

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #↑s = lift.{u, v} #↑t
⊢ lift.{v, u} #↑sᶜ = lift.{u, v} #↑tᶜ

Tactic:
by
  cases nonempty_fintype α
  rcases lift_mk_eq'.1 h1 with ⟨e⟩; let : Fintype β := Fintype.ofEquiv α e
  replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm
  classical
    lift s to Finset α using s.toFinite
    lift t to Finset β using t.toFinite
    simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
    simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
      lift_natCast, h1, h2]

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
i : ι
⊢ i ∈ sg → i ∈ sf ∨ i ∈ sg

Tactic:
exact Or.inr

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

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
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ a ∈ s, t a)

Tactic:
biUnion_eq_iUnion

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
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ LinearIndepOn R v (⋃ x, t ↑x)
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
⊢ LinearIndependent R ![x, -y] ↔ LinearIndependent R ![x, y]

Tactic:
pair_symm_iff,

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![-y, x] ↔ LinearIndependent R ![x, y]
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
⊢ Injective fun ψ ↦ f.compAddChar ψ

Tactic:
rintro ψ χ h

Goal state after:
B : Type u_2
M : Type u_3
N : Type u_4
inst✝² : AddMonoid B
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
hf : Injective ⇑f
ψ χ : AddChar B M
h : (fun ψ ↦ f.compAddChar ψ) ψ = (fun ψ ↦ f.compAddChar ψ) χ
⊢ ψ = χ
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
⊢ Injective fun ψ ↦ ψ.compAddMonoidHom f

Tactic:
rintro ψ χ h

Goal state after:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : (fun ψ ↦ ψ.compAddMonoidHom f) ψ = (fun ψ ↦ ψ.compAddMonoidHom f) χ
⊢ ψ = χ
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ ((r + s) * x✝)

Tactic:
right_distrib,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ (r * x✝ + s * x✝)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [← linearIndependent_equiv (finSuccEquiv n).symm, linearIndependent_option]
  rfl

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
⊢ m ∈ AddSubmonoid.closure s

Tactic:
by
  suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' s) by
    simpa [← AddSubmonoid.toSubmonoid_closure]
  let s' := @Submonoid.closure (Multiplicative M) Multiplicative.mulOneClass s
  have h' : Submonoid.map (of R M) s' = Submonoid.closure (of R M '' s) :=
    MonoidHom.map_mclosure _ _
  rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h
  simpa using! of'_mem_span.1 h

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
r₁ r₂ : R
m₁ m₂ : M
⊢ single m₁ r₁ = single m₂ r₂ ↔ m₁ = m₂ ∧ r₁ = r₂ ∨ r₁ = 0 ∧ r₂ = 0

Tactic:
simp [← coeff_inj, Finsupp.single_eq_single_iff]

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = s.sup fun x ↦ t.sup fun x_1 ↦ g (f x x_1)

Tactic:
simp only [image₂, sup_image, sup_product_left]

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (s.sup fun i ↦ t.sup fun i' ↦ (g ∘ uncurry f) (i, i')) = s.sup fun x ↦ t.sup fun x_1 ↦ g (f x x_1)
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
j : ι
⊢ (B.repr ((algebraMap R S) r)) j = (Finsupp.single i r) j

Tactic:
simp [Algebra.algebraMap_eq_smul_one, ← hBi]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
⊢ 1 < #(map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A) ∨ 1 < #(map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B)

Tactic:
card_map

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
⊢ 1 < #A ∨ 1 < #B
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
⊢ ∀ (x : α) (y z : K[X]), (x • y) • z = x • y • z

Tactic:
by
    rintro _ ⟨⟩ ⟨⟩
    simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
k : ℕ
⊢ (monomial n) r ^ k = (monomial (n * k)) (r ^ k)

Tactic:
induction k with
  | zero => simp [pow_zero, monomial_zero_one]
  | succ k ih => simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * (X * p) = p * X ^ (n + 1)

Tactic:
X_mul,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * (p * X) = p * X ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ X * (monomial n) r = (monomial (n + 1)) r

Tactic:
X_mul,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
r : R
⊢ (monomial n) r * X = (monomial (n + 1)) r
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ ((monomial n) c).coeffs = {c}

Tactic:
rw [coeffs, support_monomial n hc]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Semiring R
inst✝ : DecidableEq ι
⊢ LinearIndependent R fun i ↦ single i 1

Tactic:
by
  rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
  exact Pi.linearIndependent_single (fun (_ : ι) (_ : Unit) ↦ (1 : R))
    <| by simp +contextual [Fintype.linearIndependent_iffₛ]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (p.projection q hpq) x + (q.projection p ⋯) x = x

Tactic:
dsimp only [projection, projectionOnto]

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ (p.subtype ∘ₗ LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q hpq).symm) x +
      (q.subtype ∘ₗ LinearMap.fst R ↥q ↥p ∘ₗ ↑(q.prodEquivOfIsCompl p ⋯).symm) x =
    x
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
a : WithBot α
⊢ 1 ≤ a ↔ 0 < a

Tactic:
cases a <;> simp [Order.one_le_iff_pos]

Goal state after: