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

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down

Tactic:
rw [finprod, dif_pos hf]

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
hf : HasFiniteMulSupport (f ∘ PLift.down)
s : Finset (PLift α)
hs : Finite.toFinset hf ⊆ s
⊢ ∏ i ∈ Finite.toFinset hf, f i.down = ∏ i ∈ s, f i.down
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ioo i j = Ioo ↑i ↑j

Tactic:
by
  rw [← preimage_val_Ioo_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans j.is_lt

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) ⁻¹' uIoo (i.addNat m) (j.addNat m) = uIoo i j

Tactic:
simp [uIoo, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

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

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ (fun x ↦ x.addNat m) '' uIoo i j = uIoo (i.addNat m) (j.addNat m)

Tactic:
simp [uIoo, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

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

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1

Tactic:
by_cases H : (fun _ : α ↦ (0 : M)).HasFiniteMulSupport

Goal state after:
case pos
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : HasFiniteMulSupport fun x ↦ 0
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1

case neg
M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : ¬HasFiniteMulSupport fun x ↦ 0
⊢ ∏ᶠ (x : α), 0 ≤ ∏ᶠ (x : α), 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ f a ∣ finprod f

Tactic:
rw [notMem_mulSupport.mp ha]

Goal state after:
case neg
α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
ha : a ∉ mulSupport f
⊢ 1 ∣ finprod f
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin 1
⊢ (finRotate 1) i = i + 1

Tactic:
exact @Subsingleton.elim (Fin 1) _ _ _

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑((finCycle k.succ) i) = ↑((finRotate (n + 1)) ((⇑(finRotate (n + 1)))^[↑k] i))

Tactic:
← ih,

Goal state after:
case succ
n✝ n : ℕ
i : Fin (n + 1)
k : Fin n
ih : (finCycle k.castSucc) i = (⇑(finRotate (n + 1)))^[↑k] i
⊢ ↑((finCycle k.succ) i) = ↑((finRotate (n + 1)) ((finCycle k.castSucc) i))
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n m : ℕ
h : n = m
f : Fin m → M
a b : Fin n
⊢ ∏ i ∈ uIcc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ uIcc a b, f (Fin.cast h i)

Tactic:
by
  simp [← map_finCongr_uIcc]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : MulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v

Tactic:
convert! h.group_smul (fun i ↦ (w i)⁻¹)

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : MulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
w : ι → G
h : LinearIndependent R (w • v)
⊢ v = (fun i ↦ (w i)⁻¹) • w • v
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a : ℕ
⊢ a ≡ 0 [MOD n] ↔ n ∣ a

Tactic:
by rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
ha : a • v i ∈ span R (v '' (univ \ {i}))
⊢ a = 0

Tactic:
rw [Finsupp.span_image_eq_map_linearCombination, mem_map] at ha

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
a : R
ha : ∃ y ∈ Finsupp.supported R R (univ \ {i}), (Finsupp.linearCombination R v) y = a • v i
⊢ a = 0
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a : Fin (0 ^ (n + 1))
⊢ ↑a / 0 ^ ↑b % 0 < 0

Tactic:
zero_pow n.succ_ne_zero

Goal state after:
case succ.zero
ι : Type u_1
M : Type u_2
n : ℕ
b : Fin (n + 1)
a✝ : Fin (0 ^ (n + 1))
a : Fin 0
⊢ ↑a✝ / 0 ^ ↑b % 0 < 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ ∑ x ∈ s with x ∈ range Sum.inl ∨ x ∈ range Sum.inr, g x • v x = 0

Tactic:
simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]

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
⊢ (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      a [MOD n] ∧
    (match n.xgcd m with
      | (c, d) => ((↑n * c * ↑b + ↑m * d * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat) ≡
      b [MOD m]

Tactic:
by
        rw [xgcd_val]
        dsimp
        rw [modEq_iff_dvd, modEq_iff_dvd,
          Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))]
        have hnonzero : (gcd n m : ℤ) ≠ 0 := by
          norm_cast
          rw [Nat.gcd_eq_zero_iff, not_and]
          exact fun _ => hm
        have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _
        have := gcd_eq_gcd_ab n m
        constructor <;> rw [Int.emod_def, ← sub_add] <;>
            refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _) <;>
          try norm_cast
        · rw [← sub_eq_iff_eq_add'] at this
          rw [← this, Int.sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← Int.mul_sub,
            Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left _ hnonzero,
            Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, Int.dvd_neg, mul_assoc]
          · exact dvd_mul_right _ _
          norm_cast
          exact dvd_mul_right _ _
        · exact dvd_lcm_left n m
        · rw [← sub_eq_iff_eq_add] at this
          rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
            zero_add, mul_assoc]
          · exact dvd_mul_right _ _
          · exact hcoedvd _
        · exact dvd_lcm_right n m

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

Goal state before:
pp: case succ
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
⊢ (take (i + 1) (ofFn f)).prod = ∏ j with ↑j < i + 1, f j

Tactic:
by_cases h : i < n
    · have : i < length (ofFn f) := by rwa [length_ofFn]
      rw [prod_take_succ _ _ this]
      have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by grind
      grind
    · have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
      have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
        intro j
        have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
        simp [this, lt_trans this (Nat.lt_succ_self _)]
      simp [← A, B, IH]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
lhs
    rw [xgcdAux]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| if _hr : r = 0 then (r', s', t')
  else
    have q := r' / r;
    have x := ⋯;
    xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
⊢ lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')

Tactic:
refine _root_.lift_rank_le_of_injective_injectiveₛ i j hi hj fun r _ ↦ ?_
  have := congr($hc r)
  simp only [RingHom.coe_comp, comp_apply] at this
  simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]

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

Goal state before:
pp: R : Type u
R' : Type u'
M : Type v
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : Module R' M
inst✝³ : SMulWithZero R R'
inst✝² : IsScalarTower R R' M
inst✝¹ : FaithfulSMul R R'
inst✝ : IsScalarTower R R' R'
⊢ Module.rank R' M ≤ Module.rank R M

Tactic:
rw [Module.rank, Module.rank]
  exact ciSup_le' fun ⟨s, hs⟩ ↦ le_ciSup_of_le Cardinal.bddAbove_of_small
    ⟨s, hs.restrict_scalars (by simpa [← faithfulSMul_iff_injective_smul_one])⟩ le_rfl

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : Finite ↑(s ∪ t)
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
finite_coe_iff,

Goal state after:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
Module: Mathlib.Data.Set.Card

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

Tactic:
ncard_sdiff_singleton_of_mem h

Goal state after:
case pos
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.ncard - 1 ≤ s.ncard - 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : t.Finite
h' : ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
⊢ False

Tactic:
simp only [Ne, not_exists, not_and, not_imp_not] at h'

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
hc : t.ncard < s.ncard
f : α → β
hf : ∀ a ∈ s, f a ∈ t
ht : t.Finite
h' : ∀ x ∈ s, ∀ x_1 ∈ s, f x = f x_1 → x = x_1
⊢ False
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ⇑(leftRel s) = LeftCosetEquivalence ↑s

Tactic:
by
  ext
  rw [leftRel_eq]
  exact (leftCoset_eq_iff s).symm

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ (leftRel (s.subgroupOf t)) ⟨(f (Quotient.mk'' b))⁻¹ * b, ⋯⟩ ⟨(f (Quotient.mk'' c))⁻¹ * c, ⋯⟩

Tactic:
rw [leftRel_apply]

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ ⟨(f (Quotient.mk'' b))⁻¹ * b, ⋯⟩⁻¹ * ⟨(f (Quotient.mk'' c))⁻¹ * c, ⋯⟩ ∈ s.subgroupOf t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h₁ : {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe
h₂ : SetLike.coe ⁻¹' {t | t ⊆ ↑s ∧ t.ncard = n} = ↑(Finset.powersetCard n s)
⊢ {t | t ⊆ ↑s ∧ t.ncard = n}.ncard = (↑s).ncard.choose n

Tactic:
grind [ncard_coe_finset, ncard_preimage_of_injective_subset_range, Finset.card_powersetCard]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard = Nat.card α - s.ncard

Tactic:
rw [← ncard_add_ncard_compl s hs hsc, Nat.add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
s : Set α
n : ℕ
h : Nat.card α = n + s.ncard
⊢ sᶜ.ncard = n

Tactic:
← ncard_compl_add_ncard s,

Goal state after:
α : Type u_1
inst✝ : Finite α
s : Set α
n : ℕ
h : sᶜ.ncard + s.ncard = n + s.ncard
⊢ sᶜ.ncard = n
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ c : Con M
d : Con N
e : M ≃* N
h : c = comap ⇑e ⋯ d
⊢ ∀ (x y : c.Quotient),
    (Quotient.congr ↑e ⋯).toFun (x * y) = (Quotient.congr ↑e ⋯).toFun x * (Quotient.congr ↑e ⋯).toFun y

Tactic:
rintro ⟨x⟩ ⟨y⟩; exact congrArg toQuotient (e.map_mul x y)

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case disjoint
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₂
⊢ Disjoint (inl R M M₂).range (inr R M M₂).range

Tactic:
rw [disjoint_def]
    rintro ⟨_, _⟩ ⟨x, hx⟩ ⟨y, hy⟩
    simp only [Prod.ext_iff, inl_apply, inr_apply] at hx hy ⊢
    exact ⟨hy.1.symm, hx.2.symm⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_3
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
⊢ (codRestrict (⨅ i ∈ J, (proj i).ker) (pi fun i ↦ if h : i ∈ I then proj ⟨i, h⟩ else 0) ⋯ ∘ₗ
      pi fun i ↦ proj ↑i ∘ₗ (⨅ i ∈ J, (proj i).ker).subtype) =
    id

Tactic:
ext1 ⟨b, hb⟩
    apply Subtype.ext
    ext j
    have hb : ∀ i ∈ J, b i = 0 := by
      simpa only [mem_iInf, mem_ker, proj_apply] using (mem_iInf _).1 hb
    simp only [comp_apply, pi_apply, id_apply, codRestrict_apply]
    split_ifs with h
    · rfl
    · exact (hb _ <| (hu trivial).resolve_left h).symm

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : 0 + g z = 0
this : f y = 0
⊢ f y = 0 ∧ g z = 0

Tactic:
simpa [this] using h

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

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
s : Set α
a : α
hs : s.Nonempty
hs' : s.Finite
hs'' : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b

Tactic:
by
  have := hs.to_subtype
  have := hs'.to_subtype
  simp [sSup_eq_iSup', le_iSup_iff_of_directed hs''.directed_val]

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

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGLB (Set.Ioi i) k
⊢ IsGLB (Set.Ioc i j) k

Tactic:
IsGLB,

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j k : ι
hij_lt : i < j
h : IsGreatest (lowerBounds (Set.Ioi i)) k
⊢ IsGreatest (lowerBounds (Set.Ioc i j)) k
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : IsGLB (Set.Ioi i) (succFn i)
⊢ succFn i ≤ j

Tactic:
IsGLB,

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : IsGreatest (lowerBounds (Set.Ioi i)) (succFn i)
⊢ succFn i ≤ j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
⊢ ∃ n, succ^[n] i = j

Tactic:
by_contra! h

Goal state after:
case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMonoid A
inst✝ : HasMulAntidiagonal A
n : A
xy : A × A
⊢ xy.swap ∈ mulAntidiagonal n ↔ xy ∈ mulAntidiagonal n

Tactic:
simp [mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CommMonoid A
inst✝ : HasMulAntidiagonal A
n : A
x✝ : A × A
a b : A
⊢ (a, b) ∈ map (Equiv.prodComm A A).toEmbedding (mulAntidiagonal n) ↔ (a, b) ∈ mulAntidiagonal n

Tactic:
simp [mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : CancelMonoid A
inst✝ : HasMulAntidiagonal A
p q : A × A
n : A
hp : p ∈ mulAntidiagonal n
hq : q ∈ mulAntidiagonal n
⊢ p = q ↔ p.1 = q.1

Tactic:
refine ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((mul_right_inj q.fst).mp ?_)⟩
  rw [mem_mulAntidiagonal] at hp hq
  rw [hq, ← h, hp]

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

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ n - (n - j) = j

Tactic:
tsub_tsub_cancel_of_le (this _ jm)

Goal state after:
case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
i : ℕ
left✝¹ : k ≤ i
im : i < m
j : ℕ
left✝ : k ≤ j
jm : j < m
Hij : n - i = n - j
⊢ j = j
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ (toZ ⊥ (succ^[↑n] ⊥)).toNat ≤ ↑n

pp: case refine_2
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat

Tactic:
· rw [Int.toNat_le]
      exact toZ_iterate_succ_le _

Goal state after:
case refine_2
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
n : ↥(Finset.range ((toZ ⊥ ⊤).toNat + 1))
⊢ ↑n ≤ (toZ ⊥ (succ^[↑n] ⊥)).toNat
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
⊢ ∀ {a b : ι},
    { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by
    intro i j
    simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Int.toNat_le]
    rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]

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

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

Tactic:
rw [Ideal.span_insert, sup_eq_left, span_singleton_le_span_singleton]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m ∈ antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)

Tactic:
Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),

Goal state after:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ k ∈ range n.succ, n.choose k • (x ^ k * y ^ (n - k))
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose (2 * m + 1 - i) =
    ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Tactic:
sum_Ico_reflect _ _ (by lia)

Goal state after:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i +
      ∑ j ∈ Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), (2 * m + 1).choose j =
    ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i
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
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
⊢ ∀ (a₁ : R) (a₂ : ι → R) (b₁ : R) (b₂ : ι → R),
    (Submodule.quotientRel I) a₁ b₁ →
      (Submodule.quotientRel (pi fun x ↦ I)) a₂ b₂ → Submodule.Quotient.mk (a₁ • a₂) = Submodule.Quotient.mk (b₁ • b₂)

Tactic:
by
      intro c₁ m₁ c₂ m₂ hc hm
      apply Ideal.Quotient.eq.2
      rw [Submodule.quotientRel_def] at hc hm
      intro i
      exact I.mul_sub_mul_mem hc (hm i)

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

Goal state before:
pp: α : Type u_1
B : FilterBasis α
⊢ B.filter = ⨅ s, 𝓟 ↑s

Tactic:
by
  have : Directed (· ≥ ·) fun s : B.sets => 𝓟 (s : Set α) := by
    rintro ⟨U, U_in⟩ ⟨V, V_in⟩
    rcases B.inter_sets U_in V_in with ⟨W, W_in, W_sub⟩
    use ⟨W, W_in⟩
    simp only [le_principal_iff, mem_principal]
    exact subset_inter_iff.mp W_sub
  ext U
  simp [mem_filter_iff, mem_iInf_of_directed this]

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

Goal state before:
pp: α : Type u_1
a : α
p : α → Prop
⊢ (∃ᶠ (x : α) in pure a, p x) ↔ p a

Tactic:
simp [Filter.Frequently]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ￢𝓟 s = 𝓟 sᶜ

Tactic:
by
  simpa [← compl_eq_univ_sdiff] using @principal_sdiff_principal _ univ s

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

Goal state before:
pp: α : Type u
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f

Tactic:
simp only [mem_inf_principal', imp_iff_not_or, ofPred_or, compl_def, ofPred_mem_eq]

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

Goal state before:
pp: α : Type u
p : α → Prop
f : Filter α
⊢ (¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x

Tactic:
simp [Filter.Frequently]

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

Goal state before:
pp: α : Type u
p : α → Prop
⊢ (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ x, p x

Tactic:
simp [Filter.Frequently]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g}.seq s ∈ (pure g).seq f

Tactic:
apply seq_mem_seq _ hs

Goal state after:
α : Type u_1
β : Type u_2
g : α → β
f : Filter α
s : Set α
hs : s ∈ f
⊢ {g} ∈ pure g
Module: Mathlib.Algebra.Group.Shrink

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Mul α
x y : Shrink.{v, u_2} α
⊢ (equivShrink α).symm (x * y) = (equivShrink α).symm x * (equivShrink α).symm y

Tactic:
simp [Equiv.mul_def]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Small.{v, u_2} α
inst✝ : Mul α
x y : α
⊢ (equivShrink α) (x * y) = (equivShrink α) x * (equivShrink α) y

Tactic:
simp [Equiv.mul_def]

Goal state after: