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

Goal state before:
pp: α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
⊢ ∏ᶠ (i : α), f i ≠ 0

Tactic:
by_cases h₂ : Set.Finite f.mulSupport

Goal state after:
case pos
α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
h₂ : (mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i ≠ 0

case neg
α : Type u_1
M₀ : Type u_7
inst✝² : CommMonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
f : α → M₀
h : ∀ (i : α), f i ≠ 0
h₂ : ¬(mulSupport f).Finite
⊢ ∏ᶠ (i : α), f i ≠ 0
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∑ a ∈ s with f a ≠ 0, f a • g a = ∑ a ∈ s, f a • g a

Tactic:
Finset.sum_filter_of_ne

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∑ x ∈ s, f x • g x = ∑ a ∈ s, f a • g a

α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ ∀ x ∈ s, f x • g x ≠ 0 → f x ≠ 0
Module: Mathlib.Data.Fintype.Fin

Goal state before:
pp: n : ℕ
⊢ map valEmbedding univ = Iio n

Tactic:
by
  ext
  simp [orderIsoSubtype.symm.surjective.exists, OrderIso.symm]

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

Goal state before:
pp: n : ℕ
x : { x // x ≠ Fin.last n }
⊢ (finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯

Tactic:
rw [← Option.some_inj]
  simp [finSuccAboveEquiv]

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

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

Tactic:
obtain rfl | h := Fin.eq_or_lt_of_le i.le_last
    · simp [finRotate_last]
    · cases i
      simp only [Fin.lt_def, Fin.val_last] at h
      simp [finRotate_of_lt h, Fin.add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ h)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset (α × β)
f : α × β → M
⊢ ∏ᶠ (ab : α × β) (_ : ab ∈ s), f ab = ∏ᶠ (a : α) (b : β) (_ : (a, b) ∈ s), f (a, b)

Tactic:
rw [finprod_mem_finset_product']
    simp

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
n : ℕ
h : a ≡ b [PMOD p]
⊢ n • a ≡ n • b [PMOD n • p]

Tactic:
rw [modEq_iff_nsmul] at *
  rcases h with ⟨k, l, h⟩
  use k, l
  rw [← mul_nsmul, mul_nsmul', ← nsmul_add, h, nsmul_add, ← mul_nsmul, mul_nsmul']

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

Goal state before:
pp: case refine_1
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ ↑m ∣ ↑c * ↑b - ↑c * ↑a

Tactic:
exact modEq_iff_dvd.mp h

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

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
by
  apply cancel_left_div_gcd hm
  simpa [mul_comm] using h

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
this :
  ∀ (n : Fin m → ℕ) (nn : ℕ) (f : (i : Fin m) → Fin (n i)) (fn : Fin nn),
    ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn
⊢ ∑ i, ↑(f i.castSucc) * ∏ j, n (Fin.castLE ⋯ j) + ↑(f (Fin.last m)) * ∏ j, n (Fin.castLE ⋯ j) <
    (∏ i, n i.castSucc) * n (Fin.last m)

Tactic:
by
        solve_by_elim

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x : ℤ
h✝ : ¬0 ≤ x
h : ¬n ∣ x.natAbs
⊢ ¬↑n ∣ x

Tactic:
rwa [← Int.natCast_dvd] at h

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
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ f i = g i

Tactic:
apply (not_le.1 hi').le.antisymm

Goal state after:
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
this✝ : Sub R := ⋯
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ g i ≤ f i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hdj : Disjoint s t
⊢ LinearIndepOn R id (s ∪ t) ↔ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t)

Tactic:
by
  rw [linearIndepOn_union_iff hdj, image_id, image_id]

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

Goal state before:
pp: case refine_2
ι : 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 ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ i ∈ t₁ᶜ, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i

Tactic:
← Finset.sum_subset ht₁t₂.le_compl_left

Goal state after:
case refine_2
ι : 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 ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∑ i ∈ t₁, (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) • v i = ∑ x ∈ t₂, (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x

case refine_2
ι : 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 ι
h : ∀ (t : Finset ι) (f : ι → R), ∑ i ∈ t, f i • v i = ∑ i ∈ tᶜ, f i • v i → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : ∑ i ∈ t₁, f i • v i = ∑ i ∈ t₂, f i • v i
⊢ ∀ x ∈ t₁ᶜ, x ∉ t₂ → (if x ∈ t₁ ∨ x ∈ t₂ then f x else 0) • v x = 0
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
inst✝ : Nontrivial R
n : ℕ
⊢ ↑n ≤ Module.rank R M ↔ ∃ f, Injective ⇑f

Tactic:
refine le_rank_iff.trans ⟨fun ⟨v, v_ind⟩ ↦ ?_, fun ⟨f, f_inj⟩ ↦
    ⟨_, (Module.Basis.ofEquivFun <| .refl ..).linearIndependent.map_injOn f f_inj.injOn⟩⟩

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
x✝ : ∃ v, LinearIndependent R v
v : Fin n → M
v_ind : LinearIndependent R v
⊢ ∃ f, Injective ⇑f
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}

Tactic:
· rintro rfl; exact (hs.symm.subset (Or.inr rfl)).2 rfl

Goal state after:
case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}
Module: Mathlib.Data.Set.Card

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

Tactic:
rcases s.infinite_or_finite with hs | hs
  · simp_all [ncard, Infinite.sdiff hs (finite_singleton a)]
  · exact eq_tsub_of_add_eq (ncard_sdiff_singleton_add_one h hs)

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: case mpr
ι : Type u_1
R : Type u_3
A : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : SMulCommClass R R A
inst✝ : IsScalarTower R A A
b : Basis ι R A
z : A
⊢ ((∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)) →
    z ∈ center A

Tactic:
intro h
    rw [center, mem_ofPred_eq]
    constructor
    case comm =>
      intro y
      rw [← b.linearCombination_repr y, linearCombination_apply, sum, commute_iff_eq,
        Finset.sum_mul, Finset.mul_sum]
      simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]
    case left_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
          Finset.mul_sum]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
        Finset.smul_sum, smul_mul_assoc, mul_smul_comm, (h.2 _ _).1,
        (@SMulCommClass.smul_comm R R A)]
      rw [Finset.sum_comm]
    case right_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
      simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
n : ℕ
⊢ {t | t ⊆ s ∧ t.ncard = n}.ncard = s.ncard.choose n

Tactic:
by
  lift s to Finset α using hs
  have h₁ : {t ⊆ (s : Set α) | t.ncard = n} ⊆ range ((↑) : Finset α → Set α) := by
    intro t ht
    rw [Finset.mem_range_coe_iff]
    exact s.finite_toSet.subset ht.1
  have h₂ : (↑) ⁻¹' {t ⊆ (s : Set α) | t.ncard = n} = (s.powersetCard n : Set (Finset α)) := by
    ext t
    simp
  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 t : Set α
h : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard + s.encard = t.encard

Tactic:
ht.sdiff.cast_ncard_eq,

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ (t \ s).encard + s.encard = t.encard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    (fun q i ↦ quotientMapOfLE ⋯ q) (Quotient.mk'' a₁) = (fun q i ↦ quotientMapOfLE ⋯ q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
by
      simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]

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

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

Tactic:
@Finset.card_eq_one _ (toFinset s)

Goal state after:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
⊢ ∃ a, s = {a}
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a ≤ b
⊢ insert (pred a) (Icc a b) = Icc (pred a) b

Tactic:
by
  ext x; simp [or_and_left, pred_le_iff_eq_or_le]; simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: 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
M₅ : Type u_1
M₆ : Type u_2
S : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : Semiring S
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : AddCommMonoid M₄
inst✝⁹ : AddCommMonoid M₅
inst✝⁸ : AddCommMonoid M₆
inst✝⁷ : Module R M
inst✝⁶ : Module R M₂
inst✝⁵ : Module R M₃
inst✝⁴ : Module R M₄
inst✝³ : Module R M₅
inst✝² : Module R M₆
f : M →ₗ[R] M₂
inst✝¹ : Module S M₃
inst✝ : SMulCommClass R S M₃
a b : (M →ₗ[R] M₃) × (M₂ →ₗ[R] M₃)
⊢ (a + b).1.coprod (a + b).2 = a.1.coprod a.2 + b.1.coprod b.2

Tactic:
by
    ext
    simp only [Prod.snd_add, add_apply, coprod_apply, Prod.fst_add, add_add_add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
⊢ ∀ i ∈ J, (if h : i ∈ I then proj ⟨i, h⟩ else 0) b = 0

Tactic:
intro j hjJ

Goal state after:
case refine_1
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M₃
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
b : (i : ↑I) → φ ↑i
j : ι
hjJ : j ∈ J
⊢ (if h : j ∈ I then proj ⟨j, h⟩ else 0) b = 0
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
by
  rw [← comp_apply]
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type u_1
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (φ i)
I : Set ι
i : ι
⊢ p i ≤ comap (single R φ i) (pi I p)

Tactic:
intro x hx
  rw [Submodule.mem_comap, Submodule.mem_pi]
  rintro j -
  rcases eq_or_ne j i with rfl | hne <;> simp [*]

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (a - 1) (Ico a b) = Ico (a - 1) b

Tactic:
by
  simpa [pred_eq_sub_one] using insert_Ico_left_eq_Ico_pred_of_not_isMin h ha

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert (b - 1) (Ico a (b - 1)) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using insert_Ico_pred_right_eq_Ico h

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ upperBounds (Set.range ⇑(partialSups f)) = upperBounds (Set.range f)

Tactic:
ext a
  simp only [mem_upperBounds, Set.forall_mem_range, partialSups_le_iff]
  exact ⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| ∏ i ∈ Icc ⊥ n, ∏ x ∈ disjointed s i, g x

Tactic:
Nat.bot_eq_zero,

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
s : ℕ → Finset α
hs : Monotone s
g : α → β
n : ℕ
| ∏ i ∈ Icc 0 n, ∏ x ∈ disjointed s i, g x
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:
by
  rw [Nat.range_succ_eq_Iic, biUnion_Iic_disjointed]

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

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

Tactic:
rw [antidiagonal_succ, prod_cons, prod_map]; rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p

Tactic:
conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]
  rfl

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | a.1 ≤ k} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + (n - k), inj' := ⋯ }) (antidiagonal k)

Tactic:
by
  have aux₁ : fun a ↦ a.fst ≤ k = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
  have aux₂ : ∀ i j, (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔
                      ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
  rw [← map_prodComm_antidiagonal]
  simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
  ext ⟨i, j⟩
  simpa using aux₂ i j

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

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d ∈ I

Tactic:
by
  rw [show a * c - b * d = (a - b) * c + b * (c - d) by rw [sub_mul, mul_sub]; abel]
  exact I.add_mem (I.mul_mem_right _ h1) (I.mul_mem_left _ h2)

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Tactic:
intro J

Goal state after:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
I : Ideal α
hI : I ∈ s
hI' : x✝ ∉ I
J : Ideal α
⊢ J ∈ s → y✝ ∈ J
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case refine_2
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
p : Ideal α
hIp : I ≤ p
hp : Maximal (fun x ↦ x ∈ {p | Disjoint ↑p ↑S}) p
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

Tactic:
exact ⟨p, isPrime_of_maximally_disjoint _ _ hp.1 (fun _ ↦ hp.not_prop_of_gt), hIp, hp.1⟩

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ↑(Submonoid.powers a) → a_1 ∉ ↑I

Tactic:
rw [ha.coe_powers]

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
a : α
ha : IsIdempotentElem a
haI : a ∉ I
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ {1, a} → a_1 ∉ ↑I
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
intro J

Goal state after:
case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
⊢ ∀ (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ s = univ

Tactic:
rw [mem_top_iff_forall, eq_univ_iff_forall]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s ∈ ⊤ ↔ s = univ

Tactic:
by
  rw [mem_top_iff_forall, eq_univ_iff_forall]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ ∀ {x y : Set α},
    x ∈ {t | ∃ i, p i ∧ s i = t} → y ∈ {t | ∃ i, p i ∧ s i = t} → ∃ z ∈ {t | ∃ i, p i ∧ s i = t}, z ⊆ x ∩ y

Tactic:
by
    rintro _ _ ⟨i, hi, rfl⟩ ⟨j, hj, rfl⟩
    rcases h.inter hi hj with ⟨k, hk, hk'⟩
    exact ⟨_, ⟨k, hk, rfl⟩, hk'⟩

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

Goal state before:
pp: α : Type u
f g : Filter α
⊢ (f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot

Tactic:
simp only [neBot_iff, not_and_or, Ne, sup_eq_bot_iff]

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

Goal state before:
pp: case refine_2
α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
x : α
hx : x ∈ Ioi a
⊢ x ∈ ⋃ i ∈ s, Ici i

Tactic:
· rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
    rw [mem_iUnion₂]
    exact ⟨y, hys, hyx.le⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map (mab ∘ mba) g ≤ map mab f

Tactic:
← map_map

Goal state after:
α : Type u_1
β : Type u_2
mab : α → β
mba : β → α
f : Filter α
g : Filter β
h₁ : mab ∘ mba =ᶠ[g] id
h₂ : Tendsto mba g f
⊢ map mab (map mba g) ≤ map mab f
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : IsEmpty α
f : α → β
la : Filter α
lb : Filter β
⊢ Tendsto f la lb

Tactic:
simp only [filter_eq_bot_of_isEmpty la, tendsto_bot]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι' : Sort u_5
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
h : lb.HasBasis pb sb
⊢ (⊤ ×ˢ lb).HasBasis pb fun x ↦ univ ×ˢ sb x

Tactic:
by
  simpa only [principal_univ] using h.principal_prod univ

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

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
f : α → β
hf : ∀ (x : α), (∃ y, r x y) → r x (f x)
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
exact ⟨f, h.mono hf⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
F : Filter α
G : Filter β
m : α → β
hm : G ≤ map m F
this : RightInvOn (fun x ↦ F ⊓ comap m x) (map m) (Iic G)
⊢ SurjOn (map m) (Iic F) (Iic G)

Tactic:
exact this.surjOn fun H _ ↦ mem_Iic.mpr inf_le_left

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

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
mul : Mul α := e.mul
⊢ Semigroup α

Tactic:
apply e.injective.semigroup _

Goal state after:
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y