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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
t : Finset α
h : s ∩ mulSupport f = ↑t ∩ mulSupport f
⊢ ∀ {x : α}, f x ≠ 1 → (x ∈ s ↔ x ∈ t)

Tactic:
by
    intro x hxf
    rw [← mem_mulSupport] at hxf
    refine ⟨fun hx => ?_, fun hx => ?_⟩
    · refine ((mem_inter_iff x t (mulSupport f)).mp ?_).1
      rw [← Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩
    · refine ((mem_inter_iff x s (mulSupport f)).mp ?_).1
      rw [Set.ext_iff.mp h x, mem_inter_iff]
      exact ⟨hx, hxf⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hf : HasFiniteMulSupport f
⊢ s ∩ mulSupport f = ↑({i ∈ Finite.toFinset hf | i ∈ s}) ∩ mulSupport f

Tactic:
ext x
    simp [and_comm]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ ∏ᶠ (a : α), s.mulIndicator f a = 1

Tactic:
apply finprod_of_infinite_mulSupport

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
hs : (s ∩ mulSupport f).Infinite
⊢ (mulSupport (s.mulIndicator f)).Infinite
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t
x : α
⊢ x ∈ s ∩ mulSupport f ↔ x ∈ t ∩ mulSupport f

Tactic:
exact and_congr_left (h x)

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

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ (Fintype.linearCombination R v) (Pi.single i r) = r • v i

Tactic:
Fintype.linearCombination_apply,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Fintype α
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
inst✝ : DecidableEq α
i : α
r : R
⊢ ∑ i_1, Pi.single i r i_1 • v i_1 = r • v i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
by
  rw [← finprod_mem_union_inter' hs ht, disjoint_iff_inter_eq_empty.1 hst, finprod_mem_empty,
    mul_one]

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
⊢ x ∈ insert a s → x ∈ s

Tactic:
rintro (rfl | hxs)

Goal state after:
case inl
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
x : α
hx : x ∈ mulSupport f
h : x ∉ s → f x = 1
⊢ x ∈ s

case inr
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
s : Set α
h : a ∉ s → f a = 1
x : α
hx : x ∈ mulSupport f
hxs : x ∈ s
⊢ x ∈ s
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
rcases i.lt_or_ge n with hi | hi

Goal state after:
case inl
n i : ℕ
hi : i < n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

case inr
n i : ℕ
hi : i ≥ n
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i, (fun i ↦ ↑(t i)) i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a

Tactic:
classical
    rw [← biUnion_univ, ← Finset.coe_univ, ← Finset.coe_biUnion, finprod_mem_coe_finset,
      Finset.prod_biUnion]
    · simp only [finprod_mem_coe_finset, finprod_eq_prod_of_fintype]
    · exact fun x _ y _ hxy => Finset.disjoint_coe.1 (h hxy)

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

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx),

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
⊢ f a * ∏ i ∈ Finite.toFinset hf \ {a}, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
inst✝² : Semiring R₂
inst✝¹ : Module R₂ M'
inst✝ : SMulCommClass R R₂ M'
v : ι → M'
hv : LinearIndependent R v
x✝¹ x✝ : M
hab : ((b.constr R₂) v) x✝¹ = ((b.constr R₂) v) x✝
⊢ (linearCombination R v) (b.repr x✝¹) = (linearCombination R v) (b.repr x✝)

Tactic:
by
    simpa [constr_def] using hab

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_2 : 1 < x
this : x ≤ 1
⊢ x = 1

Tactic:
exact (not_lt_of_ge this x_2).rec

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inr.inl
x y z : ℕ∞
y_0 : y ≠ 0
z_0 : z ≠ 0
x_0 : x < 1
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rw [Order.lt_one_iff.1 x_0, zero_epow y_0, zero_epow z_0, zero_epow (mul_ne_zero y_0 z_0)]

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
inst✝ : Fintype ι
⊢ (∀ ⦃a₁ a₂ : ι → R⦄, (Fintype.linearCombination R v) a₁ = (Fintype.linearCombination R v) a₂ → a₁ = a₂) ↔
    ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i

