mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
⊢ LinearIndepOn R v s

Tactic:
rw [LinearIndepOn, linearIndependent_iff_finset_linearIndependent]

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (t : Finset ι), ↑t ⊆ s → LinearIndepOn R v ↑t
⊢ ∀ (s_1 : Finset ↑s), LinearIndependent R ((fun x ↦ v ↑x) ∘ Subtype.val)
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n i : ℕ
h : i + 1 < n + 1 + 1
x hd : M
tl : Fin n → M
i_lt : i < n + 1
i_fin : Fin (n + 1) := ⟨i, i_lt⟩
⊢ hd * ∏ i, i_fin.insertNth x tl i = x * (hd * ∏ i, tl i)

Tactic:
rw [prod_insertNth_go n i i_lt x tl, mul_left_comm]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
h : m.Coprime n
⊢ m.lcm n = m * n

Tactic:
rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
⊢ Coprime 1 n ↔ True

Tactic:
by simp [Coprime]

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: n : ℕ
⊢ n.Coprime 1 ↔ True

Tactic:
by simp [Coprime]

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

Goal state before:
pp: m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]

Tactic:
rw [hm, gcd_zero_right] at h; constructor
      · exact h.symm
      · rfl

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

Goal state before:
pp: m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
| ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩

Tactic:
equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]

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

Goal state before:
pp: case pos
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

pp: case neg
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : ¬iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j

Tactic:
· conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
    simpa using! ih _

Goal state after:
case neg
m : ℕ
ih : ∀ {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (m + 1) → ℕ
iv : ℕ
hi : iv < m + 1
j : Fin (n ⟨iv, hi⟩)
him : ¬iv < m
⊢ ↑(Sum.elim (Fin.castAdd (n (Fin.last m))) (Fin.natAdd (∑ i, n i.castSucc))
        ((finSigmaFinEquiv.sumCongr
            (Equiv.uniqueSigma fun i ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) (Sum.inr i)))))
          ((Equiv.sumSigmaDistrib fun a ↦ Fin (n (Sum.elim (Fin.castAdd 1) (Fin.natAdd m) a)))
            ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩))) =
    ∑ x, n (Fin.castLE ⋯ x) + ↑j
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ m * n - 1 = m * n - m + (m - 1)

Tactic:
←
      Nat.add_sub_assoc (by lia),

Goal state after:
m n : ℕ
hm1 : m % 2 = 1
hn1 : n % 2 = 1
hn0 : 0 < n
⊢ m * n - 1 = m * n - m + m - 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ Nat.card ↥s = s.card

Tactic:
by
  simp only [Nat.card_eq_fintype_card, Fintype.card_coe]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
by
  classical
  rw [_root_.and_comm, Bijective, and_congr_left_iff]
  intro h
  have := Fintype.ofFinite α
  have := Fintype.ofSurjective f h
  revert h
  rw [← and_congr_left_iff, ← Bijective, ← and_comm,
    card_eq_fintype_card, card_eq_fintype_card, Fintype.bijective_iff_surjective_and_card]

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝ : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
x y : (i : ι) → β i
⊢ (rightRel (Subgroup.pi univ s')) x y ↔ piSetoid x y

Tactic:
simp [Setoid.piSetoid_apply, rightRel_apply, Subgroup.mem_pi]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑(Quotient.out L • ↑s)

Tactic:
by
        rw [← eq_class_eq_leftCoset]
        change
          (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃
            _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _
        simp
        rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
H : ∀ (x y : R), c x y ↔ d x y
x✝¹ x✝ : R
⊢ c x✝¹ x✝ ↔ d x✝¹ x✝

Tactic:
apply H

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✝ : Nontrivial R
x y : R
ne : x ≠ y
⊢ ⊥ x y ≠ ⊤ x y

Tactic:
simp [ne]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ x * y * z = z

Tactic:
hxy,

Goal state after:
R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ 1 * z = z
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₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q

Tactic:
by rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
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
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
this : j ∉ I
⊢ (if h : j ∈ I then proj ⟨j, h⟩ else 0) b = 0

Tactic:
rw [dif_neg this, zero_apply]

Goal state after:
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:
rw [toZ_of_ge hi]

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)
Module: Mathlib.Data.Multiset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x : ℕ × ℕ
⊢ x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n

Tactic:
List.Nat.mem_antidiagonal

Goal state after:
n : ℕ
x : ℕ × ℕ
⊢ x.1 + x.2 = n ↔ x.1 + x.2 = n
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x} ⊔ span {y} = span {y} ↔ y ∣ x

Tactic:
sup_eq_right,

Goal state after:
α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x} ≤ span {y} ↔ y ∣ x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case inr
ι : Type u_1
R : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
inst✝ : DecidableEq ι
i : ι
r : R i
hr : r ∈ I i
j : ι
ne : i ≠ j
⊢ Pi.single i r j ∈ I j

Tactic:
simp [ne]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker ↔ x ∈ Ideal.span {1 - e}

Tactic:
rw [Ideal.mem_span_singleton']
  refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩
  obtain ⟨x, rfl⟩ := h
  change x * (1 - e) * e = 0
  rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

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)
i : ι
r : R i
⊢ Pi.single i r = Pi.single i r * Pi.single i 1

Tactic:
simp [← Pi.single_mul_left]

Goal state after:
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
n : ℕ
⊢ ∀ ⦃x y : ℕ →₀ P⦄,
    let s := x.support ∪ y.support;
    ∀ (ne : s.Nonempty), n = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y

Tactic:
induction n using Nat.strong_induction_on with

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
⊢ Ici '' s ⊆ (generate (range Ici)).sets

Tactic:
rintro - ⟨y, -, rfl⟩

Goal state after:
case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
y : α
⊢ Ici y ∈ (generate (range Ici)).sets
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : ι → ι' → Set α
p : ι → ι' → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
⊢ (⨅ i, l i).HasBasis (fun ii' ↦ p ii'.1 ii'.2) fun ii' ↦ s ii'.1 ii'.2

Tactic:
by
  refine ⟨fun t => ?_⟩
  rw [mem_iInf_of_directed h, Prod.exists]
  exact exists_congr fun i => (hl i).mem_iff

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

Goal state before:
pp: α : Type u_6
s : Set α
t : Set ↑s
⊢ 𝓟 t = comap Subtype.val (𝓟 (Subtype.val '' t))

Tactic:
rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ¬Disjoint l l' ↔ ¬∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

Tactic:
simp only [_root_.disjoint_iff, ← Ne.eq_def, ← neBot_iff, inf_eq_inter,
    hl.inf_basis_neBot_iff hl', not_exists, not_and, bot_eq_empty, ← nonempty_iff_ne_empty]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto f l (comap Subtype.val atTop) ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
tendsto_comap_iff,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto f l (comap Subtype.val atTop) ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
tendsto_comap_iff,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : IsAddTorsionFree G
n : ℤ
x : G
hx : n • x = 0
⊢ n = 0 ∨ x = 0

Tactic:
contrapose! hx; simpa using (zsmul_right_injective hx.1).ne hx.2

Goal state after:
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring R
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := e.addCommMonoid
⊢ ∀ (r s : R) (x : α), (r + s) • x = r • x + s • x

Tactic:
by simp [add_def, smul_def, add_smul]

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

Tactic:
rw [union_comm] at hdu hdst ⊢

Goal state after:
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
hdu : d ⊆ t ∪ s
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst✝ : d ∩ s ∪ d ∩ t = d
hdst : d ∩ t ∪ d ∩ s = 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 ∈ t ∪ s
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∈ s
⊢ f a ≤ b

Tactic:
simp_all [mem_upperBounds]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f (f^[n] a) ≤ ⨆ n, f^[n] a

pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f^[n] a ≤ ⨆ i, f (f^[i] a)

Tactic:
· rw [← f.iterate_succ_apply']
    exact le_ciSup hf' _

Goal state after:
case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
n : ℕ
⊢ f^[n] a ≤ ⨆ i, f (f^[i] a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x : α
⊢ Bounded r {x}

Tactic:
by
  refine ⟨enum r ⟨succ (typein r x), hr.succ_lt (typein_lt_type r x)⟩, ?_⟩
  intro b hb
  rw [mem_singleton_iff.1 hb]
  nth_rw 1 [← enum_typein r x]
  rw [@enum_lt_enum _ r, Subtype.mk_lt_mk]
  apply lt_succ

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α = (cof α).ord.card

Tactic:
card_ord

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ cof α = cof α
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ (type r).brange (bfamilyOfFamily' r f) → a ∈ range f

pp: case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r f)

Tactic:
· rintro ⟨i, hi, rfl⟩
    apply mem_range_self

Goal state after:
case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.bsup f = o₂.bsup fun a h ↦ f a ⋯

Tactic:
by
  subst ho
  rfl

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

Goal state before:
pp: ⊢ GaloisConnection ord card

Tactic:
refine fun c o ↦ c.inductionOn fun α ↦ o.inductionOn fun β s _ ↦ ?_

Goal state after:
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.blsub f = o₂.blsub fun a h ↦ f a ⋯

Tactic:
by
  subst ho
  rfl

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

Goal state before:
pp: case refine_2
c : Cardinal.{v}
⊢ lift.{u, v} c ≤ lift.{u, v} c.ord.card

Tactic:
card_ord

Goal state after:
case refine_2
c : Cardinal.{v}
⊢ lift.{u, v} c ≤ lift.{u, v} c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b x : ℕ
hx : x = 0
⊢ log b x ≤ x

Tactic:
simp [hx]

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

Goal state before:
pp: case cons.cons.head
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
⊢ b ≤ a

Tactic:
exact List.head_le_of_lt hmltl

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

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
a : Ordinal.{u}
h : ∀ (i : ι), f i a = a
⊢ nfpFamily f a = a

Tactic:
apply (Ordinal.iSup_le ?_).antisymm (le_nfpFamily f a)
  intro l
  rw [List.foldr_fixed' h l]

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

Goal state before:
pp: o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ IsPrincipal op o ↔ ∀ a < o, op a a < o

Tactic:
by
  use fun h a ha => h ha ha
  intro H a b ha hb
  obtain hab | hba := le_or_gt a b
  · exact (h₂ b hab).trans_lt <| H b hb
  · exact (h₁ a hba.le).trans_lt <| H a ha

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c.ord.card.ord = c.ord

Tactic:
card_ord

Goal state after:
c : Cardinal.{u_1}
⊢ c.ord = c.ord
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card.ord.card

Tactic:
card_ord

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
⊢ ℵ_ 1 ≤ #α ↔ Uncountable α

Tactic:
aleph_one_le_iff,

Goal state after:
α : Type u_1
⊢ ℵ₀ < #α ↔ Uncountable α
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
grw [one_le_iff_pos.2 a0]

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

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
i : ι
hi : x < f i
⊢ ∃ a, (fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩) a = ⟨x, hx⟩

Tactic:
exact ⟨⟨i, .mk ⟨x, hi⟩⟩, by simp⟩

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

Goal state before:
pp: a✝ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝ : Ordinal.{?u.6}
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi : i < a.cof.ord
⊢ a.cof.ord ≤ o

Tactic:
rw [hf.cof_eq]

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

Goal state before:
pp: case refine_1
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o' ≤ a.cof.ord

Tactic:
rw [hf.cof_eq]

Goal state after:
case refine_1
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o' ≤ o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{max u v, u} #(List ι) < (lift.{u, max u v} c).cof

pp: case refine_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
⊢ List.foldr f a l < c

Tactic:
· rw [Cardinal.lift_umax, c.lift_id']
    apply (Cardinal.lift_le.2 (mk_list_le_max _)).trans_lt
    rw [Cardinal.lift_max]
    apply max_lt <;> simpa

Goal state after:
case refine_2
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
l : List ι
⊢ List.foldr f a l < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ (ℵ_ 1).IsRegular

Tactic:
rw [← succ_aleph0]

Goal state after:
⊢ (succ ℵ₀).IsRegular
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
this : Nonempty ((α → Bool) ↪ Perm (α × Bool))
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
by
      obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by simp [← Cardinal.eq, mul_two]
      simp only [← le_def, mk_pi, mk_fintype, Fintype.card_bool, Nat.cast_ofNat,
        prod_const, lift_ofNat, lift_uzero] at this
      rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]

Goal state after:
Module: Mathlib.Data.DFinsupp.Ext

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)
x : ι
y : β x
⊢ f (single x y) = g (single x y)

Tactic:
apply H

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ filter p (single i x) = 0

Tactic:
by rw [filter_single, if_neg h]

Goal state after: