mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | k ≤ a.1} =
    map ({ toFun := fun x ↦ x + k, inj' := ⋯ }.prodMap (Embedding.refl ℕ)) (antidiagonal (n - k))

Tactic:
ext ⟨i, j⟩
  suffices i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa
  refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩
  · rw [← Nat.sub_add_comm hi.2, hi.1]
  · rintro ⟨l, hl, rfl⟩
    refine ⟨?_, Nat.le_add_left k l⟩
    rw [add_right_comm, hl]
    exact tsub_add_cancel_of_le h

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a - a = 0

Tactic:
sub_self

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 0 = 0
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Tactic:
obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI
  rcases mem_span_insert.1
      (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
        (subset_span (mem_insert _ _))) with
    ⟨y, z, hz, hy⟩
  refine ⟨y, z, ?_, hy.symm⟩
  rwa [← span_eq I]

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
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
⊢ ∀ (a₁ : R) (a₂ : ι → R) (b₁ : R) (b₂ : ι → R),
    (Submodule.quotientRel I) a₁ b₁ →
      (Submodule.quotientRel (pi fun x ↦ I)) a₂ b₂ → Submodule.Quotient.mk (a₁ • a₂) = Submodule.Quotient.mk (b₁ • b₂)

Tactic:
intro c₁ m₁ c₂ m₂ hc hm

Goal state after:
ι : 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
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : (Submodule.quotientRel I) c₁ c₂
hm : (Submodule.quotientRel (pi fun x ↦ I)) m₁ m₂
⊢ Submodule.Quotient.mk (c₁ • m₁) = Submodule.Quotient.mk (c₂ • m₂)
Module: Mathlib.Algebra.Order.SuccPred.PartialSups

Goal state before:
pp: ι : Type u_2
inst✝⁴ : LinearOrder ι
α : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrder ι
inst✝¹ : SuccOrder ι
inst✝ : OrderBot ι
f : ι → α
i j : ι
x✝ : ⊥ ≤ j
h : (partialSups f) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) j
this :
  (partialSups (f ∘ Order.succ)) (Order.succ j) = (partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)
⊢ (partialSups f) (Order.succ (Order.succ j)) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) (Order.succ j)

Tactic:
simp [this, h, sup_assoc]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_5
inst✝ : Unique α
m : M
⊢ (finsuppUnique R M α).symm m = single default m

