mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
rw [add_comm, add_eq_max hb, max_comm]

Goal state after:
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: γ : Type u
inst✝ : LinearOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = Order.cof γ

Tactic:
simpa using lift_cof_iSup_add_one hf

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c < ℶ_ ↑n ↔ c < ℶ_ ↑n

Tactic:
simpa using lift_lt (b := ℶ_ n)

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

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ b

Tactic:
by
        rw [← hb]
        exact H _ hf

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

Goal state before:
pp: α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ #(α ≃ β) = 2 ^ #α

Tactic:
by
  rw [mk_equiv_of_lift_eq (lift_inj.mpr eq), lift_id]

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

Goal state before:
pp: case mk.hf
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ∃ a, (fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) a = ⟨s, ⋯⟩

Tactic:
use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)

Goal state after:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
⊢ ((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
      if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 }) =
    ⟨s, ⋯⟩
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) v ∈ ⨆ i, ⨆ (_ : p i), S i

Tactic:
refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ i, ⨆ (_ : p i), S i
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ ⟨i, ⋯⟩ ∈ (↑s).toFinset.attach.val

Tactic:
apply Multiset.mem_attach

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ((Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)) ⋯ =
    ⟦a⟧

Tactic:
Equiv.subtypeQuotientEquivQuotientSubtype,

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
a : (i : ι) → α i
l : List ι
hl : ⟦l⟧ = Finset.univ.val
⊢ ({
            toFun := fun a ↦
              Quotient.hrecOn (motive := fun x ↦
                (∀ (i : ι), i ∈ x) → Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l)) (↑a)
                (fun a h ↦ ⟦⟨a, ⋯⟩⟧) ⋯ ⋯,
            invFun := fun a ↦ a.liftOn (fun a ↦ ⟨⟦↑a⟧, ⋯⟩) ⋯, left_inv := ⋯, right_inv := ⋯ }
          ⟨⟦l⟧, ⋯⟩).liftOn
      (fun l ↦ Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ ⟦a i⟧)) ⋯ =
    ⟦a⟧
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ i ∈ f.support ↔ f i ≠ 0

Tactic:
by
  obtain ⟨f, s⟩ := f
  induction s using Trunc.induction_on with | _ s
  dsimp only [support, Trunc.lift_mk]
  rw [Finset.mem_filter, Multiset.mem_toFinset, coe_mk']
  grind

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

Goal state before:
pp: case mk.mk.e_a
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
⊢ ∑ x ∈ (sf + sg).toFinset, (φ x) (g x) = ∑ x ∈ sg.toFinset, (φ x) (g x)

Tactic:
refine (Finset.sum_subset ?_ ?_).symm
      · intro i
        simp only [Multiset.mem_toFinset, Multiset.mem_add]
        exact Or.inr
      · intro i _ H2
        simp only [Multiset.mem_toFinset] at H2
        rw [(hg i).resolve_left H2, map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
⊢ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p) v ∈ ⨆ i, ⨆ (_ : p i), S i

Tactic:
refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i ≠ 0
⊢ ((fun i ↦ (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ i, ⨆ (_ : p i), S i
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
u : S
hu : u ≠ 0
⊢ LinearIndependent R ![u • x, u • y] ↔ LinearIndependent R ![x, y]

Tactic:
simp only [LinearIndependent.pair_iff]
  refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩
  · exact h s t (by rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero])
  · specialize h (u • s) (u • t) (by rw [smul_assoc, smul_assoc, smul_comm u s, smul_comm u t, hst])
    exact ⟨(smul_eq_zero_iff_right hu).mp h.1, (smul_eq_zero_iff_right hu).mp h.2⟩

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

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ ψ a * (χ a)⁻¹ = ψ a / χ a

Tactic:
div_eq_mul_inv

Goal state after:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ ψ a * (χ a)⁻¹ = ψ a * (χ a)⁻¹
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑(insert a s)) ↦ f ↑x) ↔
    (LinearIndependent K fun (x : ↑s) ↦ f ↑x) ∧ f a ∉ span K (f '' s)

Tactic:
← linearIndependent_equiv
    ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm),

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndependent K ((fun x ↦ f ↑x) ∘ ⇑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) ↔
    (LinearIndependent K fun (x : ↑s) ↦ f ↑x) ∧ f a ∉ span K (f '' s)
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ (s 0 :: List.ofFn fun i ↦ s i.succ).prod ↔ ∃ f, (↑(f 0) :: List.ofFn fun i ↦ ↑(f i.succ)).prod = a

Tactic:
List.prod_cons,

Goal state after:
case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ a ∈ s 0 * (List.ofFn fun i ↦ s i.succ).prod ↔ ∃ f, ↑(f 0) * (List.ofFn fun i ↦ ↑(f i.succ)).prod = a
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ s, Injective (f a)
hs : ((fun a ↦ image (f a) t) '' ↑s).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f s t)

Tactic:
induction s using Finset.induction with

Goal state after:
case insert
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : (∀ a ∈ s, Injective (f a)) → ((fun a ↦ image (f a) t) '' ↑s).PairwiseDisjoint id → #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f (insert a s) t)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
f : R →+* S
x y : R[M]
⊢ map (↑f) (x * y) = map (↑f) x * map (↑f) y

Tactic:
ext
  simp [mul_def, sum_mapRange_index, map_finsuppSum, single_apply, apply_ite]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ↑u ⊆ image2 f s t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Tactic:
← Set.image_prod,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ↑u ⊆ (fun x ↦ f x.1 x.2) '' s ×ˢ t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
⊢ erase m x + single m (x.coeff m) = x

Tactic:
by
  ext; simp [Finsupp.erase_add_single]

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

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ∀ (b : A × A),
    b.1 ∈ f.coeff.support ∧ b.2 ∈ g.coeff.support →
      b ≠ (a0, b0) → (if b.1 * b.2 = a0 * b0 then f.coeff b.1 * g.coeff b.2 else 0) = 0

pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0

Tactic:
· refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
    exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support) → (if True then f.coeff a0 * g.coeff b0 else 0) = 0
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
div_eq_mul_inv

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
by
  rw [div_eq_mul_inv]; exact subset_mul_left _ <| by simpa

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
div_eq_mul_inv

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor
  · contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.zpow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_zpow hn

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
simpa [support] using! Finsupp.support_add

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * c3 * (d3 * c2⁻¹) = d1⁻¹ * c1 * (d2 * c2⁻¹) → d1⁻¹ * c3 = d1⁻¹ * c1 ∧ d3 * c2⁻¹ = d2 * c2⁻¹
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2

Tactic:
rw [mul_left_cancel_iff, mul_right_cancel_iff,
            mul_assoc, ← mul_assoc c3, he, mul_assoc, mul_assoc] at hu

Goal state after:
case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
h12 : c1 ≠ 1 ∨ d2 ≠ 1
c3 d3 : G
hu : d1⁻¹ * (c1 * (d2 * c2⁻¹)) = d1⁻¹ * (c1 * (d2 * c2⁻¹)) → c3 = c1 ∧ d3 = d2
hc3 : c3 ∈ C
hd3 : d3 ∈ D
he : c3 * d3 = c1 * d2
⊢ c3 = c1 ∧ d3 = d2
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
ext; simp [coeff, update]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support

Tactic:
by classical rw [support_update, if_neg ha]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
s : Set ℕ∞
c : R
⊢ c • sSup s = ⨆ a ∈ s, c • a

Tactic:
by
  simp_rw [sSup_eq_iSup, smul_iSup]

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)

Goal state after:
case inl
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : 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)
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc, (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ) ∈ r

Tactic:
by
    obtain hi | rfl | hi :=
      lt_trichotomy i (Fin.castLE (by lia) (Fin.last _ : Fin (p.length + 1)))
    · convert! p.step ⟨i.1, hi⟩ <;> convert! Fin.append_left p q _ <;> rfl
    · convert! connect
      · convert! Fin.append_left p q _
      · convert! Fin.append_right p q _; rfl
    · set x := _; set y := _
      change Fin.append p q x ~[r] Fin.append p q y
      have hx : x = Fin.natAdd _ ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <|
          i.2.trans <| by lia⟩ := by
        ext; dsimp [x, y]; rw [Nat.add_sub_cancel']; exact hi
      have hy : y = Fin.natAdd _ ⟨i - p.length, Nat.sub_lt_left_of_lt_add (le_of_lt hi)
          (by exact i.2)⟩ := by
        ext
        dsimp
        conv_rhs => rw [Nat.add_comm p.length 1, add_assoc,
          Nat.add_sub_cancel' <| le_of_lt (show p.length < i.1 from hi), add_comm]
        rfl
      rw [hx, Fin.append_right, hy, Fin.append_right]
      convert! q.step ⟨i - (p.length + 1), Nat.sub_lt_left_of_lt_add hi <| by lia⟩
      rw [Fin.succ_mk, Nat.sub_eq_iff_eq_add (le_of_lt hi : p.length ≤ i),
        Nat.add_assoc _ 1, add_comm 1, Nat.sub_add_cancel]
      exact hi

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
⊢ height a + 1 ≤ height b

Tactic:
cases hfin : height a with
  | top =>
    have : ⊤ ≤ height b := by
      rw [← hfin]
      gcongr
    simp [this]
  | coe n =>
    apply Order.add_one_le_of_lt
    rw [← hfin]
    gcongr
    simp [hfin]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ krullDim α = ⨆ a, ↑(coheight a)

Tactic:
rw [krullDim_eq_iSup_coheight_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
⊢ ∀ (i : α), ↑(height i) ≤ ((↑m + 1) * ⨆ a, ↑(height a)) + ↑m

Tactic:
refine fun x ↦ (WithBot.coe_mono (height_le_of_krullDim_preimage_le f h x)).trans ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
⊢ (fun a ↦ ↑a) ((↑m + 1) * height (f x) + ↑m) ≤ ((↑m + 1) * ⨆ a, ↑(height a)) + ↑m
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' (a :: as).prod = (⇑f '' a :: List.map (fun s ↦ ⇑f '' s) as).prod

Tactic:
List.prod_cons,

Goal state after:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' (a * as.prod) = (⇑f '' a :: List.map (fun s ↦ ⇑f '' s) as).prod
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' (a * as.prod) = (⇑f '' a :: List.map (fun s ↦ ⇑f '' s) as).prod

Tactic:
List.prod_cons,

Goal state after:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' (a * as.prod) = ⇑f '' a * (List.map (fun s ↦ ⇑f '' s) as).prod
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
α : Type u_22
s : Finset α
m : α → M
n : N
⊢ (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n

Tactic:
induction s using Finset.induction with

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
m : M
α : Type u_22
s : Finset α
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a

Tactic:
induction s using Finset.induction with

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

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
f : M ≃ₗ[R] M
g : N ≃ₗ[R] N
n : ℤ
⊢ congr f g ^ n = congr (f ^ n) (g ^ n)

Tactic:
by
  cases n with
  | ofNat n => exact congr_pow _ _ _
  | negSucc n => simp_rw [zpow_negSucc, congr_pow]; exact congr_symm _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹² : KleeneAlgebra α
inst✝¹¹ : LE β
inst✝¹⁰ : LT β
inst✝⁹ : Zero β
inst✝⁸ : One β
inst✝⁷ : Add β
inst✝⁶ : Mul β
inst✝⁵ : Pow β ℕ
inst✝⁴ : SMul ℕ β
inst✝³ : NatCast β
inst✝² : Max β
inst✝¹ : Bot β
inst✝ : KStar β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
kstar : ∀ (a : β), f a∗ = (f a)∗
a b : β
h : b * a ≤ b
⊢ b * a∗ ≤ b

Tactic:
by
    rw [← le, mul, kstar]
    rw [← le, mul] at h
    exact mul_kstar_le_self h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
p : Fin 2 → R
h : IsCoprime (p 0) (p 1)
⊢ p ≠ 0

Tactic:
rintro rfl
  exact not_isCoprime_zero_zero h

Goal state after:
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ m ∈ 1 • N

Tactic:
rw [← one_smul A m]

Goal state after:
case refine_2
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ 1 • m ∈ 1 • N
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I✝ : Ideal R
J✝ : Ideal S
I J : Ideal (R × S)
h : map (RingHom.fst R S) I ≤ map (RingHom.fst R S) J ∧ map (RingHom.snd R S) I ≤ map (RingHom.snd R S) J
⊢ I ≤ J

Tactic:
ideal_prod_eq I,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I✝ : Ideal R
J✝ : Ideal S
I J : Ideal (R × S)
h : map (RingHom.fst R S) I ≤ map (RingHom.fst R S) J ∧ map (RingHom.snd R S) I ≤ map (RingHom.snd R S) J
⊢ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) ≤ J
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ I.prod J = ⊥ ↔ I = ⊥ ∧ J = ⊥

Tactic:
rw [← prod_inj, prod_bot_bot]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : WellFoundedGT (Submodule R R)
inst✝ : WellFoundedGT (Submodule S S)
⊢ WellFoundedGT (Submodule (R × S) (R × S))

Tactic:
exact Ideal.idealProdEquiv.toOrderEmbedding.wellFoundedGT

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'
⊢ x ∈ M'

Tactic:
choose f hf using H

Goal state after:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
f : ↑s → ℕ
hf : ∀ (r : ↑s), ↑r ^ f r • x ∈ M'
⊢ x ∈ M'