mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ↑n ∣ ↑a - ↑((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat ∧
    ((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat ≡ b [MOD m]

Tactic:
modEq_iff_dvd,

Goal state after:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ ↑n ∣ ↑a - ↑((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat ∧
    ↑m ∣ ↑b - ↑((↑n * n.gcdA m * ↑b + ↑m * n.gcdB m * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: iv : ℕ
ih : ∀ {n : Fin iv → ℕ} (k : (i : Fin iv) × Fin (n i)), ↑(finSigmaFinEquiv k) = ∑ i, n (Fin.castLE ⋯ i) + ↑k.snd
n : Fin (iv + 1) → ℕ
hi : iv < iv + 1
j : Fin (n ⟨iv, hi⟩)
⊢ ⟨Fin.addCases Sum.inl Sum.inr ⟨iv, hi⟩, ⋯ ▸ j⟩ = ⟨Sum.inr 0, j⟩

Tactic:
simp [Fin.addCases, Fin.natAdd]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
⊢ Nat.card { x // p x } = Fintype.card { x // p x }

Tactic:
Fintype.card_eq_nat_card

Goal state after:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
⊢ Nat.card { x // p x } = Nat.card { x // p x }
Module: Mathlib.Algebra.BigOperators.Fin

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

Tactic:
by
    change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
    rw [Fin.prod_univ_succ]; simp

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ (∑ i ∈ insert a s, g i • ⇑i) (x * y) - a x * (∑ i ∈ insert a s, g i • ⇑i) y = 0

Tactic:
by rw [hg]; simp

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

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b

Tactic:
exact mul_left_not_lt b h

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ IsEmpty ↑s ↔ s = ∅

Tactic:
isEmpty_subtype,

Goal state after:
α : Type u_1
s : Set α
⊢ (∀ (x : α), x ∉ s) ↔ s = ∅
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:
conv =>
    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) =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
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'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} #↑↑⟨rangeSplitting ⇑f '' s, ⋯⟩

Tactic:
· exact (Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
inst✝ : Finite α
this : Fintype α
⊢ Fintype.card α ≤ Nat.card α

Tactic:
Fintype.card_eq_nat_card

Goal state after:
α : Type u_1
l : List α
h : l.Nodup
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≤ Nat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
hs : ∅.Finite
⊢ ∅.ncard ≤ 1 ↔ ∅ = ∅ ∨ ∃ a, ∅ = {a}

case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
  rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
  obtain ⟨a, t, hat, hts, rfl⟩ := h
  simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
  refine ⟨a, t, hat, ?_, ?_⟩
  · simp [Set.ext_iff, hts]
  · simp

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 ι
I J : Set ι
h : Disjoint I J
⊢ ⨆ i ∈ I, (single R φ i).range ≤ ⨅ i ∈ J, (proj i).ker

Tactic:
refine iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 ?_

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ comap (single R φ i) (⨅ i ∈ J, (proj i).ker) = ⊤
Module: Mathlib.Order.Interval.Set.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
Icc_eq_empty,

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ∅ = Ioo a b

case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
R₃ : Type u_5
M₃ : Type u_6
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : Ring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ g.ker ≤ f.range ↔ f.range.mkQ ∘ₗ g.ker.subtype = 0

Tactic:
by
  rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]

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

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert (b + 1) (Ioc a b) = Ioc a (b + 1)

Tactic:
by
  simpa [succ_eq_add_one] using insert_Ioc_right_eq_Ioc_succ_of_not_isMax h hb

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case intro
R : Type u
inst✝³ : Semiring R
ι : Type v
inst✝² : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
val✝ : Fintype ι
⊢ motive' ((i : ι) → M i)

Tactic:
revert M

Goal state after:
case intro
R : Type u
inst✝¹ : Semiring R
ι : Type v
inst✝ : Finite ι
motive : (N : Type u) → [inst : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
val✝ : Fintype ι
⊢ ∀ (M : ι → Type u) [inst : (i : ι) → AddCommMonoid (M i)] [inst_1 : (i : ι) → Module R (M i)],
    (∀ (i : ι), motive (M i)) → motive' ((i : ι) → M i)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case intro
ι : Type v
inst✝³ : Finite ι
R : Type u_1
inst✝² : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst✝¹ : (i : ι) → AddCommGroup (M i)
inst✝ : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
val✝ : Fintype ι
⊢ motive' ((i : ι) → M i)

Tactic:
revert M

Goal state after:
case intro
ι : Type v
inst✝¹ : Finite ι
R : Type u_1
inst✝ : Ring R
motive : (N : Type u) → [inst : AddCommGroup N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst : AddCommGroup N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'], motive N → motive' N' → motive' (N × N')
val✝ : Fintype ι
⊢ ∀ (M : ι → Type u) [inst : (i : ι) → AddCommGroup (M i)] [inst_1 : (i : ι) → Module R (M i)],
    (∀ (i : ι), motive (M i)) → motive' ((i : ι) → M i)
Module: Mathlib.Order.PartialSups

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

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

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, f.range = (↑e).graph

Tactic:
by
  obtain ⟨e₁, he₁⟩ := f.exists_range_eq_graph hf₁ fun _ _ ↦ (hf _ _).1
  obtain ⟨e₂, he₂⟩ := ((LinearEquiv.prodComm _ _ _).toLinearMap.comp f).exists_range_eq_graph
    (by simpa) <| by simp [hf]
  have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂
    rw [Eq.comm, ← he₁ (h, i), Eq.comm, ← he₂ (i, h)]
    simp only [mem_range, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.prodComm_apply, Prod.swap_eq_iff_eq_swap, Prod.swap_prod_mk]
  exact ⟨
  { toFun := e₁
    map_smul' := e₁.map_smul'
    map_add' := e₁.map_add'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

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
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x > a, f x = ∏ x ≥ a, f x

Tactic:
rw [Ici_eq_cons_Ioi, prod_cons]

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : CompleteBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
⊢ disjointed f i = f i ⊓ ⨅ j, ⨅ (_ : j < i), (f j)ᶜ

Tactic:
by
  simp only [disjointed_apply, Finset.sup_eq_iSup, mem_Iio, sdiff_eq, compl_iSup]

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

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

Tactic:
apply eq_of_veq

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (0, n + 1)
        (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (antidiagonal n)) ⋯).val
Module: Mathlib.Data.Finset.NatAntidiagonal

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

Tactic:
apply eq_of_veq

Goal state after:
n : ℕ
⊢ (antidiagonal (n + 1)).val =
    (cons (n + 1, 0)
        (map ((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (antidiagonal n)) ⋯).val
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
⊢ y * x ∈ I ↔ x ∈ I

Tactic:
refine ⟨fun h => ?_, fun h => I.mul_mem_left y h⟩

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
⊢ x ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ x * ∑ m ∈ range (n + 1), t n m + y * ∑ m ∈ range (n + 1), t n m =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))

Tactic:
mul_sum,

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ ∑ i ∈ range (n + 1), x * t n i + y * ∑ m ∈ range (n + 1), t n m =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))
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 : x✝ * y✝ ∈ sInf s
hx : x✝ ∉ sInf s
⊢ y✝ ∈ sInf s

Tactic:
rw [Ideal.mem_sInf] at hx e ⊢
      push Not at hx
      obtain ⟨I, hI, hI'⟩ := hx
      intro J hJ
      rcases hs'.total hI hJ with h | h
      · exact h (((H I hI).mem_or_mem (e hI)).resolve_left hI')
      · exact ((H J hJ).mem_or_mem (e hJ)).resolve_left fun x => hI' <| h x

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
x : α
s : Set α
⊢ span (insert (-x) s) = span (insert x s)

Tactic:
span_insert,

Goal state after:
α : Type u
inst✝ : Ring α
x : α
s : Set α
⊢ span {-x} ⊔ span s = span (insert x s)
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
x : α
s : Set α
inst✝ : LinearOrder α
⊢ span (insert |x| s) = span (insert x s)

Tactic:
span_insert,

Goal state after:
α : Type u
inst✝¹ : Ring α
x : α
s : Set α
inst✝ : LinearOrder α
⊢ span {|x|} ⊔ span s = span (insert x s)
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
⊢ ∀ (x y : (ι → R) ⧸ pi fun x ↦ I),
    Quotient.liftOn' (x + y) (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
      Quotient.liftOn' x (fun f i ↦ (Quotient.mk I) (f i)) ⋯ + Quotient.liftOn' y (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
by rintro ⟨_⟩ ⟨_⟩; rfl

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
⊢ ∀ (m : R ⧸ I) (x : (ι → R) ⧸ pi fun x ↦ I),
    Quotient.liftOn' (m • x) (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
      (RingHom.id (R ⧸ I)) m • Quotient.liftOn' x (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
by rintro ⟨_⟩ ⟨_⟩; rfl

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.PartialSups

Goal state before:
pp: ι : Type u_2
inst✝⁴ : LinearOrder ι
α : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : LocallyFiniteOrder ι
inst✝¹ : SuccOrder ι
inst✝ : OrderBot ι
f : ι → α
i : ι
⊢ (partialSups f) (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ Order.succ)) i

Tactic:
refine Succ.rec (by simp) (fun j _ h ↦ ?_) (bot_le (a := i))
  have : (partialSups (f ∘ Order.succ)) (Order.succ j) =
      ((partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)) := by simp
  simp [this, h, sup_assoc]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ x ∈ (mapRange.linearMap f).range → x ∈ submodule fun x ↦ f.range

pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ (x ∈ submodule fun x ↦ f.range) → x ∈ (mapRange.linearMap f).range

Tactic:
· rintro ⟨y, hy⟩
    simp [← hy]

Goal state after:
case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
⊢ (x ∈ submodule fun x ↦ f.range) → x ∈ (mapRange.linearMap f).range
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋃ i, s i
hs : Monotone s
f g : (a : α) → β a
a : α
i : ι
hi : a ∈ s i
j : ι
hij : i ≤ j
⊢ (s j).piecewise f g a = (⋃ i, s i).piecewise f g a

Tactic:
simp only [Set.piecewise_eq_of_mem, hs hij hi, subset_iUnion _ _ hi]

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → y ∈ ⋃ i, (f i).sets → x ∩ y ∈ ⋃ i, (f i).sets

Tactic:
by
        simp only [mem_iUnion, exists_imp]
        intro x y a hx b hy
        rcases h a b with ⟨c, ha, hb⟩
        exact ⟨c, inter_mem (ha hx) (hb hy)⟩

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ 𝓟 s ⊓ 𝓟 t ≤ 𝓟 (s ∩ t)

Tactic:
by simp only [le_principal_iff, mem_inf_iff]; exact ⟨s, Subset.rfl, t, Subset.rfl, rfl⟩

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ 𝓟 (s ∩ t) ≤ 𝓟 s ⊓ 𝓟 t

Tactic:
simp [le_inf_iff, inter_subset_left, inter_subset_right]

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → β
⊢ f =ᶠ[⊤] g ↔ f = g

Tactic:
simp [EventuallyEq, funext_iff]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
hl : la.HasBasis pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j

Tactic:
by
    simpa only [exists_prop, subset_inter_iff] using
      hl.mem_iff.1 (inter_mem (hl.mem_of_mem hi) (hl.mem_of_mem hj))

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

Goal state before:
pp: α : Type u_1
la : Filter α
r : α → α → Prop
⊢ (∃ t ∈ la, t ×ˢ t ⊆ {x | (fun x ↦ r x.1 x.2) x}) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y

Tactic:
simp only [prod_subset_iff, mem_ofPred_eq]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
by
  rw [atTop_Ici_eq, tendsto_comap_iff, Function.comp_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : SMul R M
inst✝ : SMul S N
φ : R → S
f : M →ₑ[φ] N
r : R
x✝¹ x✝ : M
h : (Setoid.ker ⇑f) x✝¹ x✝
⊢ (Setoid.ker ⇑f) (r • x✝¹) (r • x✝)

Tactic:
by rw [Setoid.ker_def] at h ⊢; simp_rw [map_smulₛₗ, h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ a₁ • _b < a₂ • _b

Tactic:
by
    rw [← sub_pos, ← sub_smul]; exact smul_pos (sub_pos.2 ha) hb

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝ : Module.Finite A C
⊢ g.Finite

Tactic:
exact .of_restrictScalars_finite A B C

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (Iic x) ≤ x

pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ (f '' f ⁻¹' Iic x).Nonempty

Tactic:
· rw [csSup_Iic]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ (f '' f ⁻¹' Iic x).Nonempty
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ (typein r).toRelEmbedding i < o

Tactic:
rw [← ho]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : ι
⊢ (typein r).toRelEmbedding i < type r