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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ s.ncard = n

Tactic:
let f' : Fin n → α := fun i ↦ f i.val i.is_lt
  suffices himage : s = f' '' Set.univ by
    rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]
    exact InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h
  ext x
  simp only [image_univ, mem_range]
  refine ⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩
  obtain ⟨i, hi, rfl⟩ := hf x hx
  use ⟨i, hi⟩

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe

Tactic:
intro t ht

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
t : Set α
ht : t ∈ {t | t ⊆ ↑s ∧ t.ncard = n}
⊢ t ∈ range SetLike.coe
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ (t \ s).ncard + s.ncard = t.ncard

Tactic:
by
  to_encard_tac
  rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.sdiff.cast_ncard_eq,
    encard_sdiff_add_encard_of_subset h]

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : ↑s.card < ENat.card α
⊢ ∃ a, a ∉ s

Tactic:
by
  contrapose! hs
  simp [← Set.encard_coe_eq_coe_finsetCard, Set.eq_univ_of_forall (α := α) (s := s) hs]

Goal state after:
Module: Mathlib.Algebra.Group.Graph

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : Monoid I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →* I
he₁ : mrange f = e₁.mgraph
⊢ ∀ (g₁ g₂ : G),
    ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).1 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).1 →
      ((MulEquiv.prodComm.toMonoidHom.comp f) g₁).2 = ((MulEquiv.prodComm.toMonoidHom.comp f) g₂).2

Tactic:
by simp [hf]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁹ : Semiring R
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
i : ι
x : φ i
⊢ ((lsum R φ S) f) (Pi.single i x) = (f i) x

Tactic:
lsum_apply,

Goal state after:
R : Type u
M : Type v
ι : Type x
inst✝⁹ : Semiring R
φ : ι → Type i
inst✝⁸ : (i : ι) → AddCommMonoid (φ i)
inst✝⁷ : (i : ι) → Module R (φ i)
inst✝⁶ : DecidableEq ι
S : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : (i : ι) → φ i →ₗ[R] M
i : ι
x : φ i
⊢ (∑ i, f i ∘ₗ proj i) (Pi.single i x) = (f i) x
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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₂
⊢ (inr R M M₂).ker = ⊥

Tactic:
rw [ker, ← prod_bot, prod_comap_inr]

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝² : IsTrans α r
ι : Sort u_4
κ : Sort u_5
inst✝¹ : Nonempty ι
inst✝ : Finite κ
f : ι → α
hf : Directed r f
g : κ → ι
⊢ ∃ z, ∀ (i : κ), r (f (g i)) (f z)

Tactic:
simpa using
    (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g))

Goal state after:
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 : ι
⊢ p ((partialSups f) i) ↔ ∀ j ≤ i, p (f j)

Tactic:
rw [partialSups_apply, apply_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i ↦ (partialSups f) i)

Tactic:
bddAbove_range_partialSups

Goal state after:
case pos.refine_2
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range f)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
⊢ ∀ (g₁ g₂ : G),
    ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₁).1 = ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₂).1 →
      ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₁).2 = ((↑(LinearEquiv.prodComm S H I) ∘ₛₗ f) g₂).2

Tactic:
by simp [hf]

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

Goal state before:
pp: case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ -↑n ≤ toZ i0 (pred^[n] i0)

Tactic:
rw [toZ_of_lt h]
    refine Int.neg_le_neg ?_
    norm_cast
    exact Nat.find_min' _ rfl

Goal state after:
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) = ↑n

pp: case neg
ι : 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) = ↑n

Tactic:
· nth_rw 2 [← hmn]
    rw [Int.toNat_eq_max, toZ_of_ge (le_succ_iterate _ _), max_eq_left]
    exact Int.natCast_nonneg _

Goal state after:
case neg
ι : 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) = ↑n
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 ∈ antidiagonal n | x.2 = m} = if m ≤ n then {(n - m, m)} else ∅

Tactic:
rw [← map_swap_antidiagonal, filter_map]
  simp [filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m✝ n : ι
this : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
m : ι
hm : n ≤ m
ih : (Ioc n m).sup (disjointed f) = f m \ f n
h'm : ¬IsMax m
⊢ (Ioc n (succ m)).sup (disjointed f) = f (succ m) \ f n

Tactic:
rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]
      simp only [sup_insert, hf.disjointed_succ h'm, ih]
      exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ j ∈ range n, f (n - 1 - j) = ∏ j ∈ range n, f j

Tactic:
by
  cases n
  · simp
  · simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
    rw [prod_Ico_reflect _ _ le_rfl]
    simp

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ I = ⊤ → ∀ (M : Ideal α), M.IsMaximal → ¬I ≤ M

Tactic:
rintro rfl _ hMmax

Goal state after:
α : Type u
inst✝ : Semiring α
M✝ : Ideal α
hMmax : M✝.IsMaximal
⊢ ¬⊤ ≤ M✝
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x + y * z, y} = span {x, y}

Tactic:
ext
  simp_rw [mem_span_pair]
  exact ⟨fun ⟨a, b, h⟩ => ⟨a, b + a * z, by rw [← h]; ring1⟩,
    fun ⟨a, b, h⟩ => ⟨a, b - a * z, by rw [← h]; ring1⟩⟩

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

Goal state before:
pp: case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
⊢ ∀ ⦃a_1 b : α⦄, a = a_1 * b → IsUnit a_1 ∨ IsUnit b

Tactic:
intro u

Goal state after:
case isUnit_or_isUnit
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
u : α
⊢ ∀ ⦃b : α⦄, a = u * b → IsUnit u ∨ IsUnit b
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.IsPrime

Tactic:
or_iff_right_of_imp

Goal state after:
α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P.IsPrime ↔ P.IsPrime

α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
P : Ideal α
⊢ P = ⊥ → P.IsPrime
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: 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
h : map f K ≤ map i K
n : ℕ
⊢ f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K

Tactic:
nth_rw 2 [iterateMapComap]

Goal state after:
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
h : map f K ≤ map i K
n : ℕ
⊢ f.iterateMapComap i n K ≤ (fun K ↦ comap f (map i K))^[n + 1] K
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I

Tactic:
Finset.prod_eq_prod_sdiff_singleton_mul hi

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ (∏ x ∈ s \ {i}, f x) * f i ∈ I
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
I : Ideal R
h_bot : I ≠ ⊥
h_top : I ≠ ⊤
⊢ ¬IsField R

Tactic:
by
  contrapose h_bot
  exact ((isField_iff_maximal_bot.mp h_bot).eq_of_le h_top bot_le).symm

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

Goal state before:
pp: case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨U, U_in⟩) ((fun s ↦ 𝓟 ↑s) ⟨W, W_in⟩) ∧
    (fun x1 x2 ↦ x1 ≥ x2) ((fun s ↦ 𝓟 ↑s) ⟨V, V_in⟩) ((fun s ↦ 𝓟 ↑s) ⟨W, W_in⟩)

Tactic:
simp only [le_principal_iff, mem_principal]

Goal state after:
case h
α : Type u_1
B : FilterBasis α
U : Set α
U_in : U ∈ B.sets
V : Set α
V_in : V ∈ B.sets
W : Set α
W_in : W ∈ B.sets
W_sub : W ⊆ U ∩ V
⊢ W ⊆ U ∧ W ⊆ V
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f (1 • ⋯.choose) y = Pi.single x 1 y

pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0

Tactic:
one_smul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ f ⋯.choose y = Pi.single x 1 y

R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
α : Type u_5
inst✝ : Finite α
f : M →ₗ[R] α → R
s : Surjective ⇑f
x y : α
⊢ 0 • ⋯.choose = 0
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ comap (lsingle i) (submodule p)
⊢ x ∈ p i

Tactic:
by simpa using hx i

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

Goal state before:
pp: case right
α : 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 := ⋯
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
⊢ ∀ (t' : Set α), s ∩ t ⊆ t' → p t'

Tactic:
intro u

Goal state after:
case right
α : 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
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
⊢ s ∩ t ⊆ u → p u
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ s ∈ comap (Prod.mk x) F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F

Tactic:
mem_comap',

Goal state after:
α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ {y | ∀ ⦃x_1 : β⦄, (x, x_1) = y → x_1 ∈ s} ∈ F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F
Module: Mathlib.Order.Filter.Basic

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

Tactic:
simp only [le_principal_iff, mem_principal]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : Filter α
b : β
⊢ Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b

Tactic:
by
  simp only [Tendsto, le_pure_iff, mem_map', mem_singleton_iff, Filter.Eventually]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t

Tactic:
← image_inter h,

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' (s₁ ∩ s₂) ⊆ t
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
⊢ atTop.HasBasis (fun x ↦ a < x) Ioi

Tactic:
have : Nonempty α := ⟨a⟩
  refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
  obtain ⟨d, hcd⟩ := exists_gt c
  exact ⟨d, hac.trans_lt hcd, Ioi_subset_Ioi (hbc.trans hcd.le)⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
u : α → β
inst✝ : Preorder β
h : Tendsto u atTop atTop
a : α
b : β
this✝ : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a', a ≤ a' ∧ b ≤ u a'

Tactic:
exact this.exists

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁶ : Preorder α
inst✝⁵ : Monoid α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : DistribMulAction α β
inst✝ : SMulPosReflectLT α β
_b : βᵒᵈ
hb : 0 ≤ _b
a₁ a₂ : α
h : a₁ • _b < a₂ • _b
⊢ a₁ < a₂

Tactic:
by
    rw [← neg_lt_neg_iff, ← smul_neg, ← smul_neg] at h
    exact lt_of_smul_lt_smul_right (β := β) h <| neg_nonneg.2 hb

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α] (hDL : IsLowerSet D) (hs : DirSupClosedOn D s)
    (ht : DirSupClosedOn D t) ⦃d : Set α⦄ (hD : d ∈ D) (hdu : d ⊆ s ∪ t) (hd₀ : d.Nonempty)
    (hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d) ⦃a : α⦄ (ha : IsLUB d a) (hdst : d ∩ s ∪ d ∩ t = d),
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) → a ∈ s ∪ t
h : ¬(DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s))
⊢ a ∈ s ∪ t

pp: α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s)
⊢ a ∈ s ∪ t

Tactic:
· rw [union_comm] at hdu hdst ⊢
    exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <|
      (directedOn_union_iff.mp (by rwa [hdst])).resolve_right h

Goal state after:
α✝ : Type u_1
s✝ t✝ : Set α✝
D✝ : Set (Set α✝)
inst✝¹ : Preorder α✝
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu : d ⊆ s ∪ t
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst : d ∩ s ∪ d ∩ t = d
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s)
⊢ a ∈ s ∪ t
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ ⨆ i, f i + 1 = ⨆ i, f i

Tactic:
apply (iSup_le_iSup_add_one f).antisymm'
  by_cases hf' : BddAbove (range f)
  · rw [ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')]
    intro i
    obtain ⟨j, hj⟩ := exists_gt i
    apply (le_ciSup hf' j).trans'
    rw [add_one_le_iff]
    exact hf hj
  · rw [ciSup_of_not_bddAbove hf', ciSup_of_not_bddAbove]
    rwa [← bddAbove_range_add_one_iff] at hf'

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

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ o.bsup f = 0 ↔ ∀ (i : Ordinal.{u_3}) (hi : i < o), f i hi = 0

Tactic:
refine
    ⟨fun h i hi => ?_, fun h =>
      le_antisymm (bsup_le fun i hi => nonpos_iff_eq_zero.2 (h i hi)) zero_le⟩

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
h : o.bsup f = 0
i : Ordinal.{u_3}
hi : i < o
⊢ f i hi = 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ iSup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ∨
    succ (iSup (o.familyOfBFamily f)) = lsub (o.familyOfBFamily f)

Tactic:
exact iSup_eq_lsub_or_succ_iSup_eq_lsub _

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
h : (log.go y b y).snd ≥ x
⊢ b ^ x ≤ b ^ (log.go y b y).snd

Tactic:
exact Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

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

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

Tactic:
by grind [isSuccLimit_add]

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ IsSuccPrelimit a ↔ ω ∣ a

Tactic:
by
  refine ⟨fun l => ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩, fun h => ?_⟩
  · refine l.le_iff_forall_le.2 fun x hx => le_of_lt ?_
    rw [lt_mul_iff_div_lt omega0_ne_zero, ← succ_le_iff, ← mul_le_iff_le_div omega0_ne_zero,
      mul_succ, add_le_iff_of_isSuccLimit isSuccLimit_omega0]
    intro b hb
    rcases lt_omega0.1 hb with ⟨n, rfl⟩
    grw [mul_div_le]
    exact (lt_sub.1 <| natCast_lt_of_isSuccLimit (isSuccLimit_sub l hx) _).le
  · rcases h with ⟨a0, b, rfl⟩
    exact isSuccPrelimit_mul_left isSuccLimit_omega0

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b n ≤ clog b n

Tactic:
obtain hb | hb := le_or_gt b 1
  · rw [log_of_left_le_one hb]
    exact zero_le _
  cases n with
  | zero =>
    rw [log_zero_right]
    exact zero_le _
  | succ n =>
    exact (Nat.pow_le_pow_iff_right hb).1
      ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

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

Goal state before:
pp: x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
by
  obtain hb | hb := lt_or_ge 1 b
  · rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]
    exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)
  · simpa only [log_of_left_le_one hb, zero_add] using le_rfl

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : o.IsInitial
c : Cardinal.{u_1}
⊢ o ≤ c.ord ↔ o.card ≤ c

Tactic:
by
  grw [← ord_le_ord, ho.ord_card]

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

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d

Tactic:
apply mul_le_mul_right

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ succ b ≤ d
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case refine_1.refine_1
a : Ordinal.{u_1}
⊢ preBeth a < preBeth (succ a)

pp: case refine_1.refine_2
a : Ordinal.{u_1}
⊢ preBeth (succ a) ≤ 2 ^ preBeth a

Tactic:
· rw [preBeth_lt_preBeth, lt_succ_iff]

Goal state after:
case refine_1.refine_2
a : Ordinal.{u_1}
⊢ preBeth (succ a) ≤ 2 ^ preBeth a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a

Tactic:
rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)

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

case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 1 = a

case refine_2.inr.inr
b : Cardinal.{u_1}
⊢ 0 * b = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b ≤ c

pp: case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b

Tactic:
· rw [← h]
    apply self_le_add_left

Goal state after:
case a
a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ c ≤ b
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

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

Tactic:
by
  apply le_antisymm
  · simp_rw [Ordinal.iSup_le_iff, add_one_le_iff]
    exact fun i ↦ (f i).2
  · refine le_of_forall_lt fun b hb ↦ ?_
    obtain ⟨_, ⟨c, rfl⟩, hc : b ≤ _⟩ := hf.isCofinal_range ⟨b, hb⟩
    apply hc.trans_lt
    rw [← add_one_le_iff]
    apply Ordinal.le_iSup

Goal state after: