mathlib-initiative/mathlib-tactics huggingface dataset:
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 < Cardinal.lift.{u + 1, u} (⨆ i, ↑(f i) + 1).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False

Tactic:
← Cardinal.lift_lt.{_, u + 2},

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 : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u + 2, u + 1} (Cardinal.lift.{u + 1, u} (⨆ i, ↑(f i) + 1).cof)
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
· rintro rfl
    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
    exact ha.not_ge (cof_le_cardinalMk _)

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ iSup f < c

Tactic:
apply lift_iSup_lt_of_lt_cof _ hf

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} c).cof
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
h : 1 < a
⊢ max a.card ω.card = max ℵ₀ a.card

Tactic:
card_omega0,

Goal state after:
a : Ordinal.{u_1}
h : 1 < a
⊢ max a.card ℵ₀ = max ℵ₀ a.card
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
θ : Cardinal.{u}
hθ : θ ≤ #β
h₁ : ℵ₀ ≤ θ
h₂ : #α < θ.ord.cof
⊢ ∃ a, θ ≤ #↑(f ⁻¹' {a})

Tactic:
by
  rcases le_mk_iff_exists_set.1 hθ with ⟨s, rfl⟩
  obtain ⟨a, ha⟩ := infinite_pigeonhole (f ∘ Subtype.val : s → α) h₁ h₂
  use a; rw [← ha, @preimage_comp _ _ _ Subtype.val f]
  exact mk_preimage_of_injective _ _ Subtype.val_injective

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
by
  rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']

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

Goal state before:
pp: α β : Type u
⊢ #(α ↪ β) = 0 ↔ #β < #α

Tactic:
mk_embedding_eq_zero_iff_lift_lt,

Goal state after:
α β : Type u
⊢ lift.{u, u} #β < lift.{u, u} #α ↔ #β < #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ Classical.choose this = ⟨x, h⟩

Tactic:
apply g.2

Goal state after:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ g.toFun (Classical.choose this) = g.toFun ⟨x, h⟩
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω.card * ω.card < c

Tactic:
card_omega0,

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ * ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ⇑f)ᶜ
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h✝ : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
g : ↑sᶜ ≃ ↑(range ⇑f)ᶜ
h : α ≃ β := (Set.sumCompl s).symm.trans (((ofInjective ⇑f ⋯).sumCongr g).trans (Set.sumCompl (range ⇑f)))
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
l : { l // ∀ (i : ι), i ∈ l }
⊢ ∀ ⦃a b : (i : ι) → i ∈ ↑l → α i⦄, a ≈ b → (fun i ↦ a i ⋯) ≈ fun i ↦ b i ⋯

Tactic:
exact fun _ _ h i ↦ h i _

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case neg
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∉ x.support
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = 0

Tactic:
mk_of_notMem mem,

Goal state after:
case neg
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∉ x.support
⊢ (f i) 0 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
hi0 : g i = 0
hj0 : g j = 0
⊢ ∀ i ∈ t, g i = 0

Tactic:
exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
x : M
⊢ x = eval [(1, x)]

Tactic:
simp [eval]

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 : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ u • s • x + u • t • y = 0

Tactic:
smul_comm u s,

Goal state after:
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s • u • x + u • t • y = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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

Tactic:
apply linearIndepOn_iUnion_of_directed

Goal state after:
case hs
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ ⋃ i_1 ∈ i, f i_1

case h
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ ∀ (i : Finset ι), LinearIndepOn R id (⋃ i_1 ∈ i, f i_1)
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ s, Injective (f a)
hs : ((fun a ↦ image (f a) t) '' ↑s).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f s t)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s _ ih => ?_

Goal state after:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : (∀ a ∈ s, Injective (f a)) → ((fun a ↦ image (f a) t) '' ↑s).PairwiseDisjoint id → #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f (insert a s) t)
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
have hD : 1 ∈ D := mem_map.mpr ⟨b, hb, mul_inv_cancel b⟩

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu : UniqueMul A B a b
C : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ X.coeff n = 0

Tactic:
coeff_X,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 1
⊢ (if 1 = n then 1 else 0) = 0
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ ((monomial n) a).support = {n}

Tactic:
← ofFinsupp_single,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
h : a ≠ 0
⊢ { toFinsupp := single n a }.support = {n}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ ((monomial n) a).support ⊆ {n}

Tactic:
← ofFinsupp_single,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
⊢ { toFinsupp := single n a }.support ⊆ {n}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.support = {1}

Tactic:
by
  rw [← pow_one X, support_X_pow 1]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hC : 1 ∈ C
hD✝ : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1✝ : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hD : 1 < #D
d : G
hd : d ∈ D
hd1 : d ≠ 1
⊢ d = 1

Tactic:
simpa using hu ⟨_, ⟨_, hd, rfl⟩, _, hC, rfl⟩ ⟨_, hd, _, ⟨_, hC, rfl⟩, rfl⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R fun ix ↦ single ix.fst (f ix.fst ix.snd)

Tactic:
convert!
    (DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn

Goal state after:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
x✝ : (i : ι) × φ i
⊢ single x✝.fst (f x✝.fst x✝.snd) =
    (⇑↑(finsuppLequivDFinsupp R).symm ∘ fun ix ↦ DFinsupp.single ix.fst (f ix.fst ix.snd)) x✝
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
H : x ∈ Set.range f
⊢ g' (g x) = 1

Tactic:
mulExact x |>.mpr H,

Goal state after:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : One P
inst✝ : One P'
mulExact : MulExact f g
inj : Injective g'
h0 : g' 1 = 1
x : N
H : x ∈ Set.range f
⊢ g' 1 = 1
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ Function.Surjective ⇑(f.prod g)

Tactic:
by
      rw [← range_eq_top]
      simp [range_prod_eq hfg.sup_eq_top, *]

Goal state after:
Module: Mathlib.Data.Rel

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

Tactic:
Set.image_swap_prod,

Goal state after:
α : Type u_1
s₁ s₂ : Set α
R : SetRel α α
inst✝ : R.IsSymm
⊢ s₂ ×ˢ s₁ ⊆ R ↔ s₂ ×ˢ s₁ ⊆ Prod.swap ⁻¹' R
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
motive : RelSeries r → Sort u_3
singleton : (x : α) → motive (RelSeries.singleton r x)
cons : (p : RelSeries r) → (x : α) → (hx : (x, p.head) ∈ r) → motive p → motive (p.cons x hx)
d : ℕ
hd : (p : RelSeries r) → p.length = d → motive p
p : RelSeries r
heq : p.length = d + 1
⊢ motive p

Tactic:
have lq := p.tail_length (heq ▸ d.zero_ne_add_one.symm)
      nth_rw 3 [heq] at lq
      convert!
        cons (p.tail (heq ▸ d.zero_ne_add_one.symm)) p.head (p.3 ⟨0, heq ▸ d.zero_lt_succ⟩)
          (hd _ lq)
      exact (p.cons_self_tail (heq ▸ d.zero_ne_add_one.symm)).symm

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l : RelSeries r
⊢ ∃ y, l.length < y.length

Tactic:
obtain ⟨l', hl'⟩ := H (l.length + 1)

Goal state after:
case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
H : ∀ (n : ℕ), ∃ x, x.length = n
l l' : RelSeries r
hl' : l'.length = l.length + 1
⊢ ∃ y, l.length < y.length
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin (↑lf + 1)), f i = g i
⊢ f = g

Tactic:
funext_iff

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin (↑lf + 1)), f i = g i
⊢ ∀ (x : Fin (↑lf + 1)), f x = g x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x = ⨆ y, ⨆ (_ : y < x), height y + 1

Tactic:
apply le_antisymm
  · apply height_le
    intro p hp
    cases hlen : p.length with
    | zero => simp
    | succ n =>
      apply le_iSup_of_le p.eraseLast.last
      apply le_iSup_of_le (by rw [← hp]; exact p.eraseLast_last_rel_last (by lia))
      rw [height_add_const]
      apply le_iSup₂_of_le p.eraseLast (by rfl) (by simp [hlen])
  · apply iSup₂_le; intro y hyx
    rw [height_add_const]
    apply iSup₂_le; intro p hp
    apply le_iSup₂_of_le (p.snoc x (hp ▸ hyx)) (by simp) (by simp)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case pos.succ
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : height a < ⊤
n✝ : ℕ
hn : n = n✝ + 1
⊢ height a = ↑(n✝ + 1) ↔ Minimal (fun y ↦ ↑(n✝ + 1) ≤ height y) a

Tactic:
simp [minimal_iff_forall_lt, height_eq_coe_add_one_iff, ENat.add_one_le_iff,
        coe_lt_height_iff, *]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ height a = ↑n ↔ Minimal (fun y ↦ ↑n ≤ height y) a

Tactic:
suffices ∃ x < a, ↑n ≤ height x by
      simp_all [minimal_iff_forall_lt]

Goal state after:
case neg
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hfin : ⊤ ≤ height a
⊢ ∃ x < a, ↑n ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x

Tactic:
rintro ⟨y, z, hzy, hyx⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : Preorder α
x y z : α
hzy : z < y
hyx : y < x
⊢ 2 ≤ height x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
i : Fin 1
⊢ (![x, y] i.castSucc, ![x, y] i.succ) ∈ {(a, b) | a < b}

Tactic:
by obtain rfl := Subsingleton.elim i 0; simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ ↑(LTSeries.longestOf α).length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ RelSeries.last (LTSeries.longestOf α)), ↑p.length

Tactic:
exact le_iSup_iff.mpr <| fun _ h ↦ iSup_le_iff.mp (h _) le_rfl

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

Goal state before:
pp: R : Type u_1
R' : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : Monoid R'
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : DistribMulAction R' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R' M
x✝ : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 1 • x = x
ihy : 1 • y = y
⊢ 1 • (x + y) = x + y

Tactic:
rw [TensorProduct.smul_add, ihx, ihy]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ↑(coheight ⊥) = krullDim α

Tactic:
rw [← krullDim_orderDual]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ↑(coheight ⊥) = krullDim αᵒᵈ
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y ↦ ↑y
⊢ ↑p.length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length

Tactic:
← LTSeries.map_length p (fun x ↦ x.1) mono,

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries ↑(Set.Iic x)
i✝ : RelSeries.last p ≤ ⊤
mono : StrictMono fun y ↦ ↑y
⊢ ↑(p.map (fun x_1 ↦ ↑x_1) mono).length ≤ ⨆ p, ⨆ (_ : RelSeries.last p ≤ x), ↑p.length
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
m : M
hm : ∃ b, m + b = 0
n : N
b : M
eq : m + b = 0
⊢ m ⊗ₜ[R] n + b ⊗ₜ[R] n = 0

Tactic:
by rw [← add_tmul, eq, zero_tmul]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ ↑p.length ≤ height ↑x

Tactic:
let p' := p.map _ WithTop.coe_strictMono

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries α
hlast : RelSeries.last p = x
p' : LTSeries (WithTop α) := p.map (fun a ↦ ↑a) ⋯
⊢ ↑p.length ≤ height ↑x
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
| krullDim (WithBot α)

Tactic:
rw [← krullDim_orderDual]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
| krullDim (WithBot α)ᵒᵈ
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
| krullDim α + 1

Tactic:
rw [← krullDim_orderDual]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
| krullDim αᵒᵈ + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: ⊢ krullDim ℕ∞ = ⊤

Tactic:
by
  change (krullDim (WithTop ℕ) = ⊤)
  simp [← WithBot.coe_top, ← WithBot.coe_one, ← WithBot.coe_add]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Monoid R
r : R
inst✝ : IsMulTorsionFree R
hx : IsLeftRegular r
hx' : r ≠ 1
n m : ℕ
hnm : (fun n ↦ r ^ n) n = (fun n ↦ r ^ n) m
main : ∀ {n m : ℕ}, n ≤ m → r ^ n = r ^ m → n = m
h : m ≤ n
⊢ n = m

Tactic:
exact (main h hnm.symm).symm

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝ : Semiring α
h : ∀ (a : α), a + a = a
a b : α
hab : a + b = b
hba : b + a = a
⊢ a = b

Tactic:
by rwa [← hba, add_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : c * a ≤ c
⊢ b * a∗ ≤ c

Tactic:
hb,

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : c * a ≤ c
⊢ c * a∗ ≤ c
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
⊢ a∗ * b ≤ c

Tactic:
hb,

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a b c : α
hb : b ≤ c
ha : a * c ≤ c
⊢ a∗ * c ≤ c
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
r : R
y : M
hy : y ∈ a
⊢ r • y ∈ a

Tactic:
exact smul_mem _ _ hy

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
y : M
hy : y ∈ a
r : R
⊢ r • y ∈ a

Tactic:
exact smul_mem _ _ hy

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)

Tactic:
exact h.add_mul_left_right z

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (x + 1) y

Tactic:
obtain ⟨z, rfl⟩ := h
  rw [mul_add_left_left_iff]
  exact isCoprime_one_left

Goal state after:
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
h_eq : ¬val i = val j
⊢ val i ≤ val j ↔ ↑⋯.choose ≤ ↑⋯.choose

Tactic:
generalize_proofs _ hi hj

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