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

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y + x * z} = span {x, y}

Tactic:
by
  rw [span_pair_comm, span_pair_add_right_mul, span_pair_comm]

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

Goal state before:
pp: case inr.succ
n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)

Tactic:
← Ico_insert_right (by lia),

Goal state after:
case inr.succ
n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ ∑ m ∈ insert (n + 1) (Ico k (n + 1)), m.choose k = (n + 1 + 1).choose (k + 1)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ↑(Submonoid.powers a) → a_1 ∉ ↑I

Tactic:
ha.coe_powers

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ {1, a} → a_1 ∉ ↑I
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case not_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
ha : IsUnit a
⊢ span {a} = ⊤

Tactic:
span_singleton_eq_top.2 ha

Goal state after:
case not_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
ha : IsUnit a
⊢ ⊤ = ⊤
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
⊢ f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K

Tactic:
by
  nth_rw 2 [iterateMapComap]
  rw [iterate_succ', Function.comp_apply, ← iterateMapComap, ← map_le_iff_le_comap]
  induction n with
  | zero => exact h
  | succ n ih =>
    simp_rw [iterateMapComap, iterate_succ', Function.comp_apply]
    calc
      _ ≤ (f.iterateMapComap i n K).map i := map_comap_le _ _
      _ ≤ (((f.iterateMapComap i n K).map f).comap f).map i := by grw [← le_comap_map]
      _ ≤ _ := by gcongr; exact ih

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (a : R ⧸ I) (x y : (ι → R) ⧸ pi fun x ↦ I), a • (x + y) = a • x + a • y

Tactic:
by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (smul_add _ _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
x : ℕ →₀ P
⊢ ∀ x_1 ∈ x.support, (x_1 ∉ Set.range fun x ↦ x + 1) → ((((inr R P M ∘ₗ f) ^ x_1) ∘ₗ inl R P M) (x x_1)).2 = 0

Tactic:
by simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
set n := s.max' ne with hn

Goal state after:
case inr
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ := s.max' ne
hn : n = s.max' ne
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type w
f : ι → Filter α
m : α → β
p : ι → Prop
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) {x | p x}
ne : ∃ i, p i
⊢ map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), map m (f i)

Tactic:
have := nonempty_subtype.2 ne
  simp only [iInf_subtype']
  exact map_iInf_eq h.directed_val

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter (α → β)
g : Filter α
s : Set β
⊢ s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s

Tactic:
simp only [mem_seq_def, seq_subset]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
⊢ atTop.HasBasis (fun x ↦ a ≤ x) Ici

Tactic:
by
  have : Nonempty α := ⟨a⟩
  refine atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
  exact ⟨c, hac, Ici_subset_Ici.2 hbc⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
⊢ let this := e.zero;
  let this_1 := Equiv.smul R e;
  NoZeroSMulDivisors R α

Tactic:
extract_lets

Goal state after:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst✝³ : Zero R
inst✝² : Zero β
inst✝¹ : SMul R β
inst✝ : NoZeroSMulDivisors R β
this✝¹ : Zero α := e.zero
this✝ : SMul R α := Equiv.smul R e
⊢ NoZeroSMulDivisors R α
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
e : α ≃ β
inst✝² : AddCommMonoid β
inst✝¹ : Module R β
inst✝ : Module.IsTorsionFree R β
⊢ let this := e.addCommMonoid;
  let this_1 := Equiv.module R e;
  Module.IsTorsionFree R α

Tactic:
extract_lets

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
e : α ≃ β
inst✝² : AddCommMonoid β
inst✝¹ : Module R β
inst✝ : Module.IsTorsionFree R β
this✝¹ : AddCommMonoid α := e.addCommMonoid
this✝ : Module R α := Equiv.module R e
⊢ Module.IsTorsionFree R α
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), PosSMulStrictMono α (β i)
⊢ ∀ ⦃a : α⦄,
    0 < a → ∀ ⦃b₁ b₂ : (i : ι) → β i⦄, (b₁ ≤ b₂ ∧ ∃ i, b₁ i < b₂ i) → a • b₁ ≤ a • b₂ ∧ ∃ i, (a • b₁) i < (a • b₂) i

Tactic:
rintro _a ha _b₁ _b₂ ⟨hb, i, hi⟩

Goal state after:
α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), PosSMulStrictMono α (β i)
_a : α
ha : 0 < _a
_b₁ _b₂ : (i : ι) → β i
hb : _b₁ ≤ _b₂
i : ι
hi : _b₁ i < _b₂ i
⊢ _a • _b₁ ≤ _a • _b₂ ∧ ∃ i, (_a • _b₁) i < (_a • _b₂) i
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc'✝ : b < f c
hc' : a ≤ c
⊢ False

Tactic:
exact hc.not_ge hc'

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f (f^[n] a) ≤ ⨆ n, f^[n] a

Tactic:
rw [← f.iterate_succ_apply']
    exact le_ciSup hf' _

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

Goal state before:
pp: o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ ?m.25 < Ordinal.liftPrincipalSeg.top

Tactic:
by simpa using h

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

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
ha.ordinalPred_eq,

Goal state after:
case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a ≤ b ↔ a ≤ succ b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ StrictMono f ∧ range f = s → Subtype.val ∘ ⇑(enum s hs) = f

Tactic:
rintro ⟨hf, rfl⟩
    rw [← StrictMono.range_inj H hf]
    simp
    rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Ordinal.{v} ≤i Ordinal.{max u v}

Tactic:
by
  refine ⟨RelEmbedding.ofMonotone lift.{u} (by simp),
    fun a b ↦ Ordinal.inductionOn₂ a b fun α r _ β s _ h ↦ ?_⟩
  rw [RelEmbedding.ofMonotone_coe, ← lift_id'.{max u v} (type s),
    ← lift_umax.{v, u}, lift_type_lt] at h
  obtain ⟨f⟩ := h
  use typein r f.top
  rw [RelEmbedding.ofMonotone_coe, ← lift_umax, lift_typein_top, lift_id']

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.bsup f = o₂.bsup fun a h ↦ f a ⋯

Tactic:
subst ho
  rfl

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

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ b ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨a, ⋯⟩

Tactic:
rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
        Subtype.mk_le_mk, ← lt_succ_iff, ha]
      exact typein_lt_type ..

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.blsub f = o₂.blsub fun a h ↦ f a ⋯

Tactic:
subst ho
  rfl

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

Goal state before:
pp: b n : ℕ
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
rcases Nat.lt_or_ge 1 b with hb | hb
  · rcases eq_or_ne n 0 with rfl | hn
    · grind [log_of_lt]
    · rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]
  · simp [hb, log_of_left_le_one]

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b

Tactic:
rw [← mul_le_iff_le_div b0, mul_add, add_le_add_iff_left]

Goal state after:
case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
⊢ 0 ^ a ≤ 1

Tactic:
by
  rw [zero_opow']
  exact sub_le_self 1 a

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

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)

Tactic:
rw [log_of_left_le_one hb]
    exact zero_le _

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

Goal state before:
pp: b n : ℕ
⊢ log b (n / b) = log b n - 1

Tactic:
by
  rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb, log_of_left_le_one hb, Nat.zero_sub]
  rcases lt_or_ge n b with h | h
  · rw [div_eq_of_lt h, log_of_lt h, log_zero_right]
  rw [log_of_one_lt_of_le hb h, Nat.add_sub_cancel_right]

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

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : a ≤ 1
⊢ a ^ b ≠ 1

pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ a ^ b ≠ 1

Tactic:
· simp_all [le_one_iff]

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ a ^ b ≠ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
⊢ a ^ c ≤ b ^ c

Tactic:
by_cases c = 0 <;> simp_all

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

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
by_cases c = 0 <;> simp_all

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

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

Tactic:
simp_rw [log, one_opow, preimage_const]

Goal state after:
case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ sSup (if 1 ∈ Iic x then univ else ∅) = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n

Tactic:
rw [log_of_left_le_one hb]
    exact zero_le _

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ List.foldr f a l ≤ a

Tactic:
List.foldr_fixed' h l

Goal state after:
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
l : List ι
⊢ a ≤ a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ 0 < o / b ^ log b o

Tactic:
· rw [div_pos (opow_ne_zero _ hb.ne')]
    exact opow_log_le_self b ho

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ¬BddAbove (fixedPoints f)

Tactic:
by
  convert! not_bddAbove_fp_family fun _ : Unit => H
  exact (Set.iInter_const _).symm

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

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * (1 + ω) ≤ a * ω

Tactic:
one_add_omega0

Goal state after:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * ω ≤ a * ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a * (1 + ω) + (b - a * ω) = b

Tactic:
one_add_omega0

Goal state after:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a * ω + (b - a * ω) = b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ (1 + ω) ≤ a ^ ω

Tactic:
one_add_omega0

Goal state after:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a ^ ω ≤ a ^ ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a ^ (1 + ω) * c = a ^ ω * c

Tactic:
one_add_omega0

Goal state after:
case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a ^ ω * c = a ^ ω * c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preOmega o = ω_ o

Tactic:
← opow_natCast

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = ω_ o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ (1 + ω) * succ b ≤ a ^ ω * succ b

Tactic:
one_add_omega0

Goal state after:
case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ a ^ ω * succ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
simp_rw [isPrincipal_add_iff_add_self_lt, ← Ordinal.mul_two]
    exact fun a ha ↦ ho ha ho₂

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

Goal state before:
pp: case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω
⊢ a * ω = ω

Tactic:
exact mul_omega0 a0 h

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

Goal state before:
pp: case inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
· exact le_max_of_le_right (add_lt_aleph0 ha hb).le

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preBeth o = ℶ_ o

Tactic:
← opow_natCast

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preBeth o = ℶ_ o
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ ⨆ i, ↑(f i) + 1 ≤ o

pp: case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ o ≤ ⨆ i, ↑(f i) + 1

Tactic:
· simp_rw [Ordinal.iSup_le_iff, add_one_le_iff]
    exact fun i ↦ (f i).2

Goal state after:
case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ o ≤ ⨆ i, ↑(f i) + 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n✝ : ℕ
hn : n✝ ≠ 0
n : ℕ
hneq1 : n + 1 + 1 ≠ 0
⊢ StrictMono fun a ↦ ↑(n + 1 + 1) * a

Tactic:
intro a μ hlt
    push_cast
    conv_lhs => rw [add_mul, one_mul]
    conv_rhs => rw [add_mul, one_mul]
    refine Cardinal.add_lt_add ?_ hlt
    simpa using! (natCast_mul_strictMono (Nat.succ_ne_zero n) hlt)

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

Goal state before:
pp: κ μ : Cardinal.{u}
H1✝ : ℵ₀ ≤ κ
H2 : μ < ℵ₀
n✝ : ℕ
H3 : μ = ↑n✝
α : Type u
H1 : ℵ₀ ≤ ⟦α⟧
n : ℕ
ih : ⟦α⟧ ^ ↑n ≤ ⟦α⟧
⊢ ⟦α⟧ ^ ↑n.succ ≤ ⟦α⟧

Tactic:
by grw [Nat.cast_succ, power_add, power_one, ih, mul_eq_self H1]

Goal state after:
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} #ι
i : ι
⊢ 2 ≤ lift.{u, v} (c i)

Tactic:
← lift_two.{u, v},

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} #ι
i : ι
⊢ lift.{u, v} 2 ≤ lift.{u, v} (c i)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: case inl
β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : #α < ℵ₀
⊢ ∃ a, ℵ₀ ≤ #↑(f ⁻¹' {a})

Tactic:
exact infinite_pigeonhole_card f ℵ₀ (aleph0_le_mk β) le_rfl
      (by rwa [isRegular_aleph0.cof_ord])

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

Goal state before:
pp: case inl
β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ ∃ a, ℵ_ 1 ≤ #↑(f ⁻¹' {a})

Tactic:
exact infinite_pigeonhole_card f ℵ₁ (by simp) aleph0_lt_aleph_one.le
      (by rw [isRegular_aleph_one.cof_ord]; exact hα.trans aleph0_lt_aleph_one)

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

Goal state after:
ι : 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
i : ι
j : α i
⊢ ((f + g).sigmaCurry i) j = ((f.sigmaCurry + g.sigmaCurry) i) j
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)

Goal state after:
ι : 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
i : ι
j : α i
⊢ ((r • f).sigmaCurry i) j = ((r • f.sigmaCurry) i) j
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
s : Set (Set ι)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ ∀ (i : ↑s), LinearIndepOn R v ↑i

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝² : Semiring R
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₂ i)
inst✝ : (i : ι) → Module R (β₂ i)
⊢ (linearMap fun i ↦ LinearMap.id) = LinearMap.id

Tactic:
by
  ext
  simp [linearMap]

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)
⊢ ∀ (i : ↑s), LinearIndepOn R v (t ↑i)

Tactic:
by simpa using h

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t

Tactic:
let indep : Set ι → Prop := fun s => LinearIndepOn R v s

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
⊢ ∃ s, LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module R₂ N
inst✝² : Module R₃ P
inst✝¹ : Module R₅ P
inst✝ : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
⊢ h.compl₂ id = h

Tactic:
ext
  rw [compl₂_apply, id_coe, _root_.id]

Goal state after:
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✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
⊢ (s - t) • x + t • (x + y) = 0

Tactic:
rw [sub_smul, smul_add, ← h']; abel

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

Goal state before:
pp: k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : Semiring k
inst✝² : One G
g_hom : Type u_6
inst✝¹ : FunLike g_hom G R
inst✝ : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ (liftNC ↑f ⇑g) 1 = 1

Tactic:
by simp [one_def]

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

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

Tactic:
by
  rw [← MonoidHom.map_mclosure] at h; simpa using of_mem_span_of_iff.1 h

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
hf : Injective (f a)
⊢ #(image₂ f {a} t) = #t

Tactic:
by
  rw [image₂_singleton_left, card_image_of_injective _ hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ↑u ⊆ image2 f s t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Tactic:
rw [← Set.image_prod, subset_set_image_iff] at hu
  rcases hu with ⟨u, hu, rfl⟩
  classical
  use u.image Prod.fst, u.image Prod.snd
  simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]
  exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : One M
⊢ (coeff 1) 1 = 1

Tactic:
by simp [one_def]

Goal state after: