mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ : Nontrivial R
x✝ : ∃ f, Injective ⇑f
f : (Fin 2 → R) →ₗ[R] R
inj : Injective ⇑f
this : f ![0, 1] • ![1, 0] = f ![1, 0] • ![0, 1]
h₁ : f ![0, 1] = 0
h₂ : 0 = f ![1, 0]
⊢ 0 = 1

Tactic:
simpa using congr($(inj (h₁.trans h₂)) 1)

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

Goal state before:
pp: case neg
ι : 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 ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
refine ⟨s \ t, Finset.sdiff_subset, f, ?_, i, Finset.mem_sdiff.2 ⟨hi, hi'⟩, hfi⟩
    simpa [Finset.sdiff_sdiff_eq_self hst] using heq.symm

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.encard = 4
x : α
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
rw [← insert_eq_of_mem hx, ← insert_sdiff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (4 : ℕ∞) = 3 + 1),
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left, encard_eq_three] at h

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y z, x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : Nat.card ↥H = Nat.card G
⊢ H = ⊤

Tactic:
by
  have : Finite G := Nat.finite_of_card_ne_zero (h ▸ Nat.card_pos.ne')
  exact eq_top_of_le_card _ (Nat.le_of_eq h.symm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : (f '' s).ncard = s.ncard
hs : s.Finite
⊢ InjOn f s

Tactic:
by
  rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h
  exact hs.injOn_of_encard_image_eq h

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

Goal state before:
pp: case e'_3
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
hs.ncard

Goal state after:
case e'_3
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ 0 = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a

Tactic:
exact ha

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : s.Finite
⊢ s.Nontrivial ∧ s.Finite

Tactic:
rw [← Set.finite_coe_iff] at this

Goal state after:
case refine_1
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : Finite ↑s
⊢ s.Nontrivial ∧ s.Finite
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 : ∀ (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
⊢ ∀ (x y : H), f' (x * y) = f' x * f' y

Tactic:
simp_rw [hf₁.forall]
      rintro g₁ g₂
      exact (hf' _ _).1 ⟨g₁ * g₂, by simp [Prod.ext_iff, (hf' (f _).1 _).1 ⟨_, rfl⟩]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
⊢ (∑ i ∈ I, Pi.single i (b i)) i = b i

Tactic:
rw [Finset.sum_apply, ← Pi.single_eq_same i (b i)]

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
J : Set ι
I : Finset ι
hIJ : Codisjoint (↑I) J
b : (i : ι) → φ i
hb : ∀ i ∈ J, b i = 0
i : ι
⊢ ∑ c ∈ I, Pi.single c (b c) i = Pi.single i (b i) i
Module: Mathlib.Order.Interval.Set.SuccPred

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

Tactic:
by_cases ha : IsMax a

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b

case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b
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:
simp_rw [lsum_apply, sum_apply, comp_apply, proj_apply, apply_single, Fintype.sum_pi_single']

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
⊢ Iio (succ b) = Iic b

Tactic:
by
  ext x; rw [mem_Iio, mem_Iic, lt_succ_iff_of_not_isMax hb]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : ConditionallyCompleteLattice β
inst✝¹ : Finite ι
inst✝ : Nonempty ι
s : Set α
f : ι → α
g : α → β
hg : MonotoneOn g s
hs : ∀ (i : ι), f i ∈ s
j : ι
hj : f j = ⨆ i, f i
⊢ g (f j) = ⨆ i, g (f i)

Tactic:
exact le_antisymm (le_ciSup_of_le j le_rfl) <|
    ciSup_le fun i ↦ hg (hs i) (hs j) (hj ▸ le_ciSup f i)

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₂
s : Set M
t : Set M₂
hs : 0 ∈ s
ht : 0 ∈ t
⊢ span R (s ×ˢ t) = (span R s).prod (span R t)

Tactic:
refine le_antisymm (span_prod_le s t) ?_
  simp [Submodule.prod_le_iff, map_span]
  grind [span_mono]

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

Goal state before:
pp: case succ
ι : 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
⊢ pred^[n + 1] (succ^[n + 1] i) = i

Tactic:
rw [pred_succ_iterate_of_not_isMax]
      rw [Nat.succ_sub_succ_eq_sub, tsub_zero]
      suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this
      refine lt_of_le_of_ne ?_ ?_
      · rw [Function.iterate_succ_apply']
        exact le_succ _
      · rw [hn_eq]
        exact hn_lt_ne _ (Nat.lt_succ_self n)

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed ⇑(partialSups f)

Tactic:
← hsups,

Goal state after:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed ⇑(partialSups d)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case refine_1
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1), ⟨a.snd, a.fst - a.snd⟩ ∈ (range n).sigma fun m ↦ range (n - m)

Tactic:
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]

Goal state after:
case refine_1
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a b : ℕ), a < n → b ≤ a → b < n
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case refine_2
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m), ⟨a.fst + a.snd, a.fst⟩ ∈ (range n).sigma fun m ↦ range (m + 1)

Tactic:
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]

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

Goal state before:
pp: case refine_3
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    ⟨⟨a.snd, a.fst - a.snd⟩.fst + ⟨a.snd, a.fst - a.snd⟩.snd, ⟨a.snd, a.fst - a.snd⟩.fst⟩ = a

Tactic:
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]

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

Goal state before:
pp: case refine_4
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (n - m),
    ⟨⟨a.fst + a.snd, a.fst⟩.snd, ⟨a.fst + a.snd, a.fst⟩.fst - ⟨a.fst + a.snd, a.fst⟩.snd⟩ = a

Tactic:
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]

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

Goal state before:
pp: case refine_5
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ a ∈ (range n).sigma fun m ↦ range (m + 1),
    f a.snd (a.fst - a.snd) = f ⟨a.snd, a.fst - a.snd⟩.fst ⟨a.snd, a.fst - a.snd⟩.snd

Tactic:
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]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → ℕ → M
p : ℕ × ℕ
hp : p ∈ antidiagonal n
⊢ f p n = f p (p.1 + p.2)

Tactic:
by rw [mem_antidiagonal.mp hp]

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

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝² : Semiring α
I : Ideal α
a b : α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
h : 1 ∈ ⊥
⊢ 1 = 0

Tactic:
Submodule.mem_bot

Goal state after:
α : Type u
β : Type v
F : Type w
inst✝² : Semiring α
I : Ideal α
a b : α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
h : 1 = 0
⊢ 1 = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ Commute a b

Tactic:
have := mul_eq_zero_of_anticommute ha hab
  rw [this, zero_add] at hab
  rw [Commute, SemiconjBy, hab, this]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
by
  have ⟨M, hM, le⟩ := exists_le_maximal I hI
  have := hM.1.1
  rw [Ne, eq_top_iff, ← hs, span_le, Set.not_subset] at this
  have ⟨a, has, haM⟩ := this
  exact ⟨a, has, Set.disjoint_left.mpr fun x hx ⟨n, hn⟩ ↦
    haM (hM.isPrime.mem_of_pow_mem _ (le <| hn ▸ hx))⟩

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
h : x ∈ (LinearMap.toSpanSingleton R R e).ker
⊢ x * (1 - e) = x

Tactic:
by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]

Goal state after:
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:
by
  cases n with
  | zero => simp
  | succ n => simp [Int.alternating_sum_range_choose_eq_choose]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ IsDomain (R ⧸ I) ↔ I.IsPrime

Tactic:
by
  refine ⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩
  · have : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
    exact zero_ne_one
  · simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢
    have := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
    exact eq_zero_or_eq_zero_of_mul_eq_zero h

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

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
P : Ideal α
hP : P ≠ ⊥
⊢ (∃ p, Prime p ∧ P = span {p}) → P.IsPrime

Tactic:
by
    rintro ⟨p, hp, rfl⟩
    rwa [span_singleton_prime (by simp [hp.ne_zero])]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ ∀ (a : R ⧸ I), a • 0 = 0

Tactic:
rintro ⟨a⟩; exact congr_arg _ (smul_zero _)

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
α : Type u_5
inst✝ : Unique α
m : M
⊢ (finsuppUnique R M α).symm m = single default m

Tactic:
ext; simp [LinearEquiv.finsuppUnique, Equiv.funUnique, single, Pi.single,
    equivFunOnFinite, Function.update]

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

Goal state before:
pp: case a
α : Type u_1
B : FilterBasis α
⊢ B.filter ≤ generate B.sets

Tactic:
le_generate_iff

Goal state after:
case a
α : Type u_1
B : FilterBasis α
⊢ B.sets ⊆ B.filter.sets
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 (range Ici) ≤ generate (Ici '' s)

Tactic:
le_generate_iff

Goal state after:
case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ Ici '' s ⊆ (generate (range Ici)).sets
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:
le_generate_iff

Goal state after:
case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
⊢ range Ici ⊆ (generate (Ici '' s)).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:
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.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
⊢ ⋂ i, Iic (f i) = ∅ ↔ ¬BddBelow (range f)

Tactic:
by
  simp [not_bddBelow_iff, Set.eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
⊢ map f (generate U) ≤ generate ((fun x ↦ f ⁻¹' x) ⁻¹' U)

Tactic:
le_generate_iff

Goal state after:
α : Type u_1
β : Type u_2
U : Set (Set β)
f : β → α
⊢ (fun x ↦ f ⁻¹' x) ⁻¹' U ⊆ (map f (generate U)).sets
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ map f (generate ((fun x ↦ f ⁻¹' x) '' U)) ≤ generate U

Tactic:
le_generate_iff

Goal state after:
α : Type u_1
β : Type u_2
U : Set (Set α)
f : β → α
⊢ U ⊆ (map f (generate ((fun x ↦ f ⁻¹' x) '' U))).sets
Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂

Tactic:
by
    dsimp at hm
    rw [← sub_eq_zero, ← smul_sub] at hm
    simpa [hr.ne_zero, sub_eq_zero] using eq_zero_or_eq_zero_of_smul_eq_zero hm

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit (f a)
b : α
hb : b ⋖ a
⊢ False

pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
b : β
hb : b ⋖ f a
⊢ False

Tactic:
· rw [← f.apply_covBy_apply_iff] at hb
    exact h _ hb

Goal state after:
case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
h : IsSuccPrelimit a
b : β
hb : b ⋖ f a
⊢ False
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
⊢ IsCompactElement ⊤

Tactic:
← fg_iff_compact,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
⊢ ⊤.FG
Module: Mathlib.Order.DirSupClosed

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

Tactic:
simpa using hs.dirSupClosedOn.inter ht.dirSupClosedOn (D := .univ)

Goal state after:
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 ∨ a ≤ 0 ∧ 0 ≤ b

Tactic:
← neg_nonneg,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ -(a • b) ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
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:
← neg_nonneg,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ -(a • b) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
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 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
← neg_nonneg,

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

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
⊢ ∀ (a₁ : Submodule R V), Module.Finite R ↥a₁ → ∀ (a₂ : Submodule R V), Module.Finite R ↥a₂ → Module.Finite R ↥(a₁ ⊔ a₂)

Tactic:
intro S₁

Goal state after:
R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
S₁ : Submodule R V
⊢ Module.Finite R ↥S₁ → ∀ (a₂ : Submodule R V), Module.Finite R ↥a₂ → Module.Finite R ↥(S₁ ⊔ a₂)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b✝ b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : SMulPosReflectLT α β
inst✝ : SMulPosReflectLT α γ
b : β × γ
hb : 0 ≤ b
_a₁ _a₂ : α
h₁ : (_a₁ • b).1 ≤ (_a₂ • b).1
h₂ : (_a₁ • b).2 < (_a₂ • b).2
⊢ _a₁ < _a₂

Tactic:
· exact lt_of_smul_lt_smul_right h₂ hb.2

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
γ : Type w
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
ha : r a b
⊢ (PrincipalSeg.ofElement r a).top ∈ fun x ↦ r x b

Tactic:
exact ha

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

Goal state before:
pp: case right
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a✝ : α
b₁✝ b₂✝ : γ
h' : t b₁✝ b₂✝
⊢ Prod.Lex s t (f (a✝, b₁✝).1, (a✝, b₁✝).2) (f (a✝, b₂✝).1, (a✝, b₂✝).2)

Tactic:
· exact Prod.Lex.right _ h'

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b✝ : α
hb✝ : ∀ b < a, (Subtype.val ∘ ⇑(enum s hs)) b ≤ b✝
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
b : α
hb : b < a
c : α
hca : c < a
hbc : b < c
⊢ ↑((enum s hs) b) < sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

Tactic:
refine (H hbc).trans_le <| le_csSup bdd ⟨c, ?_⟩

Goal state after:
case refine_3
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (enum s hs))
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b✝ : α
hb✝ : ∀ b < a, (Subtype.val ∘ ⇑(enum s hs)) b ≤ b✝
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
b : α
hb : b < a
c : α
hca : c < a
hbc : b < c
⊢ c ∈ Iio a ∧ (Subtype.val ∘ ⇑(enum s hs)) c = (Subtype.val ∘ ⇑(enum s hs)) c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a / b ≤ c ↔ a < b * succ c

Tactic:
by
  rw [← lt_succ_iff, ← lt_mul_iff_div_lt b0]

Goal state after: