mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
⊢ [].alternatingProd = ∏ i, [][i] ^ (-1) ^ ↑i

Tactic:
by
    rw [alternatingProd, Finset.prod_eq_one]
    rintro ⟨i, ⟨⟩⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : LinearOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : AddRightReflectLE R
inst✝² : IsCancelAdd M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ xᶜ, x_1 i • v i), ∃ x, ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i
i : ι
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ t f, ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
exact ⟨t, f, heq, i, hi', hfi⟩

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
⊢ (s ∪ t).encard = s.encard + t.encard

Tactic:
unfold encard

Goal state after:
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ ENat.card ↑(s ∪ t) = ENat.card ↑s + ENat.card ↑t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).encard = s.encard * t.encard

Tactic:
unfold encard

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ ENat.card ↑(s ×ˢ t) = ENat.card ↑s * ENat.card ↑t
Module: Mathlib.Data.Set.Card

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

Tactic:
rw [← encard_union_eq disjoint_sdiff_left, sdiff_union_of_subset h]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R M

Tactic:
by
  rw [← rank_top R M]
  exact rank_mono le_top

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton

Tactic:
exact encard_le_one_iff_subsingleton

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
j : ι
hj : j ∉ univ \ {i}
⊢ (Finsupp.single i (l i) - l) j = 0

Tactic:
have hij : j = i :=
          Classical.not_not.1 fun hij : j ≠ i =>
            hj ((mem_sdiff _).2 ⟨mem_univ _, fun h => hij (eq_of_mem_singleton h)⟩)

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
j : ι
hj : j ∉ univ \ {i}
hij : j = i
⊢ (Finsupp.single i (l i) - l) j = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ (s ∪ r').encard = s.encard + r'.encard

Tactic:
encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)

Goal state after:
case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ s.encard + r'.encard = s.encard + r'.encard
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
⊢ v i ∉ span K (v '' (univ \ {i}))

Tactic:
h_in_span

Goal state after:
case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
h_in_span : v i ∈ span K (v '' (univ \ {i}))
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' s).encard ≤ s.encard

Tactic:
rw [s.eq_empty_of_isEmpty]; simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
I : Finset η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ I, x i = 1
h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
by
  induction I using Finset.induction_on generalizing x with
  | empty =>
    have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)
    exact this ▸ one_mem H
  | insert i I hnotMem ih =>
    have : x = Function.update x i 1 * Pi.mulSingle i (x i) := by
      ext j
      by_cases heq : j = i
      · subst heq
        simp
      · simp [heq]
    rw [this]
    clear this
    apply mul_mem (ih _ _ _) (by simp [h2]) <;> clear ih <;> intro j hj
    · by_cases heq : j = i
      · subst heq
        simp
      · simpa [heq] using h1 j (by simpa [heq] using hj)
    · have : j ≠ i := fun h => h ▸ hnotMem <| hj
      simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
      exact h2 _ (Finset.mem_insert_of_mem hj)

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

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Fintype.card ↑s < Fintype.card ↑t

Tactic:
exact Set.card_lt_card hsub

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ (insert a s).ncard ≤ s.ncard + 1

Tactic:
obtain hs | hs := s.finite_or_infinite
  · to_encard_tac; rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]; apply encard_insert_le
  rw [(hs.mono (subset_insert a s)).ncard]
  exact Nat.zero_le _

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ (sᶜ ∩ tᶜ).Nonempty

Tactic:
rw [← compl_union, nonempty_compl]

Goal state after:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
⊢ ∃ a, s = {a}

Tactic:
refine h.imp fun a ha ↦ ?_

Goal state after:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ s = {a}
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : f a = w * y
fb : f b = x * z
⊢ (conGen fun x y ↦ rel (f x) (f y)) a b

Tactic:
rw [← f.eq_symm_apply, map_mul] at fa fb
    rw [fa, fb]
    exact ConGen.Rel.mul (ih (by simp) (by simp)) (ih1 (by simp) (by simp))

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:
by simp [ne]

Goal state after:
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₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : f x = 0
⊢ R ∙ x ≤ f.ker

Tactic:
by rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case neg
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
hb✝ : b ∈ ⨅ i ∈ J, (proj i).ker
j : ι
hb : ∀ i ∈ J, b i = 0
h : j ∉ I
⊢ 0 ((pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) ⟨b, hb✝⟩) = b j

Tactic:
exact (hb _ <| (hu trivial).resolve_left h).symm

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 : ι
⊢ ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)

Tactic:
intro x y

Goal state after:
α : 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 : ι
x y : α
⊢ p (x ⊔ y) = max (p x) (p y)
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f ≤ partialSups g
⊢ ⨆ i, f i ≤ ⨆ i, g i

Tactic:
rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]
  exact iSup_mono h

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

Goal state before:
pp: case succ.hin.refine_2
ι : 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 + 1] i = j
hn_lt_ne : ∀ m < n + 1, succ^[m] i ≠ j
⊢ succ^[n] i ≠ succ^[n.succ] i

Tactic:
· rw [hn_eq]
        exact hn_lt_ne _ (Nat.lt_succ_self n)

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

Goal state before:
pp: α : Type u_2
inst✝⁵ : AddCommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedCancelAddMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x ↦ x + c) (Ioo a b) = Ioo (a + c) (b + c)

Tactic:
rw [← map_add_right_Ioo, map_eq_image, addRightEmbedding, Embedding.coeFn_mk]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p (f i \ (insert a✝ s✝).sup f)

Tactic:
rw [sup_insert, sup_comm, ← sdiff_sdiff]

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)
i : ι
hpi : p (f i)
a✝ : ι
s✝ : Finset ι
ht : a✝ ∉ s✝
IH : p (f i \ s✝.sup f)
⊢ p ((f i \ s✝.sup f) \ f a✝)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_3
f : ℕ → Set α
n : ℕ
⊢ ⋃ i ∈ range (n + 1), disjointed f i = (partialSups f) n

Tactic:
Nat.range_succ_eq_Iic,

Goal state after:
α : Type u_3
f : ℕ → Set α
n : ℕ
⊢ ⋃ i ∈ Iic n, disjointed f i = (partialSups f) n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

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

Tactic:
if_neg (not_le.mpr h_neg)

Goal state after:
case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
h_neg : toZ hι.some i < 0
⊢ pred^[(-toZ hι.some i).toNat] hι.some = i
Module: Mathlib.Algebra.BigOperators.Intervals

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

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

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (n + 1, 0) ::ₘ
      Multiset.map (⇑((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }))
        (antidiagonal n).val

Tactic:
exact Multiset.Nat.antidiagonal_succ'

Goal state after:
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 : c ∈ I
abc : b * a + c = 1
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1

Tactic:
refine ⟨mk _ b, Quot.sound ?_⟩

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 : c ∈ I
abc : b * a + c = 1
⊢ (Quotient.ringCon I).toSetoid ((fun x1 x2 ↦ x1 * x2) b a) 1
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1)).choose d + (d + (n + 1)).choose d.succ

Tactic:
← add_assoc

Goal state after:
case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ (d + n + 1).choose d + (d + n + 1).choose (d + 1) = (d + n + 1).choose d + (d + n + 1).choose d.succ
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
⊢ Injective ⇑f.prodOfFinsuppNat

Tactic:
intro x y

Goal state after:
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
⊢ f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst✝ : Subsingleton β
⊢ ⋂₀ range s ∈ f ↔ ∀ (i : β), s i ∈ f

Tactic:
sInter_eq_biInter,

Goal state after:
α : Type u
f : Filter α
β : Sort v
s : β → Set α
inst✝ : Subsingleton β
⊢ ⋂ i ∈ range s, i ∈ f ↔ ∀ (i : β), s i ∈ f
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c

Tactic:
by_cases h : c ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
h : c ∈ s
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c

case neg
α : Type u_1
β : Type u_2
f : Filter α
inst✝ : f.NeBot
c : β
s : Set β
h : c ∉ s
⊢ s ∈ map (fun x ↦ c) f ↔ s ∈ pure c
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_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ i, y ∈ (f i).sets

Tactic:
exact fun i hx hxy => ⟨i, mem_of_superset hx hxy⟩

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

Goal state before:

Tactic:
a ≤ comap (g ∘ f) c := hfg
    _ ≤ comap f b := by simpa [comap_comap] using comap_mono hg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ g = f

Tactic:
by
  refine ((comap_mono <| map_le_iff_le_comap.1 hψ).trans ?_).antisymm (map_le_iff_le_comap.1 hφ)
  rw [comap_comap, eq, comap_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
f : α → β
x : Filter α
y : ι → Filter β
⊢ Tendsto f x (⨅ i, y i) ↔ ∀ (i : ι), Tendsto f x (y i)

Tactic:
simp only [Tendsto, le_iInf_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:
rw [← map_neBot_iff, Filter.push_pull]

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeInf α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a
hg : ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ g a
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, b ≤ f a ⊓ g a

Tactic:
simp [eventually_and, hf, hg]

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b
hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b

Tactic:
simp [eventually_and, hf, hg]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
hsb : ∀ (i : ι), ∃ S, S.Finite ∧ span R S = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p

Tactic:
choose t htf hts using hsb

Goal state after:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ∃ S, S.Finite ∧ span R S = pi univ p
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
· refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
    exact smul_nonpos_of_nonneg_of_nonpos ha.le hb

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → x ∈ s → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
a b : α
hab : a ≤ b
t : Set α
ht : t ∈ s
hb : b ∈ t
⊢ ∃ y ∈ range fun x ↦ f ↑x ⋯, a ≤ y

Tactic:
simpa using ⟨t, ht, hab.trans (hf t ht b hb).le⟩

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : 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
⊢ d ⊆ s ∪ t → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t

Tactic:
hdu

Goal state after:
α : 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
⊢ d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s ∪ t
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
by
  rw [← neg_nonneg, ← smul_neg, smul_nonneg_iff_pos_imp_nonneg]; simp only [neg_pos, neg_nonneg]

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

Goal state before:
pp: a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + (c + 1) < a

Tactic:
← add_assoc

Goal state after:
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
h : b < a
c : Ordinal.{u_4}
hc : b + c < a
⊢ b + c + 1 < a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : (↑n✝).card = ↑n✝
⊢ (↑(n✝ + 1)).card = ↑(n✝ + 1)

Tactic:
simp only [card_add, card_one, Nat.cast_succ, *]

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

Goal state before:
pp: n : ℕ
⊢ (↑n).card = ↑n

Tactic:
induction n <;> [simp; simp only [card_add, card_one, Nat.cast_succ, *]]

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

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

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

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

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b = 0
⊢ b * (a / b) ≤ a

Tactic:
simp [b0]

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

Goal state before:
pp: case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b

Tactic:
rw [pow_succ', Nat.mul_comm b]

Goal state after:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)

Tactic:
rw [pow_succ', Nat.mul_comm b]

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

Goal state before:
pp: case inr.inr.add_one
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + c + 1) = a ^ b * a ^ (c + 1)

Tactic:
opow_add_one,

Goal state after:
case inr.inr.add_one
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ (b + c) * a = a ^ b * a ^ (c + 1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr.add_one
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ b * a ^ c * a = a ^ b * a ^ (c + 1)

Tactic:
opow_add_one,

Goal state after:
case inr.inr.add_one
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
IH : a ^ (b + c) = a ^ b * a ^ c
⊢ a ^ b * a ^ c * a = a ^ b * (a ^ c * a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
x : Fin n
⊢ (enum LT.lt) ⟨↑↑x, ⋯⟩ = x

Tactic:
by
  simp [← typein_inj LT.lt]

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

Goal state before:
pp: x : ℕ
⊢ (enum LT.lt) ⟨↑x, ⋯⟩ = x

Tactic:
by
  simp [← typein_inj LT.lt]

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

Goal state before:
pp: case inl
b x y : ℕ
h : x ≤ b ^ y
hb : 1 < b
⊢ clog b x ≤ y

pp: case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y

Tactic:
· rwa [clog_le_iff_le_pow hb]

Goal state after:
case inr
b x y : ℕ
h : x ≤ b ^ y
hb : 1 ≥ b
⊢ clog b x ≤ y
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ nfpFamily f a

Tactic:
← nfpFamily_fp (H i)

Goal state after:
case refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
hι : Nonempty ι
H : ∀ (i : ι), IsNormal (f i)
a b : Ordinal.{u}
h : b ≤ nfpFamily f a
i : ι
⊢ f i b ≤ f i (nfpFamily f a)