mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < lift.{v, u} (succ a).ord
⊢ b ∈ range lift.{v, u}

Tactic:
exact mem_range_lift_of_le h.le

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

Goal state before:
pp: case inl
b n : ℕ
h₁ : b ^ 0 ≤ n
h₂ : n < b ^ (0 + 1)
⊢ log b n = 0

pp: case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m

Tactic:
· rw [Nat.pow_one] at h₂
    exact log_of_lt h₂

Goal state after:
case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: ⊢ 1 < ω

Tactic:
simpa only [Nat.cast_one] using natCast_lt_omega0 1

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

Goal state before:
pp: b x c : Ordinal.{u_1}
hc : c ≠ 0
h : c ≤ log b x
⊢ b ^ c ≤ x

Tactic:
obtain hb | hb := le_or_gt b 1
  · rw [log_of_left_le_one hb] at h
    exact (h.not_gt (pos_iff_ne_zero.2 hc)).elim
  · rwa [opow_le_iff_le_log' hb hc]

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

Goal state before:
pp: case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ f i (nfpFamily f a)

Tactic:
exact (H i).monotone h

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

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≤ 1
⊢ log b 1 = 0

Tactic:
exact log_of_left_le_one hb 1

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

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * ↑m + ω ^ c * ↑m ≤ ω ^ o

Tactic:
rw [← mul_add, ← Nat.cast_add]

Goal state after:
case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
a : Ordinal.{u_1}
ha : a < ω ^ o
c : Ordinal.{u_1}
hc : c < o
m : ℕ
hm : a < ω ^ c * ↑m
⊢ ω ^ c * ↑(m + m) ≤ ω ^ o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mp
o : Ordinal.{u}
H : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ho : ¬o = 0
⊢ ¬ω ^ log ω o < o

Tactic:
obtain ⟨n, hn⟩ := lt_omega0_opow_succ.1 (lt_opow_succ_log_self one_lt_omega0 o)

Goal state after:
case mp
o : Ordinal.{u}
H : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ho : ¬o = 0
n : ℕ
hn : o < ω ^ log ω o * ↑n
⊢ ¬ω ^ log ω o < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
⊢ #α * #α ≤ #α

Tactic:
let g : α × α → α := uncurry max

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
g : α × α → α := uncurry max
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case mpr
x : Ordinal.{u_1}
⊢ x ∈ {x | ω ≤ x ∧ x.IsInitial} → x ∈ range ⇑ω_

Tactic:
rintro ⟨ha', ha⟩
    obtain ⟨a, rfl⟩ := ha.mem_range_preOmega
    use a - ω
    rw [omega0_le_preOmega_iff] at ha'
    rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']

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

Goal state before:
pp: o : Ordinal.{u_1}
| (typeLT o.ToType).cof

Tactic:
cof_type

Goal state after:
o : Ordinal.{u_1}
| Order.cof o.ToType
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof ≤ o.card

Tactic:
simpa using cof_le_cardinalMk o.ToType

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

Goal state before:
pp: ⊢ range ⇑ℵ_ = Ici ℵ₀

Tactic:
by
  ext c
  refine ⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩
  rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]
  rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

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

Goal state before:
pp: case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c

Tactic:
rw [opow_succ] at ha

Goal state after:
case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
n m k : ℕ
h : n + m = n + k
⊢ m = k

Tactic:
apply add_left_cancel h

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

Goal state before:
pp: o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card

Tactic:
apply (card_iSup_Iio_le_sum_card f).trans

Goal state after:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (sum fun i ↦ (f i.toOrd).card) ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case pos
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : c < ℵ₀
⊢ (⨆ i, f i).card ≤ c

pp: case neg
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
· obtain ⟨n, rfl⟩ := lt_aleph0.1 hc
    rw [card_le_nat]
    refine ciSup_le' fun i ↦ ?_
    simpa using hf i

Goal state after:
case neg
ι : Type u
c : Cardinal.{v}
f : ι → Ordinal.{v}
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ι), (f i).card ≤ c
hc : ℵ₀ ≤ c
⊢ (⨆ i, f i).card ≤ c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (Subtype.val '' range ⇑g)

Tactic:
g.range_eq

Goal state after:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
⊢ IsCofinal (Subtype.val '' Set.univ)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case hι
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ Cardinal.lift.{u, u + 1} #↑s ≤ Cardinal.lift.{u + 1, u} c

Tactic:
rwa [Cardinal.lift_id'.{u, u + 1}]

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ c * ⨆ i, f i = ⨆ i, c * f i

Tactic:
rw [mul_comm, Cardinal.ciSup_mul f]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
⊢ ⨆ i, f i * c = ⨆ i, c * f i
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ ⨆ i, (f i).ord < a.ord

Tactic:
apply Ordinal.lift_iSup_lt_of_lt_cof <;> simpa

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

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
rw [cof_eq_sInf_lsub]
  exact
    (le_csInf_iff'' (cof_lsub_def_nonempty o)).trans
      ⟨fun H ι f hf => H _ ⟨ι, f, hf, rfl⟩, fun H b ⟨ι, f, hf, hb⟩ => by
        rw [← hb]
        exact H _ hf⟩

Goal state after:
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:
rwa [← aleph_zero, aleph_lt_aleph]

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

Goal state before:
pp: case inr.a
α : 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}
⊢ #{ s // Bounded r s } ≤ #α

Tactic:
rw [← coe_ofPred, this]

Goal state after:
case inr.a
α : 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}) ≤ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u
h✝ : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
· rw [mk_list_eq_mk]
    apply le_max_right

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (-x)) i = (-mk s x) i

Tactic:
by simp only [neg_apply, mk_apply]; split_ifs <;> [rfl; rw [neg_zero]]

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

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ (mapRange f hf g).support ⊆ g.support

Tactic:
simp [mapRange_def]

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

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i j : ι
inst✝ : Decidable (0 = 0)
⊢ j ∈ (f.update i 0).support ↔ j ∈ (erase i f).support

Tactic:
simp [update_eq_erase, support_erase]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ s • x = (r • l).eval

Tactic:
rw [← hs, hx, ← hl, eval_smul]

Goal state after:
case h
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ l.eval = l.eval
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (⋃ i_1 ∈ insert i s, f i_1)

Tactic:
rw [Finset.set_biUnion_insert]

Goal state after:
case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
x✝² x✝¹ : A
x✝ : AddChar A M
⊢ { toFun := fun ψ ↦ ψ (x✝² + x✝¹), map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } x✝ =
    ({ toFun := fun ψ ↦ ψ x✝², map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ } +
        { toFun := fun ψ ↦ ψ x✝¹, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ })
      x✝

Tactic:
simp [map_add_eq_mul]

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)

Tactic:
LinearIndepOn,

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑(insert a s)) ↦ f ↑x) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑(insert a s)) ↦ f ↑x) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)

Tactic:
LinearIndepOn,

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑(insert a s)) ↦ f ↑x) ↔
    (LinearIndependent K fun (x : ↑s) ↦ f ↑x) ∧ f a ∉ span K (f '' s)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
⊢ LinearIndependent R (Fin.snoc v x)

Tactic:
by
  apply hv.finSnoc' v x
  intro c y hcy heq
  by_contra hc
  apply hx
  have hc' : algebraMap R K c ≠ 0 := by
    rwa [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff]
  rw [← algebraMap_smul K c x] at heq
  rw [(eq_inv_smul_iff₀ hc').mpr (eq_neg_of_add_eq_zero_left heq), smul_neg]
  exact Submodule.neg_mem _ (Submodule.smul_mem _ _ (Submodule.span_subset_span R K _ hcy))

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 γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : γ → β → δ
g : α → γ
⊢ ↑(image₂ f (image g s) t) = ↑(image₂ (fun a b ↦ f (g a) b) s t)

Tactic:
by
    push_cast
    exact image2_image_left _ _

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case right
R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Function.Surjective ⇑(p.subtype.coprod q.subtype)

Tactic:
rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]

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

Goal state before:
pp: σ : Type u_1
inst✝ : Finite σ
⊢ AddGroup.FG (FreeAbelianGroup σ)

Tactic:
← Module.Finite.iff_addGroup_fg

Goal state after:
σ : Type u_1
inst✝ : Finite σ
⊢ Module.Finite ℤ (FreeAbelianGroup σ)
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ a * ⨅ i, f i = ⨅ i, a * f i

Tactic:
obtain hι | hι := isEmpty_or_nonempty ι
  · suffices a ≠ 0 by simpa [iInf_of_empty, ite_eq_right_iff, mul_top']
    aesop
  rw [mul_iInf]

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

Goal state before:
pp: s : Set ℕ∞
a : ℕ∞
hs : s.Nonempty
⊢ a + sSup s = ⨆ b ∈ s, a + b

Tactic:
by
  rw [sSup_eq_iSup, add_biSup hs]

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

Goal state before:
pp: case inl
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
tsub_eq_zero_iff_le.2 <| le_iSup_of_le _ hi.le,

Goal state after:
case inl
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ 0 = ⨅ i, a - f i
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₁ ×ˢ s₂ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ R

Tactic:
rw [← R.inv_eq_self, SetRel.inv, ← Set.image_subset_iff, Set.image_swap_prod, ← SetRel.inv,
    R.inv_eq_self]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
⊢ p.toList.getLast ⋯ = p.last

Tactic:
by
  grind [length_toList, last, Fin.last, toList_getElem]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
i : Fin (p.length + 1)
x✝ : Fin p.length
⊢ (p.smash q h).toFun (Fin.castLE ⋯ x✝.castSucc) = p.toFun x✝.castSucc

Tactic:
by dsimp only [smash]; apply Fin.addCases_left

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ span R (image2 (fun m n ↦ (f m) n) (⋃ i, ↑(s i)) ↑t) = span R (⋃ i, image2 (fun m n ↦ (f m) n) ↑(s i) ↑t)

Tactic:
Set.image2_iUnion_left

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : α
inst✝ : OrderTop α
h : x < ⊤
⊢ 0 < coheight x

Tactic:
by
  rw [coheight_pos]
  grind [not_isMax_iff]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁵ : CommSemiring R
inst✝³⁴ : CommSemiring R₂
inst✝³³ : CommSemiring R₃
inst✝³² : Monoid R'
inst✝³¹ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid N
inst✝²⁸ : AddCommMonoid P
inst✝²⁷ : AddCommMonoid Q
inst✝²⁶ : AddCommMonoid S
inst✝²⁵ : AddCommMonoid P'
inst✝²⁴ : AddCommMonoid Q'
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid N₂
inst✝²¹ : AddCommMonoid P₂
inst✝²⁰ : AddCommMonoid Q₂
inst✝¹⁹ : AddCommMonoid M₃
inst✝¹⁸ : AddCommMonoid N₃
inst✝¹⁷ : AddCommMonoid P₃
inst✝¹⁶ : AddCommMonoid Q₃
inst✝¹⁵ : DistribMulAction R' M
inst✝¹⁴ : Module R'' M
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Module R S
inst✝¹⁰ : Module R P'
inst✝⁹ : Module R Q'
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Module R₂ N₂
inst✝⁶ : Module R₂ P₂
inst✝⁵ : Module R₂ Q₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₃ N₃
inst✝² : Module R₃ P₃
inst✝¹ : Module R₃ Q₃
inst✝ : Subsingleton M
z : M ⊗[R] N
x : M
y : N
⊢ x ⊗ₜ[R] y = 0

Tactic:
Subsingleton.elim x 0,

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁵ : CommSemiring R
inst✝³⁴ : CommSemiring R₂
inst✝³³ : CommSemiring R₃
inst✝³² : Monoid R'
inst✝³¹ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³⁰ : AddCommMonoid M
inst✝²⁹ : AddCommMonoid N
inst✝²⁸ : AddCommMonoid P
inst✝²⁷ : AddCommMonoid Q
inst✝²⁶ : AddCommMonoid S
inst✝²⁵ : AddCommMonoid P'
inst✝²⁴ : AddCommMonoid Q'
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid N₂
inst✝²¹ : AddCommMonoid P₂
inst✝²⁰ : AddCommMonoid Q₂
inst✝¹⁹ : AddCommMonoid M₃
inst✝¹⁸ : AddCommMonoid N₃
inst✝¹⁷ : AddCommMonoid P₃
inst✝¹⁶ : AddCommMonoid Q₃
inst✝¹⁵ : DistribMulAction R' M
inst✝¹⁴ : Module R'' M
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Module R S
inst✝¹⁰ : Module R P'
inst✝⁹ : Module R Q'
inst✝⁸ : Module R₂ M₂
inst✝⁷ : Module R₂ N₂
inst✝⁶ : Module R₂ P₂
inst✝⁵ : Module R₂ Q₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₃ N₃
inst✝² : Module R₃ P₃
inst✝¹ : Module R₃ Q₃
inst✝ : Subsingleton M
z : M ⊗[R] N
x : M
y : N
⊢ 0 ⊗ₜ[R] y = 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
⊢ 0 < krullDim α ↔ Nontrivial α

Tactic:
by
  rw [← not_subsingleton_iff_nontrivial, ← Order.krullDim_eq_zero_iff_of_orderTop,
    ← ne_eq, ← lt_or_lt_iff_ne, or_iff_right]
  simp [Order.krullDim_nonneg]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ IsUnit ((Algebra.lmul R A) x) ↔ IsUnit x

Tactic:
rw [Module.End.isUnit_iff, Iff.comm]
  exact IsUnit.isUnit_iff_mulLeft_bijective

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ s * t → n ∈ x → r • n ∈ s • t • x

Tactic:
rintro _ _ ⟨_, _, _, _, rfl⟩ _; rw [mul_smul]; aesop

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
hr : r ∈ s
this : SMulCommClass R R ↥x
c : R →₀ ↥x
hc1 : ↑c.support ⊆ t
hm : ↑(c.sum fun r m ↦ r • m) ∈ t • x
⊢ ∑ x_1 ∈ c.support, (r * x_1) • ↑(c x_1) ∈ (s * t) • x

Tactic:
exact Submodule.sum_mem _ fun r' hr' ↦
        mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
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
g : P →ₗ[R] Q
f : N →ₗ[R] P
m : M
n : N
⊢ (((TensorProduct.mk R M N).compr₂ₛₗ (lTensor M (g ∘ₗ f))) m) n =
    (((TensorProduct.mk R M N).compr₂ₛₗ (lTensor M g ∘ₗ lTensor M f)) m) n

Tactic:
simp only [compr₂ₛₗ_apply, mk_apply, comp_apply, lTensor_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R S
inst✝¹ : Module R P
inst✝ : Module R Q
g' : Q →ₗ[R] S
f : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ lTensor P g' ∘ₗ map f g = map f (g' ∘ₗ g)

Tactic:
simp only [lTensor, ← map_comp, id_comp]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
mn : R
hmn : mn ∈ M ⊔ N
p : R
hp : p ∈ P
⊢ mn * p ∈ M * P ⊔ N * P

Tactic:
obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N P : AddSubmonoid R
p : R
hp : p ∈ P
m : R
hm : m ∈ M
n : R
hn : n ∈ N
hmn : m + n ∈ M ⊔ N
⊢ (m + n) * p ∈ M * P ⊔ N * P
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
a b c : α
⊢ decide (a ≤ b) = true → decide (b ≤ c) = true → decide (a ≤ c) = true

Tactic:
simpa using le_trans

Goal state after: