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

Goal state before:
pp: case mpr.comm
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a : A), Commute z a

pp: case left_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (b c : A), z * (b * c) = z * b * c

pp: case mpr.right_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Tactic:
case comm =>
      intro y
      rw [← b.linearCombination_repr y, linearCombination_apply, sum, commute_iff_eq,
        Finset.sum_mul, Finset.mul_sum]
      simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]

Goal state after:
case left_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (b c : A), z * (b * c) = z * b * c

case mpr.right_assoc
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
h : (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
⊢ ∀ (a b : A), a * b * z = a * (b * z)
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ (pi univ fun i ↦ closure (s i)) ≤ closure (univ.pi fun i ↦ s i)

Tactic:
exact pi_le_iff.mpr fun i => (gc_map_comap _).l_le <| (closure_le _).2 fun _x hx =>
          subset_closure <| mem_univ_pi.mpr fun j => by
        by_cases H : j = i
        · subst H
          simpa
        · simpa [H] using hs _

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).ncard = s.ncard + 1

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one,
    hs.cast_ncard_eq, encard_insert_of_notMem h]

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
N : s.Normal
g a : α
⊢ a ∈ g • ↑s ↔ a ∈ op g • ↑s

Tactic:
simp [mem_leftCoset_iff, mem_rightCoset_iff, N.mem_comm_iff]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: A : Type u
inst✝ : CommGroup A
n : ℤ
⊢ MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n

Tactic:
by
  ext x
  rw [← Quotient.out_eq' x]
  rfl

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

Tactic:
by
  ext x
  rw [← Quotient.out_eq' x]
  rfl

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
rw [ncard_le_one hs]

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b

Tactic:
· ext x
    rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc_of_not_isMin ha b

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

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ pred^[n] j = i

Tactic:
← hn_eq

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
h_exists : ∃ n, succ^[n] i = j
n : ℕ
hn_eq : succ^[n] i = j
hn_lt_ne : ∀ m < n, succ^[m] i ≠ j
⊢ pred^[n] (succ^[n] i) = i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

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

Tactic:
rw [lt_isGLB_iff (succFn_spec i)] at hij

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i ≤ a + 1, f i = f (a + 1) * ∏ i ≤ a, f i

Tactic:
simp only [← Iio_insert, mem_Iio, lt_self_iff_false, not_false_eq_true, prod_insert,
    prod_Iio_add_one_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
⊢ {x ∈ map { toFun := Prod.swap, inj' := ⋯ } (antidiagonal n) | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅

Tactic:
filter_map

Goal state after:
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
⊢ map { toFun := Prod.swap, inj' := ⋯ }
      (filter ((fun x ↦ x.2 = m) ∘ ⇑{ toFun := Prod.swap, inj' := ⋯ }) (antidiagonal n)) =
    if m ≤ n then {(n - m, m)} else ∅
Module: Mathlib.Algebra.BigOperators.Intervals

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

Tactic:
have : ∀ i < m, i ≤ n := by
    intro i hi
    exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : SuccOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (succ i) ⊔ f i = f (succ i)

Tactic:
by
  by_cases h : IsMax i
  · simpa only [succ_eq_iff_isMax.mpr h, sup_eq_right] using disjointed_le f i
  · rw [disjointed_apply]
    have : Iio (succ i) = Iic i := by
      ext
      simp only [mem_Iio, lt_succ_iff_eq_or_lt_of_not_isMax h, mem_Iic, le_iff_lt_or_eq, Or.comm]
    rw [this, ← sup'_eq_sup nonempty_Iic, ← partialSups_apply, hf.partialSups_eq,
      sdiff_sup_cancel <| hf <| le_succ i]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ univ.sup (disjointed f' ∘ ⇑R) = univ.sup f

Tactic:
simpa only [← sup_image, image_univ_equiv, hf'] using! sup_disjointed f'

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ (∏ i ∈ range n, if h : i < n then if ⟨i, h⟩ ∈ Icc a b then f ⟨i, h⟩ else 1 else 1) =
    ∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩ else 1

Tactic:
apply prod_congr_of_eq_on_inter

Goal state after:
case h₁
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n, a_1 ∉ Icc ↑a ↑b → (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) = 1

case h₂
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ Icc ↑a ↑b, a_1 ∉ range n → (if h : a_1 < n then f ⟨a_1, h⟩ else 1) = 1

case h
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ Icc ↑a ↑b →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) = if h : a_1 < n then f ⟨a_1, h⟩ else 1
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) * (x + y) ^ n = ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) * ∑ m ∈ range (n + 1), t n m =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a : α
h2 : IsUnit a
x : α
⊢ span {x * a} = span {x}

Tactic:
rw [mul_comm, span_singleton_mul_left_unit h2]

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

Goal state before:
pp: case inr.succ
n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ (n + 1).choose k + ∑ x ∈ Icc k n, x.choose k = (n + 1 + 1).choose (k + 1)

Tactic:
ih,

Goal state after:
case inr.succ
n✝ k n : ℕ
hmn✝ : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ (n + 1).choose k + (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1)
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : -(1 - b * a) ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I

Tactic:
neg_sub

Goal state after:
case mk
R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : b * a - 1 ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I
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 x y : R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
rw [dif_neg ha]; exact Classical.choose_spec (exists_inv ha)

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i

Tactic:
prod_range_succ,

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x ∈ range n, f (x + 1) (n - x) ^ n.choose (x + 1)) * f (n + 1) (n - n) ^ n.choose (n + 1) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
rw [eq_top_iff_one, span, Finsupp.mem_span_iff_linearCombination] at hs

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : ∃ l, (Finsupp.linearCombination α Subtype.val) l = 1
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr
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
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ := s.max' ne
hn : n = s.max' ne
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
clear_value n

Goal state after:
case inr
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
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne : s.Nonempty
n : ℕ
hn : n = s.max' ne
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
rcases em (∃ i, a ∈ s i) with ⟨i, hi⟩ | ha
  · refine (eventually_ge_atTop i).mono fun j hij ↦ ?_
    simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]
  · filter_upwards with i
    simp only [Set.piecewise_eq_of_notMem, not_exists.1 ha i, mt mem_iUnion.1 ha,
      not_false_eq_true]

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

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

Tactic:
simp only [mem_iUnion, exists_imp]
        exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) S
ne : S.Nonempty
t : Set α
⊢ t ∈ ⨅ i ∈ S, 𝓟 (s i) ↔ ∃ i ∈ S, s i ⊆ t

Tactic:
by
    refine mem_biInf_of_directed ?_ ne
    rw [directedOn_iff_directed, ← directed_comp] at h ⊢
    refine h.mono_comp _ ?_
    exact fun _ _ => principal_mono.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.comap f l ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t

Tactic:
simp only [mem_comap', hl.mem_iff]
    refine exists_congr (fun i => Iff.rfl.and ?_)
    exact ⟨fun h x hx => h hx rfl, fun h y hy x hx => h <| by rwa [mem_preimage, hx]⟩

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

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

Tactic:
inter_eventuallyEq_left

Goal state after:
α : Type u
s t : Set α
l : Filter α
⊢ (∀ᶠ (x : α) in l, x ∈ t → x ∈ s) ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Disjoint (comap f G) F ↔ Disjoint G (map f F)

Tactic:
by
  simp only [disjoint_iff, ← Filter.push_pull', map_eq_bot_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (F ⊓ comap f G).NeBot ↔ (map f F ⊓ G).NeBot

Tactic:
by
  rw [← map_neBot_iff, Filter.push_pull]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ Tendsto u atTop atTop

Tactic:
apply h.tendsto_atTop_atTop

Goal state after:
ι : Type u_1
α : Type u_3
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ ∀ (b : α), ∃ a, b ≤ u a
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
⊢ SurjOn (map m) (Iic F) (Iic G) ↔ G ≤ map m F

Tactic:
refine ⟨fun hm ↦ ?_, fun hm ↦ ?_⟩
  · rcases hm self_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩
    exact map_mono hHF
  · have : RightInvOn (F ⊓ comap m ·) (map m) (Iic G) :=
      fun H (hHG : H ≤ G) ↦ by simpa [Filter.push_pull] using hHG.trans hm
    exact this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
this : IsDirectedOrder ↑s
⊢ map Subtype.val atTop = atTop

Tactic:
refine map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
this : IsDirectedOrder ↑s
c : α
hc : a ≤ c
⊢ ∃ x, ↑x = c ∧ ∀ (a : { x // x ∈ s }), ↑a ≤ c ↔ a ≤ x
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩

Tactic:
refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0

Goal state after:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
s : { x // x ⊆ S }
hs : ↑s ≠ ↑⟨S, ⋯⟩
hs' : C ↑s
⊢ ∃ c, s < c ∧ C ↑c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

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

Tactic:
obtain ⟨_, ⟨b, rfl⟩, hb⟩ := hf' (f a)

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

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

Tactic:
rw [← dirSupClosedOn_compl, compl_compl]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∩ t)

Tactic:
by
  simpa using hs.dirSupInaccOn.inter isLowerSet_univ ht.dirSupInaccOn

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
by
  obtain ⟨a, rfl⟩ | ha := mem_range_succ_or_isSuccPrelimit a
  · simp
  · rw [ha.ordinalPred_eq, ha.le_succ_iff]

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≤ a
⊢ (b + if h : b ≤ a then Classical.choose ⋯ else 0) = a

Tactic:
rw [dif_pos h]

Goal state after:
a b : Ordinal.{u_4}
h : b ≤ a
⊢ b + Classical.choose ⋯ = a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ ∃ d < c, a < b + d

Tactic:
refine ⟨_, hc.succ_lt hd, ?_⟩
    rwa [succ_eq_add_one, ← add_assoc, lt_add_one_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x✝ : Ordinal.{?u.21}
⊢ 0 * x✝ = 0

Tactic:
exact mul_eq_zero'.2 (.inl rfl)

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

Goal state before:
pp: s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s

Tactic:
by
  constructor
  · rintro rfl
    exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩
  · rintro ⟨h₁, h₂⟩
    rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]

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

Goal state before:
pp: α : Type u_1
⊢ ∃ x, ∃ (x_1 : WellFoundedLT α), (#α).ord = typeLT α

Tactic:
let ⟨r, _, hr⟩ := exists_ord_eq α

Goal state after:
α : Type u_1
r : α → α → Prop
w✝ : IsWellOrder α r
hr : (#α).ord = type r
⊢ ∃ x, ∃ (x_1 : WellFoundedLT α), (#α).ord = typeLT α
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case refine_1
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : log b n < log b (n + 1)
⊢ b ^ log b (n + 1) = n + 1

pp: case refine_2
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ log b n < log b (n + 1)

Tactic:
· apply le_antisymm _ (Nat.lt_pow_of_log_lt hb H)
    exact Nat.pow_log_le_self b (Ne.symm (Nat.zero_ne_add_one n))

Goal state after:
case refine_2
b n : ℕ
hb : 1 < b
hn : n ≠ 0
H : b ^ log b (n + 1) = n + 1
⊢ log b n < log b (n + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ u * b ≤ b ^ x

Tactic:
← opow_succ

Goal state after:
b u v w x : Ordinal.{u_1}
hv : v < b
hw : w < b ^ u
hu : u < x
⊢ b ^ succ u ≤ b ^ x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (derivFamily f '' Set.Iio o) (derivFamily f o)

Tactic:
rw [derivFamily_limit _ h, Set.image_eq_range]
    have := h.nonempty_Iio.to_subtype
    exact isLUB_ciSup bddAbove_of_small

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ log b o * b

Tactic:
← opow_succ

Goal state after:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: x✝ : Ordinal.{u_1}
⊢ nfp id x✝ = id x✝

Tactic:
← iSup_iterate_eq_nfp,

Goal state after:
x✝ : Ordinal.{u_1}
⊢ ⨆ n, id^[n] x✝ = id x✝
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
ha : 0 < a
⊢ nfp (fun x ↦ a * x) 1 = a ^ ω

Tactic:
← iSup_iterate_eq_nfp,

Goal state after:
a : Ordinal.{u_1}
ha : 0 < a
⊢ ⨆ n, (fun x ↦ a * x)^[n] 1 = a ^ ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ succ (ℵ_ o) = ℵ_ (o + 1)

Tactic:
aleph_eq_preAleph,

Goal state after:
o : Ordinal.{u_1}
⊢ succ (preAleph (ω + o)) = ℵ_ (o + 1)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ℵ_ 0 = ℵ₀

Tactic:
aleph_eq_preAleph,

Goal state after:
⊢ preAleph (ω + 0) = ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ ℵ_ o

Tactic:
aleph_eq_preAleph,

Goal state after:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ preAleph (ω + o)