Tactic:
Fintype.linearCombination_apply,

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
inst✝ : Fintype ι
⊢ (∀ ⦃a₁ a₂ : ι → R⦄, ∑ i, a₁ i • v i = ∑ i, a₂ i • v i → a₁ = a₂) ↔
    ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g 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 ∈ Ico (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Ico a b, f (Fin.cast h i)

Tactic:
by
  simp [← map_finCongr_Ico]

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

Goal state before:
pp: case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ a ^ c < a ^ b

Tactic:
Nat.pow_lt_pow_iff_right ha1

Goal state after:
case inr.inr.inr.inl
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : c < b
⊢ c < b
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case refine_2.inr.inr
G : Type u_3
inst✝ : Monoid G
n : ℕ
g : Fin (n + 1) → G
a i✝ : Fin (n + 1)
i : Fin n
hi : partialProd (a.contractNth (fun x1 x2 ↦ x1 * x2) g) i.castSucc = partialProd g (a.succ.succAbove i.castSucc)
h : ↑a < ↑i
⊢ partialProd g (a.succ.succAbove i.castSucc) * a.contractNth (fun x1 x2 ↦ x1 * x2) g i =
    partialProd g (a.succAbove i).castSucc * g (a.succAbove i)

Tactic:
rw [succAbove_of_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h,
        castSucc_succ] <;>
      simp only [le_def, val_succ, val_castSucc] <;>
      lia

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ #α < ℵ₀

Tactic:
exact Cardinal.lt_aleph0_of_finite _

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

Goal state before:
pp: α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
⊢ ∑ i, (-1) ^ ↑i • d i = 0

Tactic:
have h₁ : ∑ i : Fin (n + 2), (-1 : ℤ) ^ i.val • d i =
      d 0 +
      ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • (d (Fin.castSucc i).succ) +
      (-1 : ℤ) ^ (n + 1) • d (Fin.last (n + 1)) := by
    rw [Fin.sum_univ_succ, Fin.sum_univ_castSucc]
    simp [add_assoc]
  have h₂ : ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • (r (Fin.castSucc i) + r (Fin.succ i)) =
      ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • r (Fin.castSucc i) +
      ∑ i : Fin n, (-1 : ℤ) ^ (i.val + 1) • r (Fin.succ i) := by
    simp_rw [zsmul_add, Finset.sum_add_distrib]
  have h₃ := Fin.sum_univ_castSucc fun i ↦ (-1 : ℤ) ^ i.val • r i
  simp_all [Fin.sum_univ_succ, pow_succ']
  grind

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
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 ι
h : ∀ (t : Finset ↑↑s) (f : ↑↑s → R), ∑ i ∈ t, f i • v ↑i = ∑ i ∈ tᶜ, f i • v ↑i → ∀ (i : ↑↑s), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
⊢ ∑ i with ↑i ∈ t, (f ∘ Subtype.val) i • v ↑i = ∑ i ∈ {i | ↑i ∈ t}ᶜ, (f ∘ Subtype.val) i • v ↑i

Tactic:
simp only [Finset.compl_filter, Finset.sum_filter, Function.comp_apply, Finset.coe_sort_coe]
    rw [Finset.sum_coe_sort s fun i => if i ∈ t then f i • v i else 0,
      Finset.sum_coe_sort s fun i => if i ∉ t then f i • v i else 0]
    simpa [Finset.inter_eq_right.2 ht, Finset.sum_ite, Finset.filter_notMem_eq_sdiff]

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

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ ¬LinearIndependent R v ↔ ∃ s g, ∑ i ∈ s, g i • v i = 0 ∧ ∃ i ∈ s, g i ≠ 0

Tactic:
by
  rw [linearIndependent_iff']
  simp only [exists_prop, not_forall]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hc : t.encard < s.encard
hf : MapsTo f s t
⊢ ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂

Tactic:
by
  contrapose! hc
  suffices Function.Injective (hf.restrict f) by
    let f' : s ↪ t := ⟨hf.restrict, this⟩
    exact f'.encard_le
  simpa only [hf.restrict_inj, not_imp_not] using! hc

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
⊢ s.ncard = n

Tactic:
suffices himage : s = f' '' Set.univ by
    rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]
    exact InjOn.ncard_image <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h

Goal state after:
α : Type u_1
s : Set α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
f' : Fin n → α := fun i ↦ f ↑i ⋯
⊢ s = f' '' univ
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ t.encard

Tactic:
(ht.finite_of_encard_le hle).cast_ncard_eq

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ s.encard ≤ t.encard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ a • s
b : α
hb : b ∈ s
h : (fun x ↦ a • x) b = x
⊢ a⁻¹ * x ∈ s

Tactic:
by simp [h.symm, hb]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ op a • s
b : α
hb : b ∈ s
h : (fun x ↦ op a • x) b = x
⊢ x * a⁻¹ ∈ s

Tactic:
by simp [h.symm, hb]

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)
a : (i : ι) → φ i
h : a ∈ ⨅ i, (proj i).ker
⊢ a ∈ ⊥

Tactic:
simp only [mem_iInf, mem_ker, proj_apply] at h
      exact (mem_bot _).2 (funext fun i => h i)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b

Tactic:
· ext x
    rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) (pred b) = Ico a b

Tactic:
Ioc_pred_right_eq_Ioo,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (pred a) b = Ico a b
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

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

Tactic:
by
  simpa [succ_eq_add_one] using Ico_succ_right_eq_Icc a b

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x ↦ x + d) (Ioo a b) (Ioo (a + d) (b + d))

Tactic:
by
  rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]
  exact (Ioi_add_bij a d).inter_mapsTo (by simp [MapsTo]) fun x hx => lt_of_add_lt_add_right hx.2

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
mul_prod_Ico_eq_prod_Icc h

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ ∏ x ∈ Icc a b, f x = ∏ x ∈ Icc a b, f x
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i : ι
⊢ ∀ x ∈ Set.Ioi i, i ≤ x

