mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
f : Dual R M
⊢ f ∈ ↑(span R s).dualAnnihilator ↔ f ∈ {f | s ⊆ ↑f.ker}

Tactic:
simp only [SetLike.mem_coe, mem_dualAnnihilator, Set.mem_ofPred_eq, ← LinearMap.mem_ker]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
f : Dual R M
⊢ (∀ w ∈ span R s, w ∈ LinearMap.ker f) ↔ s ⊆ ↑(LinearMap.ker f)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ f.dualMap.ker = (Dual.eval R M' ∘ₗ f).range.dualCoannihilator

Tactic:
by
  ext x; simp [LinearMap.ext_iff (f := dualMap f x)]

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
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ (u • s) • x + (u • t) • y = 0

Tactic:
smul_assoc,

Goal state after:
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
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ u • s • x + (u • t) • y = 0
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
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ u • s • x + (u • t) • y = 0

Tactic:
smul_assoc,

Goal state after:
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
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ u • s • x + u • t • y = 0
Module: Mathlib.Tactic.Module

Goal state before:
pp: case e_f
R : Type u_2
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Semiring R
inst✝ : Module R M
l : NF R M
x : M
h :
  x =
    (map
        (fun x ↦
          match x with
          | (r, x) => r • x)
        l).sum
r : R
p : R × M
⊢ ((fun x ↦ x.1 • x.2) ∘ fun x ↦ (r * x.1, x.2)) p = ((fun x ↦ r • x) ∘ fun x ↦ x.1 • x.2) p

Tactic:
simp [mul_smul]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

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

Tactic:
List.ofFn_zero,

Goal state after:
case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ [].prod ↔ ∃ f, [].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 β
⊢ ↑(t.biUnion fun b ↦ image (fun a ↦ f a b) s) = ↑(image₂ f s t)

Tactic:
push_cast
    exact Set.iUnion_image_right _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ ↑(image₂ f (s ∪ t) (s ∩ t)) ⊆ ↑(image₂ f s t)

Tactic:
push_cast
    exact image2_union_inter_subset hf

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

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card

Tactic:
have :
    ∀ t : Finset V,
      ∀ s' : Finset V,
        ↑s' ⊆ s →
          s ∩ ↑t = ∅ →
            s ⊆ (span K ↑(s' ∪ t) : Submodule K V) →
              ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
    fun t =>
    Finset.induction_on t
      (fun s' hs' _ hss' =>
        have : s = ↑s' := eq_of_linearIndepOn_id_of_span_subtype hs hs' <| by simpa using hss'
        ⟨s', by simp [this]⟩)
      fun b₁ t hb₁t ih s' hs' hst hss' =>
      have hb₁s : b₁ ∉ s := fun h => by
        have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
        rwa [hst] at this
      have hb₁s' : b₁ ∉ s' := fun h => hb₁s <| hs' h
      have hst : s ∩ ↑t = ∅ :=
        eq_empty_of_subset_empty <|
          -- Porting note: `-subset_inter_iff` required.
          Subset.trans
            (by simp [inter_subset_inter, -subset_inter_iff])
            (le_of_eq hst)
      Classical.by_cases (p := s ⊆ (span K ↑(s' ∪ t) : Submodule K V))
        (fun this =>
          let ⟨u, hust, hsu, Eq⟩ := ih _ hs' hst this
          have hb₁u : b₁ ∉ u := fun h => (hust h).elim hb₁s hb₁t
          ⟨insert b₁ u, by simp [insert_subset_insert hust], Subset.trans hsu (by simp), by
            simp [Eq, hb₁t, hb₁s', hb₁u]⟩)
        fun this =>
        let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this
        have hb₂t' : b₂ ∉ s' ∪ t := fun h => hb₂t <| subset_span h
        have : s ⊆ (span K ↑(insert b₂ s' ∪ t) : Submodule K V) := fun b₃ hb₃ => by
          have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]
          have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
          have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
          have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
          rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃
        let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset_iff, hb₂s, hs']) hst this
        ⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu,
          by simp [eq, hb₂t', hb₁t, hb₁s']⟩

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = t.card
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r₁ r₂ : R
m₁ m₂ : M
inst✝ : Mul M
hm : Commute m₁ m₂
hr : Commute r₁ r₂
⊢ Commute (single m₁ r₁) (single m₂ r₂)

Tactic:
simp [Commute, SemiconjBy, hm.eq, hr.eq]

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

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
eq : f * (erase ag g₁ + single ag (g₁.coeff ag)) = f * (erase ag g₂ + single ag (g₁.coeff ag))
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
⊢ erase ag g₁ + single ag (g₁.coeff ag) = erase ag g₂ + single ag (g₁.coeff ag)

Tactic:
mul_add,

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
eq : f * erase ag g₁ + f * single ag (g₁.coeff ag) = f * erase ag g₂ + f * single ag (g₁.coeff ag)
⊢ erase ag g₁ + single ag (g₁.coeff ag) = erase ag g₂ + single ag (g₁.coeff ag)
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
h : l.toFinset.sort r = l
⊢ List.Pairwise r (l.toFinset.sort r)

Tactic:
exact pairwise_sort _ r

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
⊢ l.toFinset.sort r = l ↔ List.Pairwise r l

Tactic:
by
  refine ⟨?_, ((sort_perm_toList _ r).trans (List.toFinset_toList hl)).eq_of_pairwise'
    (pairwise_sort _ _)⟩
  intro h
  rw [← h]
  exact pairwise_sort _ r

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
g1 : G
h1 : g1 ∈ B * A
g2 : G
h2 : g2 ∈ B * A
hu : UniqueMul (B * A) (B * A) g1 g2
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1

Goal state after:
G : Type u_1
inst✝¹ : Semigroup G
inst✝ : IsCancelMul G
h : ∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueMul A A a1 a2
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
g2 : G
h2 : g2 ∈ B * A
b1 : G
hb1 : b1 ∈ B
a1 : G
ha1 : a1 ∈ A
h1 : b1 * a1 ∈ B * A
hu : UniqueMul (B * A) (B * A) (b1 * a1) g2
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit ↑s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
Set.isUnit_iff,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (∃ a, ↑s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a} ∧ IsUnit a
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ m ∈ ⨆ i, ⨆ (hi : i ∈ S), ⨆ (_ : ⟨i, hi⟩ ∈ s), i

Tactic:
iSup_subtype'

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i
s : Finset (Subtype (Membership.mem S))
hs : m ∈ ⨆ i ∈ s, ↑i
⊢ m ∈ ⨆ x, ⨆ (_ : ⟨↑x, ⋯⟩ ∈ s), ↑x
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p * q = ∑ i ∈ p.support, q.sum fun j a ↦ (monomial (i + j)) (p.coeff i * a)

Tactic:
apply toFinsupp_injective

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i ∈ p.support, q.sum fun j a ↦ (monomial (i + j)) (p.coeff i * a)).toFinsupp
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from rfl]
  exact Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive (Polynomial.C a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))
⊢ motive p

Tactic:
by
  have A : ∀ {n : ℕ} {a}, motive (Polynomial.C a * X ^ n) := by
    intro n a
    induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih
  have B : ∀ s : Finset ℕ, motive (s.sum fun n : ℕ ↦ Polynomial.C (p.coeff n) * X ^ n) := by
    apply Finset.induction
    · convert! C 0
      exact C_0.symm
    · intro n s ns ih
      rw [sum_insert ns]
      exact add _ _ A ih
  rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]
  exact B (support p)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (monomial n) (p.coeff n) + erase n p = p

Tactic:
apply toFinsupp_injective

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ((monomial n) (p.coeff n) + erase n p).toFinsupp = p.toFinsupp
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.update n 0 = erase n p

Tactic:
ext
  rw [coeff_update_apply, coeff_erase]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n f, f.range = N

Tactic:
simp_rw [fg_iff_exists_fin_generating_family, ← ((Pi.basisFun R _).constr ℕ).exists_congr_right]
  simp [Basis.constr_range]

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

Goal state before:
pp: case inr.inr.coe
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
⊢ a * ⨆ i, f i ≤ ↑d

Tactic:
have hlt : ⨆ i, f i < ⊤ := by
    rw [lt_top_iff_ne_top]
    intro htop
    obtain ⟨i, hi : d < f i⟩ := (iSup_eq_top ..).1 htop d (by simp)
    exact (((h i).trans_lt hi).trans_le (ENat.self_le_mul_left _ hne)).false

Goal state after:
case inr.inr.coe
ι : Sort u_2
a : ℕ∞
f : ι → ℕ∞
hne : a ≠ 0
hι : Nonempty ι
d : ℕ
h : ∀ (i : ι), a * f i ≤ ↑d
hlt : ⨆ i, f i < ⊤
⊢ a * ⨆ i, f i ≤ ↑d
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : i ≤ _k ∧ j ≤ _k
hi : i ≤ _k
hj : j ≤ _k
⊢ f i + g j ≤ f _k + g _k

Tactic:
by gcongr <;> apply_rules

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

Goal state before:
pp: a : ℕ∞
s : Set ℕ∞
⊢ sInf s + a = ⨅ b ∈ s, b + a

Tactic:
simp [sInf_eq_iInf, iInf_add]

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : Preorder ι
inst✝ : IsCodirectedOrder ι
f g : ι → ℕ∞
hf : Monotone f
hg : Monotone g
i j _k : ι
x✝ : _k ≤ i ∧ _k ≤ j
hi : _k ≤ i
hj : _k ≤ j
⊢ f _k + g _k ≤ f i + g j

Tactic:
by gcongr <;> apply_rules

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
⊢ x ∈ s.toList ↔ x ∈ s

Tactic:
RelSeries.toList,

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
x : α
⊢ x ∈ List.ofFn s.toFun ↔ x ∈ s
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
⊢ False

Tactic:
he.1,

Goal state after:
case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
he0 : a1 * b0 = (A * B).max' ⋯
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
⊢ False
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : a1 * b1 = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
⊢ False

Tactic:
he1

Goal state after:
case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
⊢ False
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t

Tactic:
suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
    simpa only [span_eq] using this

Goal state after:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
⊢ span R (image2 (fun m n ↦ (f m) n) {m} ↑s) = map (f m) (span R ↑s)

Tactic:
image2_singleton_left,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
⊢ span R ((fun n ↦ (f m) n) '' ↑s) = map (f m) (span R ↑s)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
iSup_subtype'

Goal state after:
case coe
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ height x ≤ ↑n ↔ ∀ y < x, height y < ↑n

Tactic:
by
  conv_lhs => rw [height_eq_iSup_lt_height, iSup₂_le_iff]
  congr! 2 with y _
  cases height y
  · simp
  · norm_cast

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length

Tactic:
obtain ⟨p₂, hhead, hlen₂⟩ := exists_series_of_coheight_eq_coe a hch

Goal state after:
case coe.coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
m : ℕ
hch : coheight a = ↑m
p₁ : LTSeries α
hlast : RelSeries.last p₁ = a
hlen₁ : p₁.length = n
p₂ : LTSeries α
hhead : RelSeries.head p₂ = a
hlen₂ : p₂.length = m
⊢ ↑n + ↑m ≤ ⨆ p, ↑p.length
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
i : Fin p.length
⊢ ((p.toFun i.castSucc).untop ⋯, (p.toFun i.succ).untop ⋯) ∈ {(a, b) | a < b}

Tactic:
by simpa [WithTop.untop_lt_iff, WithTop.coe_untop] using p.step i

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ y, ⨆ (_ : y ≠ ⊤), height y + 1 = ⨆ i, height i + 1

Tactic:
iSup_subtype'

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ ⨆ x, height ↑x + 1 = ⨆ i, height i + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: ⊢ krullDim (WithTop ℕ) = ⊤

Tactic:
simp [← WithBot.coe_top, ← WithBot.coe_one, ← WithBot.coe_add]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: α : Type u_2
inst✝ : CommMonoid α
n : ℕ
s : Set α
a : α
⊢ a ∈ s ^ n ↔ ∃ f, (∀ (i : Fin n), f i ∈ s) ∧ ∏ i, f i = a

Tactic:
simpa using mem_finsetProd (t := .univ) (f := fun _ : Fin n ↦ s) _

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = M * closure ↑N

Tactic:
closure_eq

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = M * N
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✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
⊢ 1 ⊆ ↑1

Tactic:
exact subset_coe_one

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : Semiring R
s : AddSubmonoid R
n : ℕ
⊢ s ^ n = closure ↑s ^ n

Tactic:
closure_eq

Goal state after:
R : Type u_2
inst✝ : Semiring R
s : AddSubmonoid R
n : ℕ
⊢ s ^ n = s ^ n
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : R
x✝ : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
⊢ x * b = 1

Tactic:
mul_zero,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x : R
x✝ : IsCoprime 0 x
a b : R
H : 0 + b * x = 1
⊢ x * b = 1
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : IsCoprime (0 0) (0 1)
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
h : IsCoprime 0 0
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

Goal state after: