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

Goal state before:
pp: case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t \ s ∪ s = insert x s

Tactic:
hx,

Goal state after:
case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ {x} ∪ s = insert x s
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
have := Fintype.ofFinite α
  have := Fintype.ofFinite β
  simp only [Nat.card_eq_fintype_card, Fintype.card_eq]

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard = s.ncard - 1

Tactic:
exact eq_tsub_of_add_eq (ncard_sdiff_singleton_add_one h hs)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
⊢ s.ncard = t.ncard

Tactic:
have hbij : f'.Bijective := by
    constructor
    · rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
      simp only [f', Subtype.mk.injEq] at hxy ⊢
      exact h₂ _ _ hx hy hxy
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := h₃ y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hbij : Function.Bijective f'
⊢ s.ncard = t.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
⊢ (s \ t ∪ s ∩ t).ncard = s.ncard

Tactic:
sdiff_union_inter

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ s.ncard = s.ncard
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
r : R
a : A
b : B
⊢ ((algebraMap R A) r * a, r • b) = ((algebraMap R A) r * a, (algebraMap R B) r * b)

Tactic:
Algebra.smul_def r b

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
r : R
a : A
b : B
⊢ ((algebraMap R A) r * a, (algebraMap R B) r * b) = ((algebraMap R A) r * a, (algebraMap R B) r * b)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.ncard = 1
⊢ ∃ a, s = {a}

Tactic:
have hft := (finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype

Goal state after:
α : Type u_1
s : Set α
h : s.ncard = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.ncard = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
by
  rw [← encard_eq_four, ncard_def]
  simp

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

Goal state before:
pp: case h
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 : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
f' : H → I
hf' : ∀ (a : H) (b : I), (∃ y, f y = (a, b)) ↔ f' a = b
⊢ mrange f = { toFun := f', map_one' := ⋯, map_mul' := ⋯ }.mgraph

Tactic:
simpa [SetLike.ext_iff] using hf'

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ f : M →* P
x y : (ker f).Quotient
h : (kerLift f).mrangeRestrict x = (kerLift f).mrangeRestrict y
⊢ (kerLift f) x = (kerLift f) y

Tactic:
rcases x with ⟨⟩

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ f : M →* P
x y : (ker f).Quotient
a✝ : M
h : (kerLift f).mrangeRestrict (Quot.mk (⇑(ker f).toSetoid) a✝) = (kerLift f).mrangeRestrict y
⊢ (kerLift f) (Quot.mk (⇑(ker f).toSetoid) a✝) = (kerLift f) y
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ ∀ (m : R) (x : M ⧸ p),
    (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun (m • x) =
      τ₁₂ m • (↑(lift p.toAddSubgroup f.toAddMonoidHom h)).toFun x

Tactic:
rintro a ⟨x⟩; exact f.map_smulₛₗ a x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
R' : Type u_4
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Add R'
inst✝¹ : Mul R'
c✝ d : RingCon R
inst✝ : Subsingleton R
c c' : RingCon R
r r' : R
⊢ True ↔ c' r r

Tactic:
c'.refl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
φ : ι → Type i
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M₂ →ₗ[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp only [LinearMap.ext_iff, pi_apply, funext_iff]
  exact ⟨fun h a b => h b a, fun h a b => h b a⟩

Goal state after:
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : IsField R
a✝ : R
ha : a✝ ≠ 0
x✝¹ x✝ : R
hb : (fun x ↦ x * a✝) x✝¹ = (fun x ↦ x * a✝) x✝
⊢ x✝¹ = x✝

Tactic:
obtain ⟨x, hx⟩ := h.mul_inv_cancel ha
    simpa [mul_assoc, hx] using congr_arg (· * x) hb

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
p : Submodule 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₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
⊢ map f (comap p.mkQ q) ≤ map (p.liftQ f h) q

Tactic:
rintro _ ⟨x, hxq, rfl⟩; exact ⟨Quotient.mk x, hxq, rfl⟩

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

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
by
  simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc a b

Goal state after:
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₂
⊢ map (LinearMap.fst R M M₂) (snd R M M₂) = ⊥

Tactic:
aesop (add simp snd)

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case a
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i : ι
⊢ ⨆ i_1, f ↑i_1 ≤ (Iic i).sup' ⋯ f

Tactic:
· exact ciSup_le fun ⟨j, hj⟩ ↦ le_sup' f (by simpa only [mem_Iic, Set.mem_Iic] using hj)

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ disjointed f i = f i

Tactic:
rw [disjointed_apply, sdiff_eq_left, disjoint_iff, sup_inf_distrib_left,
    sup_congr rfl <| fun j hj ↦ disjoint_iff.mp <| (hf _ (mem_Iio.mp hj)).symm]

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ ((Iio i).sup fun j ↦ ⊥) = ⊥
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
⊢ 0 ≤ toZ i0 i

Tactic:
by rw [toZ_of_ge hi]; exact Int.natCast_nonneg _

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 : ¬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
⊢ 0 ≤ - -↑(Nat.find ⋯)

Tactic:
rw [neg_neg]

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
⊢ 0 ≤ ↑(Nat.find ⋯)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
rcases le_or_gt hι.some i with hi | hi
    · have h_nonneg : 0 ≤ toZ hι.some i := toZ_nonneg hi
      simp_rw [if_pos h_nonneg]
      exact iterate_succ_toZ i hi
    · have h_neg : toZ hι.some i < 0 := toZ_neg hi
      simp_rw [if_neg (not_le.mpr h_neg)]
      exact iterate_pred_toZ i hi

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
⊢ toZ hι.some ((fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n

Tactic:
rcases le_or_gt 0 n with hn | hn

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ hι.some ((fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n

case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : n < 0
⊢ toZ hι.some ((fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) n) = n
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
⊢ {a ∈ antidiagonal n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔
                      ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])

Goal state after:
n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
aux₂ : ∀ (i j : ℕ), (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔ ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j
⊢ {a ∈ antidiagonal n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: α : Type u
inst✝² : Semiring α
I : Ideal α
inst✝¹ : I.IsTwoSided
inst✝ : I.IsPrime
x y : α
hx : y ∉ I
⊢ x * y ∈ I ↔ x ∈ I

Tactic:
by
  rw [Ideal.IsPrime.mul_mem_iff_mem_or_mem] <;> aesop

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ I ≠ ⊤ ↔ ∃ M, M.IsMaximal ∧ I ≤ M

Tactic:
refine ⟨exists_le_maximal I, ?_⟩

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ (∃ M, M.IsMaximal ∧ I ≤ M) → I ≠ ⊤
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
span_pair_add_right

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y} = span {x, y}
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:
span_pair_add_right_mul

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0

Tactic:
cases n with
  | zero => simp
  | succ n => simp [Int.alternating_sum_range_choose_eq_choose]

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

Goal state before:
pp: α : Type u
inst✝³ : CommSemiring α
inst✝² : IsPrincipalIdealRing α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ ⊥.IsPrime

Tactic:
exact isPrime_bot

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
⊢ ∀ {x y : Set α},
    x ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b} →
      y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b} → x ∩ y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}

Tactic:
by
        rintro x y ⟨a, ha, b, hb, rfl⟩ ⟨c, hc, d, hd, rfl⟩
        refine ⟨a ∩ c, inter_mem ha hc, b ∩ d, inter_mem hb hd, ?_⟩
        ac_rfl

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ (∀ {i : ι}, p i → (s i).Nonempty) ↔ ¬∃ i, p i ∧ s i = ∅

Tactic:
simp only [not_exists, not_and, nonempty_iff_ne_empty]

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

Goal state before:
pp: case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ generate (Ici '' s) ≤ generate (range Ici)

Tactic:
· rw [le_generate_iff]
    rintro - ⟨x, -, -, rfl⟩
    rcases hs x with ⟨y, ys, hy⟩
    have A : Ici y ∈ generate (Ici '' s) := mem_generate_of_mem (mem_image_of_mem _ ys)
    have B : Ici y ⊆ Ici x := Ici_subset_Ici.2 hy
    exact sets_of_superset (generate (Ici '' s)) A B

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
m : γ → β
n : β → α
s : Set γ
⊢ sᶜ ∈ comap m (comap n f) ↔ sᶜ ∈ comap (n ∘ m) f

Tactic:
simp only [compl_mem_comap, image_image, (· ∘ ·)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ comap f ⊤

Tactic:
by
  rw [comap_top]
  exact le_top

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
la : Filter α
lb : Filter β
h : la.NeBot → Tendsto f la lb
⊢ Tendsto f la lb

Tactic:
rcases eq_or_neBot la with rfl | hla
  · exact tendsto_bot
  · exact h hla

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map id g ≤ map mab f

Tactic:
← map_congr h₁,

Goal state after:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map (mab ∘ mba) g ≤ map mab f
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort w
s : ι → Set α
x : Set α
⊢ x ∈ ⨆ x, 𝓟 (s x) ↔ x ∈ 𝓟 (⋃ i, s i)

Tactic:
simp only [mem_iSup, mem_principal, iUnion_subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
U : Set β
V : Set α
V_in : V ∈ F
W : Set α
h : f ⁻¹' U = V ∩ W
Z : Set β
Z_in : Z ∈ G
hZ : f ⁻¹' Z ⊆ W
⊢ f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z)

Tactic:
by rw [image_inter_preimage]

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

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

Tactic:
rcases hm self_mem_Iic with ⟨H, (hHF : H ≤ F), rfl⟩
    exact map_mono hHF

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
ha : 0 ≤ a
hb : 0 ≤ b₁
⊢ 0 ≤ a • b₁

Tactic:
by
  simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosMono α β
ha : a ≤ 0
hb : 0 ≤ b
⊢ a • b ≤ 0

Tactic:
by
  simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

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✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b

Tactic:
rw [← sub_pos, ← sub_smul]

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < (a₂ - a₁) • _b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ c ≤ a - b

Tactic:
rw [← add_le_add_iff_left b]
  exact h.trans (le_add_sub a b)

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
⊢ Subtype.val ∘ ⇑(enum s hs) = f ↔ StrictMono f ∧ range f = s

Tactic:
by
  have H := (Subtype.strictMono_coe _).comp (enum s hs).strictMono
  constructor
  · rintro rfl
    use (Subtype.strictMono_coe _).comp (enum s hs).strictMono
    simp
  · rintro ⟨hf, rfl⟩
    rw [← StrictMono.range_inj H hf]
    simp
    rfl

Goal state after:
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
⊢ a < b + succ d

Tactic:
rwa [succ_eq_add_one, ← add_assoc, lt_add_one_iff]

Goal state after:
Module: Mathlib.Logic.Small.List

Goal state before:
pp: α : Type v
inst✝ : Small.{u, v} α
⊢ Small.{u, v} (List α)

Tactic:
let e : (Σ n, List.Vector α n) ≃ List α := Equiv.sigmaFiberEquiv List.length
  exact small_of_surjective e.surjective

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

Goal state before:
pp: o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi

Tactic:
simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a)

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

Goal state before:
pp: c : Cardinal.{v}
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

Tactic:
refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_
  · rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩
    rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]
  · rw [ord_le, ← lift_card, card_ord]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔ ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o

Tactic:
exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩

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

Goal state before:
pp: case inr.inl
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hm : m ≠ 0
hb : b ≤ 1
⊢ log b n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1)

pp: case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)

Tactic:
· obtain rfl | rfl := le_one_iff_eq_zero_or_eq_one.1 hb <;>
      simp only [log_zero_left, log_one_left] <;> lia

Goal state after:
case inr.inr
b m : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < b ∧ 0 ≠ 0
⊢ log b 0 = m ↔ b ^ m ≤ 0 ∧ 0 < b ^ (m + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case neg.add_one
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ (c + 1) ≤ b ^ (c + 1)

Tactic:
simpa using mul_le_mul' IH ab

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

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

Tactic:
zero_opow,

Goal state after:
case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ 0 = 0 ^ b * 0

case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
o : Ordinal.{u_4}
this : ∀ {b : ℕ}, o ≤ ↑b → ∃ c, o = ↑c
⊢ o ∈ Nat.cast '' Iio n ↔ o ∈ Iio ↑n

Tactic:
grind [Nat.cast_lt]

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

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ #α * #α ≤ #α

Tactic:
have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
⊢ #α * #α ≤ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0

Tactic:
and_assoc

Goal state after:
case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ ℵ₀ ≤ a ∧ b ≤ a ∧ b ≠ 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
add_eq_max ha

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
⊢ max b a = max b a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
add_eq_max ha

Goal state after:
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
⊢ (f a).cof = a.cof

Tactic:
rw [hf.apply_of_isSuccLimit ha, cof_iSup_Iio _ ha.isSuccPrelimit]

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
⊢ StrictMono fun b ↦ f ↑b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b = a ↔ max ℵ₀ b ≤ a ∨ b = 0

Tactic:
rw [max_le_iff]
  refine ⟨fun h => ?_, ?_⟩
  · rcases le_or_gt ℵ₀ a with ha | ha
    · left
      use ha
      rw [← not_lt]
      apply fun hb => ne_of_gt _ h
      intro hb
      exact hb.trans_le (self_le_add_left b a)
    right
    rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
    norm_cast at h ⊢
    rw [← add_right_inj, h, add_zero]
  · rintro (⟨h1, h2⟩ | h3)
    · rw [add_eq_max h1, max_eq_left h2]
    · rw [h3, add_zero]

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

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
⊢ sSup ((fun x ↦ x + 1) '' s) < a

Tactic:
let f := OrderIso.ofRelIsoLT (enum (α := s) (· < ·))

Goal state after:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
⊢ sSup ((fun x ↦ x + 1) '' s) < a