Tactic:
by
  ext; simp [LinearEquiv.finsuppUnique, Equiv.funUnique, single, Pi.single,
    equivFunOnFinite, Function.update]

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
⊢ ∀ (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets

Tactic:
a

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
⊢ x ∈ (f a).sets → ∀ (x_1 : ι), y ∈ (f x_1).sets → ∃ i, x ∩ y ∈ (f i).sets
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
l : Filter α
t : Set β
⊢ t ∈ map f (l ⊓ 𝓟 (f ⁻¹' s)) ↔ t ∈ map f l ⊓ 𝓟 s

Tactic:
by simp only [mem_map', mem_inf_principal, mem_ofPred_eq, mem_preimage]

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

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
⊢ Disjoint f (𝓟 s) ↔ sᶜ ∈ f

Tactic:
by
  rw [mem_iff_inf_principal_compl, compl_compl, disjoint_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ Tendsto m (𝓟 s) (𝓟 t) ↔ MapsTo m s t

Tactic:
tendsto_principal_principal,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ (∀ a ∈ s, m a ∈ t) ↔ MapsTo m s t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter β
x : α
this : (∀ (A : Set α), ∀ B ∈ F, f ⁻¹' B ⊆ A → x ∈ A) ↔ ∀ B ∈ F, f x ∈ B
⊢ x ∈ ⋂₀ (comap f F).sets ↔ x ∈ ⋂ U ∈ F, f ⁻¹' U

Tactic:
simp only [mem_sInter, mem_iInter, Filter.mem_sets, mem_comap, this, and_imp,
      mem_preimage, exists_imp]

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

Goal state before:
pp: case refine_1.hx
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure x ∈ Iic (𝓟 s)

Tactic:
rwa [mem_Iic, pure_le_principal]

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

Goal state before:
pp: case refine_1.hy
α : Type u_1
β : Type u_2
s : Set α
m : α → β
hm : InjOn (map m) (Iic (𝓟 s))
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : map m (pure x) = map m (pure y)
⊢ pure y ∈ Iic (𝓟 s)

Tactic:
rwa [mem_Iic, pure_le_principal]

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e✝ e : α ≃ β
inst✝ : Mul β
x✝ : Mul α := e.mul
x y : α
⊢ e.toFun (x * y) = e.toFun x * e.toFun y

Tactic:
simp [mul_def]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Module.Finite A B ↔ Module.Finite A B

Tactic:
toAlgebra_algebraMap

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Module.Finite A B ↔ Module.Finite A B
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case h
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsCofinal {t}
⊢ IsTop t

Tactic:
isCofinal_singleton_iff

Goal state after:
case h
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsTop t
⊢ IsTop t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ IsCofinal {t}

Tactic:
isCofinal_singleton_iff

Goal state after:
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ IsTop t
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
a b : α
hb : f a ≤ f b
⊢ ∃ y ∈ range g, a ≤ y

Tactic:
obtain ⟨c, hc, hc'⟩ := hs (f b)

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ ∃ y ∈ range g, a ≤ y
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s

Tactic:
simp_rw [DirSupClosedOn, DirSupInaccOn, ← not_disjoint_iff_nonempty_inter]

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ (∀ ⦃d : Set α⦄, d ∈ D → d ⊆ sᶜ → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ sᶜ) ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ¬Disjoint d s
Module: Mathlib.Algebra.Order.Module.Defs

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

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

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t

Tactic:
a

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
⊢ IsLUB d a → a ∈ s ∪ t
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
⊢ ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
a

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
⊢ IsLUB d a → a ∈ s → (d ∩ s).Nonempty
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ ¬IsMin (f a)

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
⊢ False

Tactic:
· obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin
    exact not_isMin_iff.2 ⟨_, hf.strictMono hb⟩

Goal state after:
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
⊢ False
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr.isMin
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsMin a
⊢ f ⊥ = g ⊥

Tactic:
H₁

Goal state after:
case mpr.isMin
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
H₁ : f ⊥ = g ⊥
H₂ : ∀ (a : α), f a = g a → f (succ a) = g (succ a)
a : α
ha : IsMin a
⊢ g ⊥ = g ⊥
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ ⦃a : α⦄, IsLUB s a → a ∈ range f

Tactic:
a

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
⊢ IsLUB s a → a ∈ range f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ sSup (range fun a ↦ f ↑a ⋯) = sSup (o.brange f)

Tactic:
brange,

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ sSup (range fun a ↦ f ↑a ⋯) = sSup {a | ∃ i, ∃ (hi : i < o), f i hi = a}
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ succ (iSup f) ≤ lsub f ↔ ∃ i, f i = iSup f

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · by_contra! hf
    have := forall_congr' fun i ↦ (Ordinal.le_iSup f i).lt_iff_ne.symm
    exact (succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))
  rintro ⟨_, hf⟩
  rw [succ_le_iff, ← hf]
  exact lt_lsub _ _

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

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
⊢ a * ↑n + a = a * (↑n + 1)

Tactic:
mul_add_one

Goal state after:
n : ℕ
a : Ordinal.{u_4}
⊢ a * ↑n + a = a * ↑n + a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)

Tactic:
by
  rw [lsub_eq_blsub', lsub_eq_blsub']

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

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

Tactic:
have H := mul_ne_zero hc.ne_zero hd
    apply le_antisymm
    · rw [← lt_succ_iff, ← lt_mul_iff_div_lt H, mul_assoc]
      · grw [hc, ← mul_succ]
        gcongr
        rw [succ_le_iff]
        exact lt_mul_succ_div b hd
    · grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a / b = 1 ↔ b ≤ a ∧ a < b * 2

Tactic:
by
  rw [div_eq_iff' one_ne_zero, mul_one, one_add_one_eq_two]

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

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 = 0 - 1

Tactic:
Nat.zero_sub

Goal state after:
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : Bool
n : ℕ
hn : n ≠ 0
⊢ log 2 (bit b n) = log 2 n + 1

Tactic:
by
  rw [← log_div_mul_self, bit_div_two, log_mul_base Nat.one_lt_two hn]

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

Goal state before:
pp: m n : ℕ
⊢ ↑m * ↑n + ↑m = ↑m * (↑n + 1)

Tactic:
mul_add_one

Goal state after:
m n : ℕ
⊢ ↑m * ↑n + ↑m = ↑m * ↑n + ↑m
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
tsub_eq_zero_iff_le.2 h,

Goal state after:
case inl
m n : ℕ
h : m ≤ n
⊢ ↑0 = ↑m - ↑n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case1.inl
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:
← Nat.add_one_le_iff

Goal state after:
case case1.inl
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 + 1 ≤ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
obtain rfl | rfl := le_one_iff.1 h

Goal state after:
case inl
x : Ordinal.{u_1}
h : 0 ≤ 1
⊢ log 0 x = 0

case inr
x : Ordinal.{u_1}
h : 1 ≤ 1
⊢ log 1 x = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Tactic:
exact (opow_le_iff_le_log hb hx).1 h

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

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card + 1

Tactic:
exact hc.trans ha

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

Goal state before:
pp: case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
⊢ IsPrincipal op o

Tactic:
a

Goal state after:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
a : Ordinal.{u}
⊢ ∀ ⦃b : Ordinal.{u}⦄, a < o → b < o → op a b < o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
⊢ ∃ o, derivFamily f o = a

Tactic:
suffices ∀ (o), a ≤ derivFamily f o → ∃ o, derivFamily f o = a from
      this a (isNormal_derivFamily _).strictMono.le_apply
    intro o
    induction o using limitRecOn with
    | zero =>
      intro h₁
      refine ⟨0, le_antisymm ?_ h₁⟩
      rw [derivFamily_zero]
      exact nfpFamily_le_fp (fun i => (H i).monotone) zero_le ha
    | add_one o IH =>
      intro h₁
      rcases le_or_gt a (derivFamily f o) with h | h
      · exact IH h
      refine ⟨o + 1, le_antisymm ?_ h₁⟩
      rw [derivFamily_add_one]
      exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha
    | limit o l IH =>
      intro h₁
      rcases eq_or_lt_of_le h₁ with h | h
      · exact ⟨_, h.symm⟩
      rw [derivFamily_limit _ l, ← not_le, Ordinal.iSup_le_iff, not_forall] at h
      obtain ⟨o', h⟩ := h
      exact IH o' o'.2 (le_of_not_ge h)

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

Goal state before:
pp: case pos.inr
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
hs' : s.Nonempty
x y : Ordinal.{u_1}
⊢ ∀ x_1 ∈ s, x < x_1 → ∀ x_2 ∈ s, y < x_2 → ∃ b ∈ s, op x y < b

Tactic:
a

Goal state after:
case pos.inr
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
hs' : s.Nonempty
x y a : Ordinal.{u_1}
⊢ a ∈ s → x < a → ∀ x_1 ∈ s, y < x_1 → ∃ b ∈ s, op x y < b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b

Tactic:
dvd_iff_mod_eq_zero

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case succ
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
h : a * ↑n < o
⊢ a * (↑n + 1) < o

Tactic:
mul_add_one

Goal state after:
case succ
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
n : ℕ
h : a * ↑n < o
⊢ a * ↑n + a < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a * b ≤ max a b

Tactic:
convert! mul_le_mul' (le_max_left a b) (le_max_right a b) using 1
  rw [mul_eq_self]
  exact h.trans (le_max_left a b)

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

Goal state before:
pp: f : Ordinal.{u_1} → Cardinal.{u_1}
hf : StrictMono f
o : Ordinal.{u_1}
⊢ preAleph o ≤ f o

Tactic:
simpa using (hf.comp preAleph.symm.strictMono).id_le (preAleph o)

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

Goal state before:
pp: case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : #↑s < (lift.{u + 1, u} (⨆ i, ↑(f i) + 1)).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False

Tactic:
rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift,
      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type,
      Cardinal.lift_lift, Cardinal.lift_lt] at ha

Goal state after:
case a
s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : #↑s < Order.cof ↑s
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r ↑((enum r') ⟨i, x✝¹⟩) ↑((enum r') ⟨j, h⟩)

Tactic:
change r (hrr'.1 _) (hrr'.1 _)

Goal state after:
case refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r (hrr'.toEmbedding ((enum r') ⟨i, x✝¹⟩)) (hrr'.toEmbedding ((enum r') ⟨j, h⟩))
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
apply mk_compl_eq_mk_compl_finite_lift.{u, u}
  <;> rwa [lift_inj]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∀ (x : ↥W), φ ↑x = 0 x) ↔ ∀ w ∈ W, φ w = 0

Tactic:
Subtype.forall,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∀ (a : M) (b : a ∈ W), φ a = 0 ⟨a, b⟩) ↔ ∀ w ∈ W, φ w = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
suffices LinearMap.ker (lsum ℕ fun i => (p i).subtype) = ⊥ by
    -- Lean can't find this without our help
    let thisI : AddCommGroup (Π₀ i, p i) := inferInstance
    rw [LinearMap.ker_eq_bot] at this
    exact this

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥

Tactic:
rw [LinearMap.ker_eq_bot']

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ ∀ (m : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) m = 0 → m = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
⊢ Function.Surjective ⇑((lsum ℕ) fun i ↦ (p i).subtype)

Tactic:
rwa [← LinearMap.range_eq_top, ← Submodule.iSup_eq_range_dfinsupp_lsum]

Goal state after: