mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * a ^ ω * succ b ≤ a ^ ω * succ b

Tactic:
← opow_one_add,

Goal state after:
case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ (1 + ω) * succ b ≤ a ^ ω * succ b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
rw [mul_comm, max_comm]
  exact mul_eq_max_of_aleph0_le_left h h'

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

Goal state before:
pp: case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ 0
⊢ a * ω ^ ω ^ 0 = ω ^ ω ^ 0

Tactic:
opow_zero,

Goal state after:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ 1
⊢ a * ω ^ 1 = ω ^ 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case right.right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0

Tactic:
· rintro rfl
        apply this
        rw [mul_zero] at h
        exact h.symm

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

Goal state before:
pp: case a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
one_le_iff_pos.2 a0

Goal state after:
case a
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
⊢ a * ω ^ ω ^ b ≤ a * ω ^ ω ^ b
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ ∀ (i : ↑(Iio a)), ↑(f i) < o

Tactic:
exact fun i ↦ (f i).2

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ IsCofinal (range fun i ↦ ⟨g ↑(f i), ⋯⟩)

Tactic:
rintro ⟨b, hb⟩
    rw [mem_Iio, hg.lt_iff_exists_lt ho] at hb
    obtain ⟨c, hc, hc'⟩ := hb
    obtain ⟨_, ⟨d, rfl⟩, hd⟩ := hf.isCofinal_range ⟨c, hc⟩
    refine ⟨⟨_, hg.strictMono (f d).2⟩, ?_, hc'.le.trans (hg.monotone hd)⟩
    simp

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

Goal state before:
pp: a : Ordinal.{u_1}
h : (ω_ a).IsInitial
ho : ω ≤ ω_ a
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ a)

Tactic:
exact isPrincipal_opow_omega a

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

Goal state before:
pp: case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ max c ℵ₀

Tactic:
powerlt_aleph0 h

Goal state after:
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s // Bounded r s } = #α

Tactic:
rcases eq_or_ne #α 0 with (ha | ha)
  · rw [ha]
    have := mk_eq_zero_iff.1 ha
    rw [mk_eq_zero_iff]
    constructor
    rintro ⟨s, hs⟩
    exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)
  have h' : IsStrongLimit #α := ⟨ha, @h⟩
  have ha := h'.aleph0_le
  apply le_antisymm
  · have : { s : Set α | Bounded r s } = ⋃ i, 𝒫 { j | r j i } := ofPred_exists _
    rw [← coe_ofPred, this]
    refine mk_iUnion_le_sum_mk.trans ((sum_le_mk_mul_iSup (fun i => #(𝒫 { j | r j i }))).trans
      ((mul_le_max_of_aleph0_le_left ha).trans ?_))
    rw [max_eq_left]
    apply ciSup_le' _
    intro i
    rw [mk_powerset]
    exact (h (card_typein_lt _ hr)).le
  · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
    · apply bounded_singleton
      rw [← hr]
      apply isSuccLimit_ord ha
    · intro a b hab
      simpa [singleton_eq_singleton_iff] using hab

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

Goal state before:
pp: case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #↑(Sum.inl ⁻¹' range f) ≤ #β

Tactic:
refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_

Goal state after:
case property
α : Type u
inst✝ : Infinite α
β : Type u
f : (fun α β ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #↑(range f) ≤ #β
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ Function.Surjective (mapRange f hf) ↔ ∀ (i : ι), Function.Surjective (f i)

Tactic:
by
  classical
  refine ⟨fun h i u ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨x, hx⟩ := h (single i u)
    exact ⟨x i, by simpa using congr($hx i)⟩
  · obtain ⟨x, s, hs⟩ := x
    have (i : ι) : ∃ u : β₁ i, f i u = x i ∧ (x i = 0 → u = 0) :=
      (eq_or_ne (x i) 0).elim
        (fun h ↦ ⟨0, (hf i).trans h.symm, fun _ ↦ rfl⟩)
        (fun h' ↦ by
          obtain ⟨u, hu⟩ := h i (x i)
          exact ⟨u, hu, fun h'' ↦ (h' h'').elim⟩)
    choose y hy using this
    refine ⟨⟨y, Trunc.mk ⟨s, fun i ↦ ?_⟩⟩, ext fun i ↦ ?_⟩
    · exact (hs i).imp_right (hy i).2
    · simp [(hy i).1]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ (Equiv.cast ⋯) (f (h.symm (h i))) = f i

Tactic:
Equiv.cast_eq_iff_heq,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ f (h.symm (h i)) ≍ f i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ (Equiv.cast ⋯) (f (h (h.symm k))) = f k

Tactic:
Equiv.cast_eq_iff_heq,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ f (h (h.symm k)) ≍ f k
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ (extendWith x 0) (some j) = (single none x) (some j)

Tactic:
· rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
⊢ indep (⋃ I ∈ c, ↑I)

Tactic:
dsimp [indep]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
⊢ LinearIndepOn R v (⋃ I ∈ c, ↑I)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
s t : R
hst : s • u • x + t • v • y = 0
h : (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0 → s = 0 ∧ t = 0
⊢ (s * ↑hu.unit) • x + (t * ↑hv.unit) • y = 0

Tactic:
simpa [mul_smul]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
hac : a = 0 ∧ c = 0
⊢ 1 • a • x + 0 • c • x = 0

Tactic:
by simp [hac.1, hac.2]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ LinearIndependent R fun ji ↦ f ji.fst ji.snd

Tactic:
apply LinearIndependent.of_linearIndepOn_id_range

Goal state after:
case hf
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ Injective fun ji ↦ f ji.fst ji.snd

case a
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
⊢ LinearIndepOn R id (range fun ji ↦ f ji.fst ji.snd)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
x y : R[M]
a✝ : N
⊢ (mapDomain f (x + y)).coeff a✝ = (mapDomain f x + mapDomain f y).coeff a✝

Tactic:
simp [Finsupp.mapDomain_add]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x y : R[M]
⊢ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) (x + y).coeff) =
    MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff) +
      MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) y.coeff)

Tactic:
simp [Finsupp.mapDomain_add]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
a : δ
⊢ (image₂ f s t).sup g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
rw [Finset.sup_le_iff, forall_mem_image₂]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
⊢ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) (x + y).coeff) =
    AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff) +
      AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) y.coeff)

Tactic:
simp [Finsupp.mapDomain_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ curryRingEquiv (single (m, n) r) = single m (single n r)

Tactic:
by simp [curryRingEquiv]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ ↑(s / t) ↔ ¬Disjoint ↑s ↑t

Tactic:
coe_div,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s t : Finset α
⊢ 1 ∈ ↑s / ↑t ↔ ¬Disjoint ↑s ↑t
Module: Mathlib.LinearAlgebra.Finsupp.Span

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 t : Set α
h : Disjoint s t
⊢ ⨆ a ∈ s, (lsingle a).range ≤ ⨅ a ∈ t, (lapply a).ker

Tactic:
refine iSup_le fun a₁ => iSup_le fun h₁ => range_le_iff_comap.2 ?_

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 t : Set α
h : Disjoint s t
a₁ : α
h₁ : a₁ ∈ s
⊢ comap (lsingle a₁) (⨅ a ∈ t, (lapply a).ker) = ⊤
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
⊢ (p.projection q hpq).range = p

Tactic:
by
  simp [projection, range_comp]

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
⊢ (⨆ i, f i) * a = ⨆ i, f i * a

Tactic:
simp_rw [mul_comm, ENat.mul_iSup]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
⊢ List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) x.toList

Tactic:
simp_rw [List.isChain_iff_getElem, length_toList, add_lt_add_iff_right]
  intro i h
  convert! x.step ⟨i, by simpa [toList] using h⟩ <;> apply List.get_ofFn

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inl
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc, (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ) ∈ r

Tactic:
convert! p.step ⟨i.1, hi⟩ <;> convert! Fin.append_left p q _

Goal state after:
case e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc =
    Fin.append p.toFun q.toFun (Fin.castAdd (q.length + 1) ⟨↑i, hi⟩.castSucc)

case e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ =
    Fin.append p.toFun q.toFun (Fin.castAdd (q.length + 1) ⟨↑i, hi⟩.succ)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
⊢ (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ[R] x₂ else 0

Tactic:
by split_ifs <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
⊢ (x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ[R] x₂ else 0

Tactic:
by split_ifs <;> simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
⊢ a * 1 = a

Tactic:
by
    ext x
    simp only [mem_mul, mem_one, mul_smul_comm, exists_exists_eq_and, mul_one]
    constructor
    · rintro ⟨y, hy, r, rfl⟩
      exact smul_mem _ _ hy
    · intro hx
      exact ⟨x, hx, 1, one_smul _ _⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (1 - x) y

Tactic:
sub_eq_neg_add

Goal state after:
R : Type u
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (-x + 1) y
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (1 - x) y

Tactic:
sub_eq_neg_add

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (-x + 1) y
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
⊢ ∃ tr, ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j

Tactic:
let sli := li.mergeSort

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
⊢ ∃ tr, ∀ (i j : Fin n), val i ≤ val j ↔ tr i ≤ tr j
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case pos
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

Tactic:
rw [hx, Pi.single_eq_same, Pi.single_eq_same]

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (u * ∏ j ∈ t, s j +
      ∑ x ∈ t, if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    u * ∏ i ∈ t, s i + v * s a

Tactic:
← hμ',

Goal state after:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
⊢ (u * ∏ j ∈ t, s j +
      ∑ x ∈ t, if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    u * ∏ i ∈ t, s i + ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

Tactic:
rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]

Goal state after:
case h
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ comap f (I • p) ≤ I • comap f p

Tactic:
conv_lhs => rw [← Submodule.map_comap_eq_self hp, ← Submodule.map_smul'']

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
⊢ comap f (map f (I • comap f p)) ≤ I • comap f p
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ P a b (b, 0, 1)

Tactic:
dsimp [P]; rw [mul_one, mul_zero, zero_add]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ lcm x y

Tactic:
rw [lcm, hxy, div_zero]
      exact dvd_zero _

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ lcm x y

Tactic:
rw [lcm, hxy, div_zero]
      exact dvd_zero _

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

Goal state before:
pp: R : Type u
M : Type v
M' : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
r : R
N : Submodule R M
f : M →ₗ[R] M'
⊢ map f (r • N) = r • map f N

Tactic:
simp_rw [← ideal_span_singleton_smul, map_smul'']

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m ≤ n
⊢ I ^ n ≤ I ^ m

Tactic:
by
  obtain _ | m := m
  · rw [Submodule.pow_zero, one_eq_top]; exact le_top
  obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
  rw [add_comm, Submodule.pow_add _ m.add_one_ne_zero]
  exact mul_le_right

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
← sSup_pair,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ (sSup {N, P}).annihilator = N.annihilator ⊓ P.annihilator
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this : restrictScalars S (⇑(algebraMap S R) '' ↑I • N) = ↑I • restrictScalars S N
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N

Tactic:
coe_set_smul

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this : restrictScalars S (⇑(algebraMap S R) '' ↑I • N) = I • restrictScalars S N
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case neg.refine_1.e_f
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
hs : s ≠ 0
h : ∃ x, x ∈ s ∧ x ≠ 0
f : {a : α} → a ∈ s → α
hf : ∀ {a : α} (h : a ∈ s), a = s.gcd * f h
x : α
hx : x ∈ s
⊢ id x = s.gcd * f hx

Tactic:
rw [id, ← hf hx]

Goal state after: