mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Set α
x✝ : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : s.Finite
⊢ 1 < s.ncard

Tactic:
← Set.finite_coe_iff

Goal state after:
case refine_2
α : Type u_1
s : Set α
x✝ : s.Nontrivial ∧ s.Finite
hs_nontrivial : s.Nontrivial
hs_finite : Finite ↑s
⊢ 1 < s.ncard
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ f.range.mkQ ∘ₗ g.ker.subtype = 0

Tactic:
← range_le_ker_iff,

Goal state after:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ g.ker.subtype.range ≤ f.range.mkQ.ker
Module: Mathlib.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : SuccOrder α
a : α
ha : ¬IsMax a
⊢ ↑(Ici (succ a)) = ↑(Ioi a)

Tactic:
by simpa using Set.Ici_succ_eq_Ioi_of_not_isMax ha

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
h : f ≤ ⇑g
⊢ partialSups f ≤ g

Tactic:
convert! partialSups_mono h

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
g : ι →o α
h : f ≤ ⇑g
⊢ g = partialSups ⇑g
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
this : Iic ⊥ = {⊥}
⊢ (Iic ⊥).sup' ⋯ f = f ⊥

Tactic:
simp only [this, sup'_singleton]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : PartialOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
this : Iic ⊥ = {⊥}
⊢ (Iic ⊥).sup' ⋯ f = f ⊥

Tactic:
by simp only [this, sup'_singleton]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Icc a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Icc a b) = image (fun h ↦ c + h) (Icc a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ico a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Ico a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ico a b) = image (fun h ↦ c + h) (Ico a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioc a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Ioc a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioc a b) = image (fun h ↦ c + h) (Ioc a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioo a b) = image (⇑{ toFun := fun h ↦ c + h, inj' := ⋯ }) (Ioo a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ c + x) (Ioo a b) = image (fun h ↦ c + h) (Ioo a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Icc a b) = image (⇑{ toFun := fun h ↦ h + c, inj' := ⋯ }) (Icc a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Icc a b) = image (fun h ↦ h + c) (Icc a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ico a b) = image (⇑{ toFun := fun h ↦ h + c, inj' := ⋯ }) (Ico a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ico a b) = image (fun h ↦ h + c) (Ico a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioc a b) = image (⇑{ toFun := fun h ↦ h + c, inj' := ⋯ }) (Ioc a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioc a b) = image (fun h ↦ h + c) (Ioc a b)
Module: Mathlib.Algebra.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioo a b) = image (⇑{ toFun := fun h ↦ h + c, inj' := ⋯ }) (Ioo a b)

Tactic:
Embedding.coeFn_mk

Goal state after:
α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioo a b) = image (fun h ↦ h + c) (Ioo a b)
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]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find ⋯] i0 = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ (toZ ⊥ (succ^[↑n] ⊥)).toNat ≤ ↑n

Tactic:
rw [Int.toNat_le]
      exact toZ_iterate_succ_le _

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

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝² : Semiring α
I : Ideal α
a b : α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
h : ⊥ = ⊤
⊢ 1 = 0

Tactic:
rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h

Goal state after:
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
h2 : (p * q + q * p - p) * q = p * q
h1 : q * p * q = q * p
⊢ Commute p q

Tactic:
simp_rw [sub_mul, add_mul, mul_assoc, hq.eq, add_sub_cancel_left, ← mul_assoc] at h2

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
h1 : q * p * q = q * p
h2 : q * p * q = p * q
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {-x, y} = span {x, y}

Tactic:
span_insert_neg

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case refine_1.inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : IsEmpty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

pp: case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : Nonempty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub

Tactic:
· exact ⟨I, disjoint, fun J hJ ↦ isEmptyElim (⟨J, hJ⟩ : c)⟩

Goal state after:
case refine_1.inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
h✝ : Nonempty ↑c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ {1, a} → a_1 ∉ ↑I

Tactic:
rintro _ (rfl | rfl)

Goal state after:
case inl
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ 1 ∉ ↑I

case inr
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a✝ : α
ha : IsIdempotentElem a✝
haI : a✝ ∉ I
⊢ a✝ ∉ ↑I
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ f.iterateMapComap i (m + 1) K ≠ f.iterateMapComap i (m + 1 + 1) K

Tactic:
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']

Goal state after:
case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[m]) K ≠
    ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[m + 1]) K
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ I, ⊥ < I ∧ I < ⊤

Tactic:
obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ I, ⊥ < I ∧ I < ⊤
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
⊢ ∃ p, p ≠ ⊥ ∧ p.IsPrime

Tactic:
obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : ¬IsField R
I : Ideal R
hI : I ≠ ⊥
hIm : I.IsMaximal
⊢ ∃ p, p ≠ ⊥ ∧ p.IsPrime
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder (Ideal R)

Tactic:
← not_iff_not,

Goal state after:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ ¬IsField R ↔ ¬IsSimpleOrder (Ideal R)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
by
  rw [← h.isBasis.filter_eq_generate, h.filter_eq]

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_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
⊢ p s

Tactic:
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)

Goal state after:
α : 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_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
A : ∀ (i : ι), ∀ s ∈ f i, ∀ (t : Set α), q t → q (s ∩ t)
⊢ p s
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
Ico_disjoint_Ico,

Goal state after:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : min x₂ y₂ ≤ max x₁ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
⊢ 𝓟 s = 𝓟 t ↔ s = t

Tactic:
by
  simp only [le_antisymm_iff, le_principal_iff, mem_principal]

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

Goal state before:
pp: case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)

Tactic:
exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_ge

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤

pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl ⊤ ⊓ map inr ⊤ ≤ ⊥

Tactic:
· apply inf_le_inf <;> simp

Goal state after:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl ⊤ ⊓ map inr ⊤ ≤ ⊥
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x₁ x₂ : Filter α
y : Filter β
⊢ Tendsto f (x₁ ⊔ x₂) y ↔ Tendsto f x₁ y ∧ Tendsto f x₂ y

Tactic:
by
  simp only [Tendsto, map_sup, sup_le_iff]

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
⊢ f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f

Tactic:
rw [← empty_mem_iff_bot, mem_inf_principal]

Goal state after:
α : Type u
f : Filter α
s : Set α
⊢ {x | x ∈ s → x ∈ ∅} ∈ f ↔ sᶜ ∈ f
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
⊢ CommMonoid α

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

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

Goal state before:
pp: case mpr
A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
this : Fintype ↑(range g)
⊢ N.FG

Tactic:
exact ⟨(range g).toFinset, by simpa⟩

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
⊢ ∃ x, IsTop x

Tactic:
rw [h, mk_set_eq_one_iff] at hs'

Goal state after:
case refine_1
α : Type u
inst✝ : Preorder α
h : cof α = 1
s : Set α
hs : IsCofinal s
hs' : ∃ x, s = {x}
⊢ ∃ x, IsTop x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case refine_2.a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ cof α ≤ 1

Tactic:
apply (cof_le (s := {t}) _).trans_eq (mk_singleton _)
      rwa [isCofinal_singleton_iff]

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 1 ↔ NoTopOrder α

Tactic:
← not_iff_not,

Goal state after:
α : Type u
inst✝ : Preorder α
⊢ ¬cof α ≠ 1 ↔ ¬NoTopOrder α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ 1 < cof α ↔ NoTopOrder α

Tactic:
← not_iff_not,

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ¬1 < cof α ↔ ¬NoTopOrder α
Module: Mathlib.Order.DirSupClosed

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

Tactic:
by
  simpa using dirSupInaccOn_iff_inter_subset isLowerSet_univ

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

Goal state before:
pp: δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], typeLT α = typeLT β → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ ⟦{ α := γ, r := fun x1 x2 ↦ x1 < x2, wo := ⋯ }⟧.liftOn' (fun w ↦ f w.α) ⋯ = f γ

Tactic:
rw [Quotient.liftOn'_mk]

Goal state after:
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], typeLT α = typeLT β → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ f { α := γ, r := fun x1 x2 ↦ x1 < x2, wo := ⋯ }.α = f γ
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
⊢ Cardinal.univ.{u_2, u_2 + 1}.ord ≤ (cof Ordinal.{u_2}).ord

Tactic:
ord_le_ord,

Goal state after:
α : Type u_1
⊢ Cardinal.univ.{u_2, u_2 + 1} ≤ cof Ordinal.{u_2}
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
o₁ o₂ : ↑(Iio (type r))
⊢ ¬r ((enum r) o₁) ((enum r) o₂) ↔ o₂ ≤ o₁

Tactic:
by
  rw [enum_lt_enum (r := r), not_lt]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ (Subtype.val ∘ ⇑(enum s hs) '' Iio a).Nonempty

Tactic:
simpa using ha.ne_bot

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ IsSuccPrelimit (typeLT α) ↔ NoMaxOrder α

Tactic:
← not_iff_not,

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ ¬IsSuccPrelimit (typeLT α) ↔ ¬NoMaxOrder α
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : iSup f = lsub f
i : ι
⊢ f i < lsub f

Tactic:
apply lt_lsub

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

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
⊢ (a + b) * c' ≤ a * c

Tactic:
grw [le_succ c', IH _ h, le_self_add (a := b), ba, ← mul_succ, succ_le_of_lt <| l.succ_lt h]

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

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ lift.{u, v} a.card < lift.{u, v} c

Tactic:
lift_lt,

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ a.card < c
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ (#↑s).ord ≤ (#α).ord

Tactic:
ord_le_ord,

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ #↑s ≤ #α
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
a✝ : Ordinal.{u}
ho : IsSuccLimit a✝
⊢ IsLUB (f '' Iio a✝) (f a✝)

Tactic:
rw [← h₂ _ ho]

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
a✝ : Ordinal.{u}
ho : IsSuccLimit a✝
⊢ IsLUB (f '' Iio a✝) (a✝.bsup fun x x_1 ↦ f x)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
⊢ a ^ c ≤ b ^ c

Tactic:
by_cases c = 0

Goal state after:
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : c = 0
⊢ a ^ c ≤ b ^ c

case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : ¬c = 0
⊢ a ^ c ≤ b ^ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
← natCast_div,

Goal state after:
m n : ℕ
⊢ ↑n * ↑(m / n) + ↑(m % n) = ↑m
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
by_cases c = 0

Goal state after:
case pos
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

case neg
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c