Tactic:
exact fun x hx ↦ le_of_lt hx

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]
    exact hdiff IH

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

Goal state before:
pp: case inr.inl
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : toZ i0 i ≤ toZ i0 j
hi : i < i0
hj : i0 ≤ j
⊢ i ≤ j

Tactic:
exact hi.le.trans hj

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

Goal state before:
pp: case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ 1 = ∏ k ∈ ∅, f (m + k)

Tactic:
prod_empty

Goal state after:
case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ 1 = 1
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
hf' : f = f' ∘ ⇑R
⊢ disjointed f' ∘ ⇑R ≤ f

Tactic:
intro n
    simpa only [hf'] using! disjointed_le f' (R n)

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
x : α
⊢ span {0, x} = span {x}

Tactic:
span_insert_zero

Goal state after:
α : Type u
inst✝ : Semiring α
x : α
⊢ span {x} = span {x}
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝¹ : Semiring α
I : Ideal α
a b : α
inst✝ : Nontrivial α
⊢ Nontrivial (Ideal α)

Tactic:
rcases @exists_maximal α _ _ with ⟨M, hM, _⟩

Goal state after:
α : Type u
β : Type v
F : Type w
inst✝¹ : Semiring α
I : Ideal α
a b : α
inst✝ : Nontrivial α
M : Ideal α
hM : M ≠ ⊤
right✝ : ∀ (b : Ideal α), M < b → b = ⊤
⊢ Nontrivial (Ideal α)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝ : α
⊢ (∃ a b, a * (x + y) + b * y = x✝) ↔ ∃ a b, a * x + b * y = x✝

Tactic:
exact ⟨fun ⟨a, b, h⟩ => ⟨a, b + a, by rw [add_comm b, add_mul, ← add_assoc, ← mul_add, h]⟩,
    fun ⟨a, b, h⟩ => ⟨a, b - a, by rw [mul_add, sub_mul, add_add_sub_cancel, h]⟩⟩

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

Goal state before:
pp: case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))

Tactic:
map_add_right_Ico,

Goal state after:
case e'_3.h
n k : ℕ
⊢ Icc k (n + k) = Ico (0 + k) (n + 1 + k)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
i : ι
s : Set α
hs : s ∈ f i
⊢ p s

Tactic:
by simpa using ins hs uni

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ (f '' sᶜᶜ)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l

Tactic:
compl_compl

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ (f '' s)ᶜ ∈ l ↔ (f '' s)ᶜ ∈ l
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → 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'.fst ii'.snd) fun ii' ↦ s ii'.fst ii'.snd

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ (∃ t, tᶜ ∈ f ∧ m '' t = sᶜᶜ) ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s

Tactic:
compl_compl

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
h : sᶜᶜ ∈ f
⊢ s ∈ f

Tactic:
compl_compl

Goal state after:
α : Type u
f : Filter α
s : Set α
h : s ∈ f
⊢ s ∈ f
Module: Mathlib.Order.Filter.AtTopBot.Tendsto

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto f l (comap e atTop)

Tactic:
tendsto_comap_iff

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
e : β → γ
l : Filter α
hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂
hu : ∀ (c : γ), ∃ b, c ≤ e b
⊢ Tendsto (e ∘ f) l atTop ↔ Tendsto (e ∘ f) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
rw [frequently_atTop'] at h

Goal state after:
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ⋃ i ∈ s, Iio i = univ

Tactic:
simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop]
    intro x
    obtain ⟨y, hy⟩ := exists_gt x
    obtain ⟨z, hz, hz'⟩ := hs y
    exact ⟨z, hz, hy.trans_le hz'⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
hM' : M'.FG
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
⊢ ∃ n, M' = N n

Tactic:
obtain ⟨S, hS⟩ := hM'
  have (s : S) : ∃ n, (s : M) ∈ N n :=
    (mem_iSup_of_chain N s).mp (by simpa [H, ← hS] using subset_span s.prop)
  choose f hf using this
  use S.attach.sup f
  apply le_antisymm
  · rw [← hS, span_le]
    intro s hs
    exact N.monotone' (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)
  · rw [← H]
    exact le_iSup ..

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupClosedOn D sᶜᶜ ↔ DirSupClosedOn D s

Tactic:
compl_compl

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupClosedOn D s ↔ DirSupClosedOn D s
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupClosed sᶜᶜ ↔ DirSupClosed s

Tactic:
compl_compl

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupClosed s ↔ DirSupClosed s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case intro
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✝ : Finite M
val✝ : Fintype M
⊢ Module.Finite R M

Tactic:
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ, span_univ]⟩⟩

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ span R (image2 (fun x1 x2 ↦ x1 • x2) ↑s ↑t) = ⊤

Tactic:
image2_smul,

Goal state after:
R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ span R (↑s • ↑t) = ⊤
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ ≤ a • b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
by simpa only [smul] using hf.2 h

Goal state after: