mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝¹ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Finite β
hlt : Nat.card β < Nat.card α
⊢ P β

Tactic:
hn

Goal state after:
case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝¹ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Finite β
hlt : Nat.card β < n
⊢ P β
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
⊢ x ∈ normalizer S

Tactic:
have := Classical.propDecidable; cases nonempty_fintype S
  exact fun n =>
    ⟨h n, fun h₁ =>
      have heq : (fun n => x * n * x⁻¹) '' S = S :=
        Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
          (by rw [Set.card_image_of_injective S conj_injective])
      have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
      let ⟨y, hy⟩ := this
      conj_injective hy.2 ▸ hy.1⟩

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
⊢ a₁ = a₂

Tactic:
classical
  set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
  have hsurj : f'.Surjective := by
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := hsurj y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
  have := hs.fintype
  have := Fintype.ofSurjective _ hsurj
  set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
  exact
    @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
      (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
      (by simpa) a₂ (by simpa) (by simpa)

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H),
    (fun q i ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁) =
        (fun q i ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
⊢ finZeroElim = 0

Tactic:
by
  rw [Matrix.empty_eq finZeroElim, Matrix.zero_empty]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 3 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
by
  simp only [three_lt_ncard_iff hs, exists_and_left]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : Nonempty α
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}

Tactic:
let g := Function.surjInv hf

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf
⊢ Nat.card α ≤ Nat.card β + 1 ↔ ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico_of_not_isMin ha b

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ ↑p₁
h2 : (x1, x2).2 ∈ ↑p₂
⊢ (inl R M M₂) x1 ∈ map (inl R M M₂) p₁

Tactic:
simpa using h1

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
        (bddAbove_range_partialSups.not.mpr h)]

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j ∨ i = j
⊢ ∃ n, succ^[n] i = j

Tactic:
rcases hij with hij | hij

Goal state after:
case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
⊢ ∃ n, succ^[n] i = j

case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i = j
⊢ ∃ n, succ^[n] i = j
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ i, ∏ j > i, f j i * f i j = ∏ i, ∏ j ∈ {i}ᶜ, f j i

Tactic:
← Ioi_disjUnion_Iio,

Goal state after:
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ i, ∏ j > i, f j i * f i j = ∏ x, ∏ x_1 ∈ (Ioi x).disjUnion (Iio x) ⋯, f x_1 x
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hx : x ∈ I
h : y * x = 1
z : α
x✝ : z ∈ ⊤
⊢ z * (y * x) = z

Tactic:
rw [h, mul_one]

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1, ∃ (_ : x * x_1 ∈ I), ¬(x ∈ I ∨ x_1 ∈ I)) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I

Tactic:
not_or

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (I = ⊤ ∨ ∃ x x_1, ∃ (_ : x * x_1 ∈ I), x ∉ I ∧ x_1 ∉ I) ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ y ∈ I

Tactic:
specialize oJ J x IJ hx xJ

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
⊢ y ∈ I
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ x * y - (x * y - 1) ∈ J

Tactic:
exact J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))

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

Goal state before:
pp: case e_a
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)

Tactic:
· refine prod_congr rfl fun i hi ↦ ?_
    rw [choose_symm (this _ hi)]

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

Goal state before:
pp: case inr.h
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
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
⊢ n = s.max' ne✝ → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
hn

Goal state after:
case inr.h
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
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
ha : ¬∃ i, a ∈ s i
i : ι
⊢ (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true]

Goal state after:
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
  simpa only [Ico_toDual] using! h

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝ : Nonempty α
s : Set α
hs : s ∈ ⊤
⊢ s.Nonempty

Tactic:
mem_top.1 hs,

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f g : Filter α
s✝ t : Set α
inst✝ : Nonempty α
s : Set α
hs : s ∈ ⊤
⊢ univ.Nonempty
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
inst✝ : Nonempty ι
s : Set α
⊢ s ∈ iInf f ↔ ∃ i, s ∈ f i

Tactic:
by
  simp only [← Filter.mem_sets, iInf_sets_eq h, mem_iUnion]

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

Goal state before:
pp: ι : Type u_6
α : ι → Type u_7
i : ι
f : Filter (α i)
⊢ (comap (eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot

Tactic:
by
  rcases isEmpty_or_nonempty (∀ j, α j) with H | H
  · rw [filter_eq_bot_of_isEmpty (f.comap _), ← not_iff_not]
    simp [← Classical.nonempty_pi]
  · have : ∀ j, Nonempty (α j) := Classical.nonempty_pi.1 H
    simp [comap_neBot_iff_frequently, *]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
atTop_Ici_eq,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto f l (comap Subtype.val atTop) ↔ Tendsto (fun x ↦ ↑(f x)) l atTop
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha✝ : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
ha : a₁ < a₂
⊢ a₁ • b₁ < a₂ • b₂

pp: case refine_2
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂

Tactic:
· exact (smul_le_smul_of_nonneg_left hb h₁.le).trans_lt (smul_lt_smul_of_pos_right ha h₂)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
h : a₁ • b₁ = a₂ • b₂
hb : b₁ < b₂
⊢ a₁ • b₁ < a₂ • b₂
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case refine_1
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R (span A ↑s) ≤ restrictScalars R S

Tactic:
have := span_le.mp e.le

Goal state after:
case refine_1
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
this : ↑s ⊆ ↑(restrictScalars R S)
⊢ restrictScalars R (span A ↑s) ≤ restrictScalars R S
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝² : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝¹ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this✝ : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : Module.Finite A₂ B₁
⊢ Module.Finite A₂ B₂

Tactic:
exact equiv e.toLinearEquiv

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ Module.Finite R≥0 R

Tactic:
by
  simp_rw [Module.finite_def, Submodule.fg_def, Submodule.eq_top_iff']
  refine ⟨{1, -1}, by simp, fun x ↦ ?_⟩
  obtain hx | hx := le_total 0 x
  · simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨x, hx⟩ (x := 1)
      (Submodule.subset_span <| by simp)
  · simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨-x, neg_nonneg.mpr hx⟩ (x := -1)
      (Submodule.subset_span <| by simp)

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

Goal state before:
pp: case inr
o : Ordinal.{u_4}
ho : IsSuccPrelimit o
⊢ o.pred = o ↔ IsSuccPrelimit o

Tactic:
· simp_rw [ho.ordinalPred_eq, ho]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ #α ≤ (type fun x1 x2 ↦ x1 < x2).card

Tactic:
card_type,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ #α ≤ #{ x // x ∈ s }
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
h0 : 0 < o
a : o.ToType
⊢ ¬a < (enum fun x1 x2 ↦ x1 < x2) ⟨0, ⋯⟩

Tactic:
apply enum_zero_le

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b✝ : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a b : α × γ
h : Prod.Lex r t a b
⊢ Prod.Lex s t (f a.1, a.2) (f b.1, b.2)

Tactic:
obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h

Goal state after:
case left
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a₁✝ : α
b₁✝ : γ
a₂✝ : α
b₂✝ : γ
h' : r a₁✝ a₂✝
⊢ Prod.Lex s t (f (a₁✝, b₁✝).1, (a₁✝, b₁✝).2) (f (a₂✝, b₂✝).1, (a₂✝, b₂✝).2)

case right
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a✝ : α
b₁✝ b₂✝ : γ
h' : t b₁✝ b₂✝
⊢ Prod.Lex s t (f (a✝, b₁✝).1, (a✝, b₁✝).2) (f (a✝, b₂✝).1, (a✝, b₂✝).2)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b✝ : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a b : γ × α
h : Prod.Lex t r a b
⊢ Prod.Lex t s (a.1, f a.2) (b.1, f b.2)

Tactic:
obtain ⟨-, -, h'⟩ | ⟨-, h'⟩ := h

Goal state after:
case left
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a₁✝ : γ
b₁✝ : α
a₂✝ : γ
b₂✝ : α
h' : t a₁✝ a₂✝
⊢ Prod.Lex t s ((a₁✝, b₁✝).1, f (a₁✝, b₁✝).2) ((a₂✝, b₂✝).1, f (a₂✝, b₂✝).2)

case right
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a✝ : γ
b₁✝ b₂✝ : α
h' : r b₁✝ b₂✝
⊢ Prod.Lex t s ((a✝, b₁✝).1, f (a✝, b₁✝).2) ((a✝, b₂✝).1, f (a✝, b₂✝).2)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a + 1 ≤ b ↔ a < b

Tactic:
refine inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩ <;> rintro ⟨f⟩

Goal state after:
case refine_1
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r emptyRelation ≼i s
⊢ type r < type s

case refine_2
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ type r + 1 ≤ type s
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono f ∧ range f = s → enumOrd s = f

Tactic:
· rintro ⟨h₁, h₂⟩
    rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ (type r).card = ↑(Fintype.card α)

Tactic:
card_type,

Goal state after:
α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ #α = ↑(Fintype.card α)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
⊢ (o'.bsup fun a ha ↦ f (g a ha) ⋯) = o.bsup f

Tactic:
apply le_antisymm <;> refine bsup_le fun i hi => ?_

Goal state after:
case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o'
⊢ f (g i hi) ⋯ ≤ o.bsup f

case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

pp: case inr
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
hb : b ≠ 0
⊢ a / b = c

Tactic:
· simp at hlt

Goal state after:
case inr
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
hb : b ≠ 0
⊢ a / b = c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
· rw [← hg, lt_blsub_iff] at hi
    rcases hi with ⟨j, hj, hj'⟩
    exact (hf _ _ hj').trans (le_bsup _ _ _)

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

Goal state before:
pp: x y z : Ordinal.{u_4}
⊢ x * y % (x * z) = x * (y % z)

Tactic:
obtain rfl | hx := eq_zero_or_pos x
  · simp
  · convert! mul_add_mod_mul hx y z using 1 <;>
    rw [add_zero]

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

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

Tactic:
rw [div_le hn', succ_eq_add_one, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm,
        ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]

Goal state after:
case a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n < (m / n).succ
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ u * v + w < b ^ x

Tactic:
apply (opow_mul_add_lt_opow_mul hw hv).trans_le
  rw [← opow_succ]
  exact opow_le_opow_right hv.pos (succ_le_of_lt hu)

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

Goal state before:
pp: case case1.inr
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
hy : (clog.go x b x).snd ≥ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
apply_rules [iff_of_false, Nat.not_le_of_gt, Nat.lt_add_one_of_le]
      exact Nat.lt_of_le_of_lt (Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) hy) H₁

Goal state after: