mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
⊢ (f.coprod g).ker = f.ker.prod g.ker

Tactic:
by
  apply le_antisymm _ (ker_prod_ker_le_ker_coprod f g)
  rintro ⟨y, z⟩ h
  simp only [mem_ker, mem_prod, coprod_apply] at h ⊢
  have : f y ∈ (range f) ⊓ (range g) := by
    simp only [true_and, mem_range, mem_inf, exists_apply_eq_apply]
    use -z
    rwa [eq_comm, map_neg, ← sub_eq_zero, sub_neg_eq_add]
  rw [hd.eq_bot, mem_bot] at this
  rw [this] at h
  simpa [this] using h

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (m : R) (x : α ⊕ β → M),
    (Equiv.sumArrowEquivProdArrow α β M).toFun (m • x) = (RingHom.id R) m • (Equiv.sumArrowEquivProdArrow α β M).toFun x

Tactic:
by
      intro r f
      ext <;> rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp
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₂)
⊢ p₁.prod p₂ ≤ q → map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q

pp: case mpr
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₂)
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q

Tactic:
· intro h
    constructor
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨hx, zero_mem p₂⟩
    · rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨zero_mem p₁, hx⟩

Goal state after:
case mpr
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₂)
⊢ map (inl R M M₂) p₁ ≤ q ∧ map (inr R M M₂) p₂ ≤ q → p₁.prod p₂ ≤ q
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)

pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)

Tactic:
· change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]

Goal state after:
α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x

Tactic:
Ico_eq_cons_Ioo h,

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ cons a (Ioo a b) ⋯, f x
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

Tactic:
rw [Ioc_eq_cons_Ioo h, prod_cons]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁵ : CommMonoid M
a b : α
inst✝⁴ : LinearOrder α
inst✝³ : LocallyFiniteOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
hab : a ≤ b
f : α → M
⊢ (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x

Tactic:
by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[(toZ i0 i).toNat] i0 = i

Tactic:
rw [toZ_of_ge hi, Int.toNat_natCast]
  exact Nat.find_spec (exists_succ_iterate_of_le hi)

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iic x) ≤ #(Iio i)

Tactic:
refine card_le_card (fun r hr ↦ ?_)

Goal state after:
case succ.inr.hbc
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
r : ι
hr : r ∈ Iic x
⊢ r ∈ Iio i
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ ∏ k ∈ Ico a (b + 1), f k = (∏ k ∈ Ico a b, f k) * f b

Tactic:
by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ x ∈ Ico (0 + m) (n - m + m), f x

Tactic:
zero_add,

Goal state after:
case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ x ∈ Ico m (n - m + m), f x
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 : p * q + (q * p - p) = p
⊢ Commute p q

Tactic:
add_sub

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.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
hne : M ≠ M'
⊢ M ⊔ M' = ⊤

Tactic:
contrapose! hne with h
  exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)

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

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Tactic:
by
        rw [range_eq_Ico, sum_Ico_reflect _ _ (by lia)]
        congr
        lia

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

Goal state before:
pp: case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = Ico (0 + k) (n + 1 + k)

Tactic:
zero_add,

Goal state after:
case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = Ico k (n + 1 + k)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ ¬P = ⊥ → ∃ p, Prime p ∧ P = span {p}

Tactic:
← forall_congr' isPrime_iff_of_isPrincipalIdealRing,

Goal state after:
α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P ≠ ⊥ → P.IsPrime
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
⊢ ∀ (b : (ι → R) ⧸ pi fun x ↦ I), 1 • b = b

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
ι : 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
b✝ : (ι → R) ⧸ pi fun x ↦ I
a : ι → R
⊢ 1 • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a = Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

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

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a✝¹ b : R
inst✝ : I.IsTwoSided
a✝ : R ⧸ I
a : R
⊢ Quot.mk (⇑(Submodule.quotientRel I)) a • 0 = 0
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
⊢ ∀ (x : (ι → R) ⧸ pi fun x ↦ I), 0 • x = 0

Tactic:
rintro ⟨a⟩

Goal state after:
case mk
ι : 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
x✝ : (ι → R) ⧸ pi fun x ↦ I
a : ι → R
⊢ 0 • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a = 0
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
t : Set α
⊢ t ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ t

Tactic:
simp only [h.mem_filter_iff]

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

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

Tactic:
by
  rw [← principal_univ, ← biSup_pure_eq_principal, iSup_univ]

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:
by
  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
ι : Sort x
f : ι → Filter α
s : Set α
hs : s ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
⊢ p s

Tactic:
by
  have p_of_f : ∀ i, ∀ s ∈ f i, p s := fun i s hs ↦ by simpa using ins hs uni
  let q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ t', t ⊆ t' → p t'
  have q_mono : Monotone q := fun a b hab ha ↦
    ⟨mem_of_superset ha.1 hab, fun t hbt ↦ ha.2 _ (hab.trans hbt)⟩
  have A : ∀ i, ∀ s ∈ f i, ∀ t, q t → q (s ∩ t) := fun i s hs t ht ↦ by
    use inter_mem (mem_iInf_of_mem _ hs) ht.1
    intro u hu
    have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
    rw [this]
    exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)
  have B : ∀ s t, q s → q t → q (s ∩ t) := fun s t hqs hqt ↦ by
    let 𝓕 : Filter α :=
    { sets := {s | ∀ t, q t → q (s ∩ t)}
      univ_sets := by simp
      sets_of_superset ha hab t ht := q_mono (inter_subset_inter_left _ hab) (ha t ht)
      inter_sets ha hb t ht := by simpa [inter_assoc] using ha _ (hb _ ht) }
    exact (le_iInf_iff.mpr A : 𝓕 ≤ iInf f) hqs.1 _ hqt
  have C : ∀ i, ∀ s ∈ f i, q s := fun i s hs ↦
    ⟨mem_iInf_of_mem _ hs, fun t hst ↦ p_of_f _ _ (mem_of_superset hs hst)⟩
  let 𝓖 : Filter α :=
  { sets := {t | q t}
    univ_sets := by simpa [q] using uni
    sets_of_superset ha hab :=
      ⟨mem_of_superset ha.1 hab, fun t hbt ↦ ha.2 _ (hab.trans hbt)⟩
    inter_sets := B _ _ }
  have : 𝓖 ≤ iInf f := le_iInf_iff.mpr C
  exact (this hs).2 s subset_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
b : β
⊢ comap m (pure b) = 𝓟 (m ⁻¹' {b})

Tactic:
← principal_singleton,

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
b : β
⊢ comap m (𝓟 {b}) = 𝓟 (m ⁻¹' {b})
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ f ⊓ 𝓟 (range m) ≤ map m (comap m f)

Tactic:
rintro t' ⟨t, ht, sub⟩

Goal state after:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
t' t : Set β
ht : t ∈ f
sub : m ⁻¹' t ⊆ m ⁻¹' t'
⊢ t' ∈ f ⊓ 𝓟 (range m)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
⊢ ∃ t₁ ∈ 𝓟 s, ∃ t₂ ∈ 𝓟 t, s ∩ t = t₁ ∩ t₂

Tactic:
exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩

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

Goal state before:
pp: α : Type u
s : Set α
l : Filter α
⊢ s =ᶠ[l] univ ↔ s ∈ l

Tactic:
simp [eventuallyEq_set]

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

Goal state before:
pp: α : Type u_1
f : Filter α
a : α
⊢ f ≤ pure a ↔ {a} ∈ f

Tactic:
← principal_singleton,

Goal state after:
α : Type u_1
f : Filter α
a : α
⊢ f ≤ 𝓟 {a} ↔ {a} ∈ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
⊢ s.seq t ∈ (map (fun b a ↦ (a, b)) g).seq f

Tactic:
· rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
    grw [← hs]
    rw [Set.prod_image_seq_comm]
    exact seq_mem_seq (image_mem_map ht) hu

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

Goal state before:
pp: P : ℕ → ℕ → Prop
h : ∀ (n a : ℕ), ∃ b > a, P n b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

Tactic:
choose u hu hu' using h

Goal state after:
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
Module: Mathlib.Order.Filter.AtTopBot.Basic

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

Tactic:
by
  rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddMonoid M
inst✝ : IsAddTorsionFree M
n : ℕ
x : M
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0

Tactic:
simpa using (nsmul_right_injective hx.1).ne hx.2

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 = a
⊢ b₁ < b₂

pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂

Tactic:
· simp [← ha] at h

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
⊢ ∃ x, IsTop x

pp: case refine_2
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ cof α = 1

Tactic:
· obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
    rw [h, mk_set_eq_one_iff] at hs'
    obtain ⟨t, rfl⟩ := hs'
    use t
    rwa [isCofinal_singleton_iff] at hs

Goal state after:
case refine_2
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ cof α = 1
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
by
  obtain ⟨a, ha₀, rfl⟩ := exists_nonneg_add_of_le ha
  rw [add_smul, add_smul, add_left_comm]
  gcongr

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case mpr.succ
α : 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 : ¬IsMax a
IH : f a = g a
⊢ f (succ a) = g (succ a)

Tactic:
| succ a ha IH =>

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (#α).ord = (cof α).ord

Tactic:
cof_eq_cardinalMk

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (#α).ord = (#α).ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ IsSuccPrelimit (lift.{u, v} o)

Tactic:
isSuccPrelimit_lift

Goal state after:
case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
⊢ range (familyOfBFamily' r ho f) = o.brange f

Tactic:
refine Set.ext fun a => ⟨?_, ?_⟩
  · rintro ⟨b, rfl⟩
    apply mem_brange_self
  · rintro ⟨i, hi, rfl⟩
    exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩

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

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

Tactic:
exact (mul_div_le a c).trans h

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ (typein r).toRelEmbedding (⋯.min sᶜ h) ≤ (#↑s).ord

Tactic:
Cardinal.le_ord_iff_card_le_of_lt_aleph0 _ hfin.lt_aleph0,

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
hfin : s.Finite
h : sᶜ.Nonempty
⊢ ((typein r).toRelEmbedding (⋯.min sᶜ h)).card ≤ #↑s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
by
  rw [← IsNormal.bsup.{u, u, v} H (fun x _ => x) h.ne_bot, bsup_id_limit fun _ ↦ h.succ_lt]

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

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

Tactic:
refine ⟨fun h ↦ ?_, by grind [isSuccLimit_add]⟩

Goal state after:
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ 0 + 1 ≤ log b o

Tactic:
zero_add,

Goal state after:
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ 1 ≤ log b o
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
zero_add,

Goal state after:
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ log b o < 1
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ deriv 0 a = a

Tactic:
deriv_zero,

Goal state after:
a : Ordinal.{u_1}
⊢ id a = a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c ≤ c * c

Tactic:
simpa using mul_le_mul_right (one_le_aleph0.trans hc) c

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

Goal state before:
pp: case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ a ≠ 0

Tactic:
← pos_iff_ne_zero

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

Goal state before:
pp: a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}), deriv (fun x ↦ a * x) a_1 = a ^ ω * a_1 → deriv (fun x ↦ a * x) (succ a_1) = a ^ ω * succ a_1

Tactic:
refine ⟨?_, fun c h => ?_⟩

Goal state after:
case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x ↦ a * x) ⊥ = a ^ ω * ⊥

case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ deriv (fun x ↦ a * x) (succ c) = a ^ ω * succ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩

Goal state after:
case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b

case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : a ≠ 0
⊢ (fun x1 x2 ↦ x1 * x2) a b < o

Tactic:
← pos_iff_ne_zero

Goal state after:
case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x1 x2 ↦ x1 * x2) a b < o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof.ord.cof = o.cof

Tactic:
by
  simpa using Order.cof_ord_cof o.ToType

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

Goal state before:
pp: a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ (⨆ i, f i + 1).cof = a.cof

Tactic:
cof_iSup_Iio_add_one hf

Goal state after:
a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
ha : IsSuccPrelimit a
⊢ a.cof = a.cof
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ ord 0

Tactic:
ord_zero

Goal state after:
f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}
⊢ 0 ≤ 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : ¬α ≤ β
⊢ ¬α + γ ≤ β + γ

Tactic:
rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢

Goal state after:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ (a ^ b).card = max a.card b.card

Tactic:
apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _) <;> apply card_le_card
  · exact left_le_opow a hb
  · exact right_le_opow b (one_lt_omega0.trans_le ha)

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ o.card

Tactic:
← o.card.lift_id

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card