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

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

Tactic:
by_cases ha : a ∈ Set.range g

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∈ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)

case neg
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
x : α
hx : ∀ x_1 ∉ Set.range g, x_1 ∈ {x}
a b : α
ha : a ∉ Set.range g
⊢ f a = f b → a ≠ b → a = x ∨ a = g (f x)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ⨆ i ∈ I, (single R φ i).range ≤ ⨅ i ∈ J, (proj i).ker

Tactic:
by
  refine iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 ?_
  simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
  rintro b - j hj
  rw [proj_comp_single_ne R φ j i, zero_apply]
  rintro rfl
  exact h.le_bot ⟨hi, hj⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
⊢ b i = 0 i

Tactic:
by_cases hiI : i ∈ I

Goal state after:
case pos
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∈ I
⊢ b i = 0 i

case neg
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
hiI : i ∉ I
⊢ b i = 0 i
Module: Mathlib.LinearAlgebra.Prod

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
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : Semiring S
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M₄
inst✝⁷ : AddCommMonoid M₅
inst✝⁶ : AddCommMonoid M₆
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M₄
inst✝¹ : Module R M₅
inst✝ : Module R M₆
f✝ f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
x y : M
⊢ Function.prod (⇑f) (⇑g) (x + y) = Function.prod (⇑f) (⇑g) x + Function.prod (⇑f) (⇑g) y

Tactic:
by simp only [Function.prod_apply, Prod.mk_add_mk, map_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
s : Set M₂
h₀ : s.Nonempty
h₁ : s ⊆ ↑f.range
this : comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
⊢ span R (⇑f ⁻¹' s) = comap f (span R₂ s)

Tactic:
by exact le_antisymm (span_preimage_le f s) this

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case disjoint
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₂
⊢ Disjoint (inl R M M₂).range (inr R M M₂).range

pp: case codisjoint
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₂
⊢ Codisjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
· rw [disjoint_def]
    rintro ⟨_, _⟩ ⟨x, hx⟩ ⟨y, hy⟩
    simp only [Prod.ext_iff, inl_apply, inr_apply] at hx hy ⊢
    exact ⟨hy.1.symm, hx.2.symm⟩

Goal state after:
case codisjoint
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₂
⊢ Codisjoint (inl R M M₂).range (inr R M M₂).range
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
⊢ ∃ y_1, (f y_1, g y_1) = (f x, g y)

Tactic:
simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)]

Goal state after:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
h : f.ker ⊔ g.ker = ⊤
x y : M
⊢ ∃ y_1, y_1 - x ∈ f.ker ∧ g y_1 = g y
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : j < succFn i
⊢ j ≤ i

Tactic:
lt_isGLB_iff (succFn_spec i)

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
j i : ι
hij : ∃ c ∈ lowerBounds (Set.Ioi i), j < c
⊢ j ≤ i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = ↑m

Tactic:
Int.toNat_eq_max,

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMax (succ^[n] i0)
m : ℕ := (toZ i0 (succ^[n] i0)).toNat
h_eq : succ^[m] i0 = succ^[n] i0
hmn : m = n
⊢ toZ i0 (succ^[n] i0) = max (toZ i0 (succ^[n] i0)) 0
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑m

Tactic:
Int.toNat_eq_max,

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -max (-toZ i0 (pred^[n.succ] i0)) 0
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]

Tactic:
rw [antidiagonal_succ', antidiagonal_succ]

Goal state after:
n : ℕ
⊢ map (Prod.map id Nat.succ) ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n)) ++ [(n + 1 + 1, 0)] =
    (0, n + 2) :: map (Prod.map Nat.succ Nat.succ) (antidiagonal n) ++ [(n + 2, 0)]
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m ↦ range (m + 1), f x.snd (x.fst - x.snd) =
    ∏ x ∈ (range n).sigma fun m ↦ range (n - m), f x.fst x.snd

Tactic:
refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
    simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, implies_true,
      Sigma.forall, add_tsub_cancel_of_le, add_tsub_cancel_left]

Goal state after:
case refine_1
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a b : ℕ), a < n → b ≤ a → b < n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ range (↑a + 1) →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Iic a then f ⟨a_1, h⟩.succ / f ⟨a_1, h⟩.castSucc else 1 else 1) =
        (if hi : a_1 + 1 < n + 1 then f ⟨a_1 + 1, hi⟩ else 1) / if hi : a_1 < n + 1 then f ⟨a_1, hi⟩ else 1

Tactic:
by simp_all; grind

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
⊢ False

Tactic:
have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_notMem.mpr rid.1)

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S
x y : α
hxy : x * y ∈ I
rid : x ∉ I ∧ y ∉ I
hx : ¬Disjoint ↑(I ⊔ span {x}) ↑S
⊢ False
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
have := sum_pow_mem_span_pow f.support (fun a => f a * a) n

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : (∑ i ∈ f.support, f i * ↑i) ^ (f.support.card * n + 1) ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
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
⊢ ∀ (r s : R ⧸ I) (x : (ι → R) ⧸ pi fun x ↦ I), (r + s) • x = r • x + s • x

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (add_smul _ _ _)

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

Goal state before:
pp: ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
R : ι → Type u_6
inst✝ : (i : ι) → Semiring (R i)
x : (j : ι) → R j
⊢ x ∈ span (range fun i ↦ Pi.single i 1)

Tactic:
induction x using Pi.single_induction with

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

Goal state before:
pp: case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
eq

Goal state after:
case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ x = y
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ Finsupp.single 0 (f.prodOfFinsuppNat x).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) x) =
    Finsupp.single 0 (f.prodOfFinsuppNat y).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) y)

Tactic:
eq

Goal state after:
case inr.h
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
⊢ Finsupp.single 0 (f.prodOfFinsuppNat y).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) x) =
    Finsupp.single 0 (f.prodOfFinsuppNat y).1 + mapDomain (fun x ↦ x + 1) ((comapDomain.addMonoidHom ⋯) y)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ (f.prodOfFinsuppNat x).2 = (f.prodOfFinsuppNat y).2

Tactic:
eq

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

Goal state before:
pp: α : Type u_1
l : Filter α
P : Set α → Prop
⊢ l.HasBasis (fun s ↦ s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Tactic:
simp only [hasBasis_iff, id, and_assoc]

Goal state after:
α : Type u_1
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
x✝ : xᶜ ∈ f
⊢ (m '' x)ᶜ = s ↔ m '' x = sᶜ

Tactic:
compl_eq_comm,

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
x✝ : xᶜ ∈ f
⊢ sᶜ = m '' x ↔ m '' x = sᶜ
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t u : Set α
⊢ u ∈ 𝓟 s ⊔ 𝓟 t ↔ u ∈ 𝓟 (s ∪ t)

Tactic:
by simp only [union_subset_iff, mem_sup, mem_principal]

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

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s

Tactic:
inter_comm,

Goal state after:
α : Type u
s t : Set α
l : Filter α
⊢ t ∩ s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: ι : Type u_6
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n ↦ x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Tactic:
choose ns hge hns using frequently_atTop.1 h
  exact ⟨ns, h_tendsto.comp (tendsto_atTop_mono hge tendsto_id), hns⟩

Goal state after:
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)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)

Tactic:
le_lift_cof_iff

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set β), IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #↑s
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)
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
le_lift_cof_iff

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
le_lift_cof_iff

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), PosSMulStrictMono α (β i)
⊢ ∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : (i : ι) → β i⦄, b₁ < b₂ → a • b₁ < a • b₂

Tactic:
simp_rw [lt_def]
    rintro _a ha _b₁ _b₂ ⟨hb, i, hi⟩
    exact ⟨smul_le_smul_of_nonneg_left hb ha.le, i, smul_lt_smul_of_pos_left hi ha⟩

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))

Tactic:
← not_le,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
H : BddAbove (f ⁻¹' Iic x)
⊢ ¬f (succ (sSup (f ⁻¹' Iic x))) ≤ x
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
this : o ∈ Set.range ⇑Ordinal.liftPrincipalSeg.toRelEmbedding
⊢ o.card < univ.{u, v}

Tactic:
rcases this with ⟨o, h'⟩

Goal state after:
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : Ordinal.liftPrincipalSeg.toRelEmbedding o = o✝
⊢ o✝.card < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: α : Type u
⊢ Small.{v, u} α ↔ lift.{v + 1, u} #α < univ.{v, max u (v + 1)}

Tactic:
lt_univ'

Goal state after:
α : Type u
⊢ Small.{v, u} α ↔ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a + b < a + c ↔ b < c

Tactic:
← not_le,

Goal state after:
a b c : Ordinal.{u_4}
⊢ ¬a + c ≤ a + b ↔ b < c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ ¬a + c ≤ a + b ↔ b < c

Tactic:
← not_le,

Goal state after:
a b c : Ordinal.{u_4}
⊢ ¬a + c ≤ a + b ↔ ¬c ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
h : IsSuccLimit o
n : ℕ
⊢ ↑n < o

Tactic:
simpa using h.add_natCast_lt h.bot_lt n

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

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

Tactic:
by
  obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
  · simp
  · simp_rw [ho.ordinalPred_eq, ho]

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

Goal state before:
pp: a b : Ordinal.{u}
s : Set Ordinal.{u}
hs : ¬BddAbove s
ha : a ∈ s
hb : enumOrd s b < a
⊢ enumOrd s (succ b) ≤ a

Tactic:
by
  apply enumOrd_le_of_forall_lt ha
  intro c hc
  rw [lt_succ_iff] at hc
  exact ((enumOrd_strictMono hs).monotone hc).trans_lt hb

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s

Tactic:
let t := { b | a ≤ enumOrd s b }

Goal state after:
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b, ⋯⟩ ≤ ⟨a, ⋯⟩

Tactic:
Subtype.mk_le_mk,

Goal state after:
case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b ≤ a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
a : (succ o).ToType
⊢ ⟨(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a, ⋯⟩ ≤ ⟨o, ⋯⟩

Tactic:
Subtype.mk_le_mk,

Goal state after:
o : Ordinal.{u_1}
a : (succ o).ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a ≤ o
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 * succ c' + b ≤ a * c

Tactic:
le_self_add (a := b),

Goal state after:
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 * succ c' + (b + ?m.106) ≤ a * c

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
⊢ Ordinal.{u_4}
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 * succ c' + (b + ?m.106) ≤ a * c

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
⊢ Ordinal.{u_4}

Tactic:
ba,

Goal state after:
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 * succ c' + a ≤ a * c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case add_one
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
⊢ a * (c + 1) + (b + a) + b = a * (c + 1 + 1) + b

Tactic:
ba,

Goal state after:
case add_one
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
⊢ a * (c + 1) + a + b = a * (c + 1 + 1) + b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ a < b / c ↔ c * succ a ≤ b

Tactic:
← not_le,

Goal state after:
a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ ¬b / c ≤ a ↔ c * succ a ≤ b
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
rw [opow_le_iff_le_log hb hx]

Goal state after: