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

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
⊢ ↑n + a = a

Tactic:
rw [add_comm, add_nat_eq n ha]

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

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + c < ℵ₀

Tactic:
rw [← h]

Goal state after:
a b c : Cardinal.{u_1}
h : a + b = a + c
ha : a < ℵ₀
hb : b < ℵ₀
hc : ℵ₀ ≤ c
⊢ a + b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
⊢ α + γ ≤ β + γ ↔ α ≤ β

Tactic:
refine ⟨fun h => ?_, fun h => by gcongr⟩
  contrapose h
  rw [not_le, lt_iff_le_and_ne, Ne] at h ⊢
  exact ⟨by grw [h.1], mt (add_right_inj_of_lt_aleph0 γ₀).1 h.2⟩

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

Goal state before:
pp: case inl
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ + μ₁ < κ₂ + μ₂

pp: case inr
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
⊢ κ₁ + μ₁ < κ₂ + μ₂

Tactic:
· refine add_lt_of_lt hinf ?_ ?_ <;> apply lt_of_lt_of_le <;> solve | assumption | simp

Goal state after:
case inr
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
⊢ κ₁ + μ₁ < κ₂ + μ₂
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case pos
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∀ (j : ι), r j i → f j < f i
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'

Tactic:
refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
      rw [bfamilyOfFamily'_typein]

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

Goal state before:
pp: case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof

Tactic:
rw [succ_eq_add_one, ← add_assoc, cof_add_one, cof_add_one]

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

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

pp: case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀

Tactic:
· rw [powerlt_le]
    exact fun _ a ↦ pow_le h a

Goal state after:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ max ℵ₀ #α = #α

Tactic:
max_eq_right

Goal state after:
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #α = #α

case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
b : Ordinal.{u_1}
hb : b ∈ Iio a
⊢ 2 ^ preBeth ↑⟨b, hb⟩ < c

Tactic:
exact hc.isStrongPrelimit <| IH _ hb (hb.trans ha)

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
a : (i_1 : ι) → i_1 ∈ i :: l → α i_1
⊢ (List.Pi.head fun x1 x2 ↦ ⟦a x1 x2⟧).liftOn₂ ⟦fun j hj ↦ a j ⋯⟧ (fun x1 x2 ↦ ⟦List.Pi.cons i l x1 x2⟧) ⋯ = ⟦a⟧

Tactic:
exact congrArg (⟦·⟧) (List.Pi.cons_eta a)

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
⊢ (f.sum g).support ⊆ f.support.biUnion fun i ↦ (g i (f i)).support

Tactic:
have :
    ∀ i₁ : ι,
      (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
    fun i₁ h =>
    let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨i, mem_support_iff.1 hi, Ne⟩

Goal state after:
ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (f.sum fun i b ↦ (g i b) i₁) ≠ 0 → ∃ i, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0
⊢ (f.sum g).support ⊆ f.support.biUnion fun i ↦ (g i (f i)).support
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → AddZeroClass (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
⊢ (sumZeroHom φ) f = f.sum fun x ↦ ⇑(φ x)

Tactic:
rcases f with ⟨f, s, hf⟩
  change (∑ i ∈ _, _) = ∑ i ∈ _ with _, _
  rw [Finset.sum_filter, Finset.sum_congr rfl]
  intro i _
  dsimp only [coe_mk', Subtype.coe_mk] at *
  split_ifs with h
  · rfl
  · rw [not_not.mp h, map_zero]

Goal state after:
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₂
x✝ : Dual R M₂
⊢ (∀ (x : M₁), (f.dualMap x✝) x = 0 x) ↔ x✝ ∈ f.range.dualAnnihilator

Tactic:
Submodule.mem_dualAnnihilator,

Goal state after:
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₂
x✝ : Dual R M₂
⊢ (∀ (x : M₁), (f.dualMap x✝) x = 0 x) ↔ ∀ w ∈ f.range, x✝ w = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case ha
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ ∀ (i : ι) (b : M i) (f : Π₀ (i : ι), M i),
    f i = 0 →
      b ≠ 0 →
        (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f →
          (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single i b + f)) =
            c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single i b + f)

Tactic:
intro a b f _ _ hf

Goal state after:
case ha
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f✝ : Π₀ (i : ι), M i
a : ι
b : M a
f : Π₀ (i : ι), M i
a✝¹ : f a = 0
a✝ : b ≠ 0
hf : (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f
⊢ (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • (single a b + f)) =
    c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) (single a b + f)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, (sumAddHom fun i ↦ (p i).subtype.toAddMonoidHom) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
DFinsupp.sumAddHom_apply,

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, (f.sum fun x ↦ ⇑(p x).subtype.toAddMonoidHom) = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range
m : M'
n : N'
p : P'
⊢ p = ((i.restrictScalarsRange₂ j k hk B hB) m) n ↔ k p = (B (i m)) (j n)

Tactic:
← restrictScalarsRange₂_apply i j k hk B hB m n,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
N' : Type u_7
P' : Type u_8
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : SMul S R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
inst✝¹² : Module S M
inst✝¹¹ : Module S N
inst✝¹⁰ : Module S P
inst✝⁹ : IsScalarTower S R M
inst✝⁸ : IsScalarTower S R N
inst✝⁷ : IsScalarTower S R P
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : Module S M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module S N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module S P'
inst✝ : SMulCommClass R S P
i : M' →ₗ[S] M
j : N' →ₗ[S] N
k : P' →ₗ[S] P
hk : Injective ⇑k
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range
m : M'
n : N'
p : P'
⊢ p = ((i.restrictScalarsRange₂ j k hk B hB) m) n ↔ k p = k (((i.restrictScalarsRange₂ j k hk B hB) m) n)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: 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

pp: 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)

Tactic:
· rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ hxy
    by_cases h_cases : x₁ = y₁
    · subst h_cases
      refine Sigma.eq rfl ?_
      rw [LinearIndependent.injective (hindep _) hxy]
    · have h0 : f x₁ x₂ = 0 := by
        apply
          disjoint_def.1 (hd x₁ {y₁} (finite_singleton y₁) fun h => h_cases (eq_of_mem_singleton h))
            (f x₁ x₂) (subset_span (mem_range_self _))
        rw [iSup_singleton]
        simp only at hxy
        rw [hxy]
        exact subset_span (mem_range_self y₂)
      exact False.elim ((hindep x₁).ne_zero _ h0)

Goal state after:
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.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst✝⁴ : DecidableEq ε
inst✝³ : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst✝² : DecidableEq ζ
inst✝¹ : DecidableEq ζ'
inst✝ : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ image2 f (image2 g ↑s ↑t) (image2 h ↑u ↑v) = image2 f' (image2 g' ↑s ↑u) (image2 h' ↑t ↑v)

Tactic:
exact image2_image2_image2_comm h_comm

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

Goal state before:
pp: 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)

Tactic:
| insert a s _ ih =>

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.Data.Finset.NAry

Goal state before:
pp: case h
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ↑(image Prod.fst u) ⊆ s ∧
    ↑(image Prod.snd u) ⊆ t ∧ image (fun x ↦ f x.1 x.2) u ⊆ image₂ f (image Prod.fst u) (image Prod.snd u)

Tactic:
simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right,
    image_subset_iff]

Goal state after:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
u : Finset (α × β)
hu : ↑u ⊆ s ×ˢ t
⊢ ↑u ⊆ Prod.fst ⁻¹' s ∧ ↑u ⊆ Prod.snd ⁻¹' t ∧ ∀ x ∈ u, f x.1 x.2 ∈ image₂ (fun a b ↦ f a.1 b.2) u u
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:
by 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✝ : 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:
by simp [Finsupp.mapDomain_add]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Mul M
⊢ ∀ (a b c : R[M]), a * (b + c) = a * b + a * c

Tactic:
by classical simp [mul_def, mul_add, sum_add, sum_add_index]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ AddMonoidHom.mul.compr₂ curryAddEquiv.toAddMonoidHom =
    (AddMonoidHom.mul.comp curryAddEquiv.toAddMonoidHom).compl₂ curryAddEquiv.toAddMonoidHom

Tactic:
by
    ext ⟨m₁, n₁⟩ r₁ ⟨m₂, n₂⟩ r₂; simp

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
h : l.toFinset.sort r = l
⊢ List.Pairwise r l

Tactic:
rw [← h]

Goal state after:
α : 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)
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (cons a s h₂).val.sort r = a :: s.sort r

Tactic:
cons_val,

Goal state after:
α : Type u_1
s : Finset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
a : α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ (a ::ₘ s.val).sort r = a :: s.sort r
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Inv α
s : Finset α
⊢ map opEquiv.toEmbedding s⁻¹ = (map opEquiv.toEmbedding s)⁻¹

Tactic:
by
  simp [map_eq_image, image_op_inv]

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

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Mul G
A B : Finset G
h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
hA : A.Nonempty
hB : B.Nonempty
hc : #A ≤ 1 ∧ #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
exact UniqueMul.of_card_le_one hA hB hc.1 hc.2

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : Type u_1
inst✝ : AddZeroClass M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)
⊢ Set.EqOn ⇑f ⇑g {p | ∃ n a, p = (monomial n) a}

Tactic:
rintro p ⟨n, a, rfl⟩
    exact h n a

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case disjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
⊢ Disjoint p f.ker

Tactic:
rw [disjoint_iff_inf_le]
    rintro x ⟨hpx, hfx⟩
    rw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
    simp only [hfx, zero_mem]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial

Tactic:
by
  refine ⟨fun h ↦ ⟨s 0, by simp [mem_def], s 1, by simp [mem_def],
    fun rid ↦ r.irrefl (s 0) ?_⟩, length_ne_zero_of_nontrivial⟩
  nth_rw 2 [rid]
  convert! s.step ⟨0, by lia⟩
  ext
  simpa [Nat.pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ s.length = 0 ↔ {x | x ∈ s}.Subsingleton

Tactic:
rw [← not_ne_iff, length_ne_zero, Set.not_nontrivial_iff]

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

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range ≤ g.ker
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N ⧸ f.range
⊢ (f.range.liftQ g h) x = 0 ↔ x = 0

Tactic:
obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x

Goal state after:
case mpr
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range ≤ g.ker
hfg : ∀ (x : N), g x = 0 ↔ ∃ y, f y = x
x : N
⊢ (f.range.liftQ g h) (Submodule.Quotient.mk x) = 0 ↔ Submodule.Quotient.mk x = 0
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
i : Fin 1
⊢ (![x, y] i.castSucc, ![x, y] i.succ) ∈ {(a, b) | a < b}

Tactic:
obtain rfl := Subsingleton.elim i 0

Goal state after:
α : Type u_1
inst✝ : Preorder α
H : ∀ (i : LTSeries α), ↑i.length ≤ 0
x y : α
h : x < y
⊢ (![x, y] (Fin.castSucc 0), ![x, y] (Fin.succ 0)) ∈ {(a, b) | a < b}
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y

Tactic:
simp_rw [← isMax_iff_forall_not_lt, ← krullDim_nonpos_iff_forall_isMax]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ ↑(height (RelSeries.last (LTSeries.longestOf α))) = krullDim α

Tactic:
refine le_antisymm (height_le_krullDim _) ?_
  rw [krullDim_eq_length_of_finiteDimensionalOrder, height]
  norm_cast
  exact le_iSup_iff.mpr <| fun _ h ↦ iSup_le_iff.mp (h _) le_rfl

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case ind
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n = ↑n

Tactic:
apply le_antisymm
  · apply height_le_coe_iff.mpr
    simp +contextual only [ih, Nat.cast_lt, implies_true]
  · exact length_le_height_last (p := LTSeries.range n)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ lift (lsmul R M ∘ₗ (mul R R) r) = (lsmul R M) r ∘ₗ lift (lsmul R M)

Tactic:
apply TensorProduct.ext'

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ∀ (x : R) (y : M), (lift (lsmul R M ∘ₗ (mul R R) r)) (x ⊗ₜ[R] y) = ((lsmul R M) r ∘ₗ lift (lsmul R M)) (x ⊗ₜ[R] y)
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ x ⊗ₜ[R] Pi.single i m j = Pi.single i (x ⊗ₜ[R] m) j

Tactic:
by_cases h : i = j <;> aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
N : Type u_8
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_22
inst✝² : DecidableEq ι
M : ι → Type u_23
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
i : ι
x : N
m : M i
j : ι
⊢ Pi.single i m j ⊗ₜ[R] x = Pi.single i (m ⊗ₜ[R] x) j

Tactic:
by_cases h : i = j <;> aesop

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

Goal state before:
pp: case refine_1
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
t : M ⊗[R] N
⊢ 0 ∈ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t}

Tactic:
exact Submodule.zero_mem _

Goal state after:
Module: Mathlib.Algebra.Ring.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
⊢ x * r ∣ y * r ↔ x ∣ y

Tactic:
← mul_comm r,

Goal state after:
R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
⊢ r * x ∣ r * y ↔ x ∣ y
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a b : α
hb : 1 ≤ b
⊢ b * a ≤ b → a∗ ≤ b

Tactic:
by
  simpa using mul_kstar_le hb

Goal state after: