mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Idempotent

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

Tactic:
sub_right_inj,

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ (x + y) ^ 0 = ∑ m ∈ range (0 + 1), t 0 m

Tactic:
rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = t 0 0
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x, y} = span {y} ↔ y ∣ x

Tactic:
rw [Ideal.span_insert, sup_eq_right, span_singleton_le_span_singleton]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
have ⟨M, hM, le⟩ := exists_le_maximal I hI
  have := hM.1.1
  rw [Ne, eq_top_iff, ← hs, span_le, Set.not_subset] at this
  have ⟨a, has, haM⟩ := this
  exact ⟨a, has, Set.disjoint_left.mpr fun x hx ⟨n, hn⟩ ↦
    haM (hM.isPrime.mem_of_pow_mem _ (le <| hn ▸ hx))⟩

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

Goal state before:
pp: case h
n m : ℕ
a✝ : m ∈ range (2 * n + 1)
⊢ (2 * n).choose m ≤ (2 * n).choose (2 * n / 2)

Tactic:
apply choose_le_middle

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
⊢ s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset

Tactic:
induction s using Multiset.induction_on with

Goal state after:
case cons
α : 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
⊢ (a ::ₘ s).sum ^ ((a ::ₘ s).card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) (a ::ₘ s)).toFinset
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ f x i ∈ I

Tactic:
cases nonempty_fintype ι
    rw [pi_eq_sum_univ x]
    simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
    exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

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

Goal state before:
pp: α : Type u
ι : Sort x
s : ι → Filter α
x✝ : Filter α
⊢ x✝ ≤ iInf s ↔ x✝ ≤ generate (⋃ i, (s i).sets)

Tactic:
simp [le_generate_iff]

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

Goal state before:
pp: α : Type u_1
⊢ ⨆ a, pure a = ⨆ a ∈ univ, pure a

Tactic:
iSup_univ

Goal state after:
α : Type u_1
⊢ ⨆ a, pure a = ⨆ x, pure x
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
l₁ : Filter α
l₂ : Filter β
f g : α → β
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
h₀ : Tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂
h₁ : Tendsto g (l₁ ⊓ 𝓟 {x | ¬p x}) l₂
⊢ Tendsto (fun x ↦ if p x then f x else g x) l₁ l₂

Tactic:
by
  simp only [tendsto_def, mem_inf_principal] at *
  intro s hs
  filter_upwards [h₀ s hs, h₁ s hs] with x hp₀ hp₁
  rw [mem_preimage]
  split_ifs with h
  exacts [hp₀ h, hp₁ h]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t) → ∃ i, p i ∧ sa i ×ˢ sb i ⊆ t

pp: case refine_2
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, p i ∧ sa i ×ˢ sb i ⊆ t) → ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t

Tactic:
· rintro ⟨⟨i, j⟩, ⟨hi, hj⟩, hsub : sa i ×ˢ sb j ⊆ t⟩
    rcases h_dir hi hj with ⟨k, hk, ki, kj⟩
    exact ⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, p i ∧ sa i ×ˢ sb i ⊆ t) → ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
t : Set (α × β)
⊢ (∃ i, p i ∧ sa i ×ˢ sb i ⊆ t) → ∃ i, (p i.fst ∧ p i.snd) ∧ sa i.fst ×ˢ sb i.snd ⊆ t

Tactic:
· rintro ⟨i, hi, h⟩
    exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (comap f G ⊓ F) = G ⊓ map f F

Tactic:
simp only [Filter.push_pull, inf_comm]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
⊢ MulOneClass α

Tactic:
apply e.injective.mulOneClass _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Submodule R ↥N
h : (Submodule.map N.subtype s).FG
⊢ s.FG

Tactic:
exact Submodule.fg_of_fg_map_injective N.subtype Subtype.val_injective h

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ ¬IsCofinal s ↔ ∃ x, ∀ y ∈ s, y < x

Tactic:
simp [IsCofinal]

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

Goal state before:
pp: case intro
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Sort u_3
inst✝ : Finite ι
N : ι → Submodule R M
h : ∀ (i : ι), (N i).FG
val✝ : Fintype (PLift ι)
⊢ (iSup N).FG

Tactic:
simpa [iSup_plift_down] using fg_biSup Finset.univ (N ∘ PLift.down) fun i _ => h i.down

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R ↑s) ⋯
⊢ (span R ↑s).FG

Tactic:
by use s

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ f a = ⨆ b, f ↑b

Tactic:
convert! map_iSup hf _

Goal state after:
case e'_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ a = ⨆ i, ↑i

case convert_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ Nonempty ↑(Iio a)

case convert_4
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove (range Subtype.val)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a < b + c ↔ ∃ d < c, a ≤ b + d

Tactic:
by
  use fun h ↦ ⟨_, sub_lt_of_lt_add h hc.bot_lt, le_add_sub a b⟩
  rintro ⟨d, hd, ha⟩
  exact ha.trans_lt (by gcongr)

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

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)

Tactic:
constructor <;> refine fun ⟨f⟩ ↦ ⟨?_⟩
  · exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r).symm).transInitial
      (RelIso.preimage Equiv.ulift s).toInitialSeg
  · exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r)).transInitial
      (RelIso.preimage Equiv.ulift s).symm.toInitialSeg

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

Goal state before:
pp: o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ o'.bsup g

Tactic:
obtain ⟨j, hj, hj'⟩ := h ⟨i, hi, rfl⟩

Goal state after:
o : Ordinal.{u}
o' : Ordinal.{v}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}
g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}
h : o.brange f ⊆ o'.brange g
i : Ordinal.{u}
hi : i < o
j : Ordinal.{v}
hj : j < o'
hj' : g j hj = f i hi
⊢ f i hi ≤ o'.bsup g
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
by
  simpa using card_le_nat (n := 1)

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
h : IsSuccLimit (a + 0)
⊢ IsSuccLimit 0 ∨ 0 = 0 ∧ IsSuccLimit a

pp: case inr
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
· grind

Goal state after:
case inr
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n * b) = log b n + 1

Tactic:
by
  apply log_eq_of_pow_le_of_lt_pow <;> rw [pow_succ', Nat.mul_comm b]
  exacts [Nat.mul_le_mul_right _ (pow_log_le_self _ hn),
    (Nat.mul_lt_mul_right (Nat.zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]

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

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)

Tactic:
· convert! mul_add_mod_mul hx y z using 1 <;>
    rw [add_zero]

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

Goal state before:
pp: case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ b ^ clog b n < n + 1

Tactic:
H

Goal state after:
case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ n < n + 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
obtain hb | hb := lt_or_ge 1 b
  · rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
    exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)
  · simpa only [log_of_left_le_one hb, zero_add] using le_rfl

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

Goal state before:
pp: case neg
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : ¬BddAbove s
⊢ IsPrincipal op (sSup s)

Tactic:
· rwa [csSup_of_not_bddAbove hs]

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

Goal state before:
pp: x : Ordinal.{u_1}
⊢ ω ≤ preOmega x ↔ ω ≤ x

Tactic:
conv_lhs => rw [← preOmega_omega0, preOmega_le_preOmega]

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

Goal state before:
pp: case ind.mk.hbc.inr
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝¹ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this✝ : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : ℵ₀ ≤ #↑(Iio q)
this : #↑(Iio q) < #α
⊢ #↑(Iio q) * #↑(Iio q) < #α

Tactic:
IH _ this hq

Goal state after:
case ind.mk.hbc.inr
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝¹ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this✝ : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : ℵ₀ ≤ #↑(Iio q)
this : #↑(Iio q) < #α
⊢ #↑(Iio q) < #α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ ↑x ∈ s

pp: case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
⊢ r ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩

Tactic:
· grind

Goal state after:
case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
⊢ r ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c

Tactic:
exact l.succ_lt hx

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < preBeth o
⊢ 2 ^ x < preBeth o

Tactic:
rw [preBeth_limit ho] at hx
    obtain ⟨a, ha⟩ := exists_lt_of_lt_ciSup' hx
    apply (preBeth_strictMono (ho.add_one_lt a.2)).trans_le'
    simpa using power_le_power_left two_ne_zero ha.le

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

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b✝ : 1 < m
| n < n * m

Tactic:
left; rw [← mul_one n]

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b✝ : 1 < m
| n * 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ ℶ_ c.ord

Tactic:
simpa using c.ord.card_le_beth

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

Goal state before:
pp: case refine_2.inl
o : Ordinal.{u}
ho₂ : o ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o

Tactic:
exact isPrincipal_mul_of_le_two ho₂

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

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
apply card_iSup_le_lift _ hf

Goal state after:
o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ Cardinal.lift.{v, u + 1} #↑(Iio o) ≤ Cardinal.lift.{u + 1, v} c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
a b : Ordinal.{u_1}
ha : a.card < ℵ_ o
hb : b.card < ℵ_ o
⊢ ((fun x1 x2 ↦ x1 ^ x2) a b).card < ℵ_ o

Tactic:
apply (card_opow_le a b).trans_lt (max_lt _ (max_lt ha hb))

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
H

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
H : o.bsup f = o.blsub f
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

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

Tactic:
suffices Infinite β from exists_infinite_fiber f h
  exact .of_cardinalMk_le h.le

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

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ #α < (ℵ_ 1).ord.cof

Tactic:
by rw [isRegular_aleph_one.cof_ord]; exact hα.trans aleph0_lt_aleph_one

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ < c

Tactic:
exact hc.aleph0_lt

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

Goal state before:
pp: case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : i ∈ ↑xs
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

pp: case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
· grind

Goal state after:
case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : i ∈ ↑ys
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

pp: case inr.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : y i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
· grind

Goal state after:
case inr.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : y i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
H

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
⊢ x = y
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
ij : (i : ι) × α i
x : δ ij.fst ij.snd
⊢ (single ij x).sigmaCurry = single ij.fst (single ij.snd x)

Tactic:
by
  obtain ⟨i, j⟩ := ij
  ext i' j'
  dsimp only
  rw [sigmaCurry_apply]
  obtain rfl | hi := eq_or_ne i i'
  · rw [single_eq_same]
    obtain rfl | hj := eq_or_ne j' j
    · rw [single_eq_same, single_eq_same]
    · rw [single_eq_of_ne, single_eq_of_ne hj]
      simpa using hj
  · simp [hi]

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

Goal state before:
pp: case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | f i ≠ 0}
⊢ i ∈ {i ∈ sy.toFinset | f i ≠ 0}

Tactic:
rcases Finset.mem_filter.1 H with ⟨_, h⟩

Goal state after:
case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
H : i ∈ {i ∈ sx.toFinset | f i ≠ 0}
left✝ : i ∈ sx.toFinset
h : f i ≠ 0
⊢ i ∈ {i ∈ sy.toFinset | f i ≠ 0}
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | f i ≠ 0}
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0}

Tactic:
rcases Finset.mem_filter.1 H with ⟨_, h⟩

Goal state after:
case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
H : i ∈ {i ∈ sy.toFinset | f i ≠ 0}
left✝ : i ∈ sy.toFinset
h : f i ≠ 0
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0}
Module: Mathlib.Data.Fin.Tuple.Reflection

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (seq (Matrix.vecTail f) (Matrix.vecTail v)) i = f i (v i)

Tactic:
seq_eq

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun i ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)