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

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c * c = c

Tactic:
by
  -- The only nontrivial part is `c * c ≤ c`. We prove it inductively.
  induction c using WellFoundedLT.induction with | ind c IH
  refine le_antisymm ?_ (by simpa using mul_le_mul_right (one_le_aleph0.trans hc) c)
  -- Consider the minimal well-order on `α` (a type with cardinality `c`).
  induction c using Cardinal.inductionOn with | mk α
  obtain ⟨_, _, hα⟩ := exists_ord_eq_type_lt α
  have : NoMaxOrder α := by
    rw [← isSuccPrelimit_type_lt_iff, ← hα]
    exact (isSuccLimit_ord hc).isSuccPrelimit
  -- Define an order `s` on `α × α`, comparing first by `max x.1 x.2`, then by `toLex (x.1, x.2)`.
  let g : α × α → α := uncurry max
  let f : α × α ↪ α ×ₗ (α ×ₗ α) := ⟨fun p ↦ toLex (g p, toLex p), fun p q ↦ congrArg Prod.snd⟩
  let s := f ⁻¹'o (· < ·)
  have : IsWellOrder _ s := (RelEmbedding.preimage ..).isWellOrder
  -- Every initial segment of `s` is contained in `β × β` for some `β` of cardinality `< c`.
  -- By the inductive hypothesis, this means `#(β × β) < c`. Thus, `α × α` must have
  -- cardinality `≤ c`.
  refine @card_le_card (type s) (typeLT α) <| le_of_forall_lt fun o h ↦ ?_
  obtain ⟨p, rfl⟩ := typein_surj s h
  obtain ⟨q, hq'⟩ := exists_gt (g p)
  rw [← hα, lt_ord]
  apply lt_of_le_of_lt (b := #(Iio q) * #(Iio q))
  · apply (Set.embeddingOfSubset { x | s x p } ..).cardinal_le.trans_eq (mk_setProd ..)
    simp [s, f, Prod.Lex.lt_iff, subset_def]
    grind
  rcases lt_or_ge #(Iio q) ℵ₀ with hq | hq
  · exact (mul_lt_aleph0 hq hq).trans_le hc
  · have := mk_Iio_lt q hα
    rwa [IH _ this hq]

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

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

Tactic:
by
  rcases le_or_gt ℵ₀ b with hb | hb
  · exact mul_eq_max h hb
  refine (mul_le_max_of_aleph0_le_left h).antisymm ?_
  have : b ≤ a := hb.le.trans h
  rw [max_eq_left this]
  convert! mul_le_mul_right (Cardinal.one_le_iff_ne_zero.mpr h') a
  rw [mul_one]

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

Goal state before:
pp: case inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ 0)

pp: case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ o)

Tactic:
· rw [omega_zero]
    exact isPrincipal_opow_omega0

Goal state after:
case inr
o : Ordinal.{u_1}
ho : 0 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 ^ x2) (ω_ o)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase i f) j = (f - single i (f i)) j

Tactic:
· simp [erase_ne h, single_eq_of_ne h]

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
f✝ : Π₀ (i : ι), β i
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : f i = 0
h2 : b ≠ 0
h3 : p f
j : ι
H : ¬i = j
⊢ (f + single i b) j = (single i b + f) j

Tactic:
· simp [H]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
⊢ Function.LeftInverse (fun f ↦ ⟨mk s fun i ↦ ↑(f i), ⋯⟩) fun x ↦
    match (motive := { f // f.support = s } → (i : ↥s) → { x // x ≠ 0 }) x with
    | ⟨f, hf⟩ => fun x ↦
      match x with
      | ⟨i, hi⟩ => ⟨f i, ⋯⟩

Tactic:
rintro ⟨f, rfl⟩
    ext i
    simpa using Eq.symm

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
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ d • a • s = -(d • c • t)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← smul_add, h₁, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p')
hx : ↑x ∈ p
⊢ Submodule.Quotient.mk x = (quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk ⟨↑x, hx⟩)

Tactic:
by
    rw [quotientInfEquivSupQuotient_apply_mk, inclusion_apply]

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

Goal state before:
pp: case pos
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
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
simp only [hbd.1, hbd.2, zero_smul, add_zero]
      by_cases hac : a = 0 ∧ c = 0; · exact ⟨1, 0, by simp [hac.1, hac.2], by simp⟩
      refine ⟨c • 1, -a • 1, ?_, by aesop⟩
      simp only [smul_assoc, one_smul, neg_smul]
      module

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a b : FreeAbelianGroup X
⊢ (a + b).support ⊆ a.support ∪ b.support

Tactic:
simp only [support, map_add]

Goal state after:
X : Type u_1
a b : FreeAbelianGroup X
⊢ (toFinsupp a + toFinsupp b).support ⊆ (toFinsupp a).support ∪ (toFinsupp b).support
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
a b : FreeAbelianGroup X
⊢ (a + b).support ⊆ a.support ∪ b.support

Tactic:
by
  simp only [support, map_add]
  apply Finsupp.support_add

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
i : ι
hs : LinearIndepOn R v s
hx : ∀ (r : R), r • v i ∈ span R (v '' s) → r = 0
⊢ LinearIndepOn R v (insert i s)

Tactic:
by
  rw [← Set.union_singleton]
  refine hs.union (.singleton' fun r hr ↦ hx _ <| by simp [hr]) ?_
  simp +contextual [disjoint_span_singleton'', hx]

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

Goal state before:
pp: case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ∑ a, ψ a = 0

Tactic:
refine eq_zero_of_mul_eq_self_left hx ?_

Goal state after:
case neg
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : Decidable (ψ = 0)
h : ¬ψ = 0
x : A
hx : ψ x ≠ 1
⊢ ψ x * ∑ a, ψ a = ∑ a, ψ a
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ ψ (↑n * x) = ψ x ^ n

Tactic:
← nsmul_eq_mul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ ψ (n • x) = ψ x ^ n
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
⊢ LinearIndependent R (Fin.snoc v x)

Tactic:
apply hv.finSnoc' v x
  intro c y hcy heq
  by_contra hc
  apply hx
  have hc' : algebraMap R K c ≠ 0 := by
    rwa [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff]
  rw [← algebraMap_smul K c x] at heq
  rw [(eq_inv_smul_iff₀ hc').mpr (eq_neg_of_add_eq_zero_left heq), smul_neg]
  exact Submodule.neg_mem _ (Submodule.smul_mem _ _ (Submodule.span_subset_span R K _ hcy))

Goal state after:
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 ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a

Tactic:
| succ n ih =>

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✝ : Semigroup M
⊢ ∀ (a b c : R[M]), a * b * c = a * (b * c)

Tactic:
by simp [mul_def, sum_sum_index, mul_add, add_mul, mul_assoc]

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

Goal state before:
pp: case refine_1
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
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ a * x.coeff 1 = 1

Tactic:
simpa [coeff_single_one_mul] using congr(($hax).coeff 1)

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

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ {ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton

Tactic:
rintro ⟨x1, y1⟩ (hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0) ⟨x2, y2⟩
    (hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0)
  rcases h hx.1 hx.2.1 hx.2.2 with ⟨rfl, rfl⟩
  rcases h hy.1 hy.2.1 hy.2.2 with ⟨rfl, rfl⟩
  rfl

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

Goal state before:
pp: case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (n + 1) s) = ↑s ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < (s.sort fun a b ↦ a ≤ b).length

Tactic:
rw [length_sort, h]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < k
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b2
⊢ b1 = b2

Tactic:
by
    classical
    have := mem_insert_self b1 {b2}
    obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩
    cases mem_singleton.mp ha
    simp_rw [mem_insert, mem_singleton] at hb
    obtain rfl | rfl := hb
    · exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm
    · exact (hu ha this he).2

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
m n : ℕ
a b : R
⊢ (monomial m) a = (monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, single_inj]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
n : ℕ
ih : (monomial n) 1 = X ^ n
⊢ (monomial (n + 1)) 1 = X ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ (n + 1) * p = p * X ^ (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: case refine_3
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 : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
this :
  ∃ a0 ∈ image (fun x ↦ x⁻¹) D * C,
    ∃ b0 ∈ D * image (fun x ↦ x⁻¹) C, UniqueMul (image (fun x ↦ x⁻¹) D * C) (D * image (fun x ↦ x⁻¹) C) a0 b0
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
obtain ⟨e, he, f, hf, hu⟩ := this

Goal state after:
case refine_3
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 : Finset G := map { toFun := fun x ↦ a⁻¹ * x, inj' := ⋯ } A
D : Finset G := map { toFun := fun x ↦ x * b⁻¹, inj' := ⋯ } B
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
e : G
he : e ∈ image (fun x ↦ x⁻¹) D * C
f : G
hf : f ∈ D * image (fun x ↦ x⁻¹) C
hu : UniqueMul (image (fun x ↦ x⁻¹) D * C) (D * image (fun x ↦ x⁻¹) C) e f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: case succ
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))
a : R
n : ℕ
ih : motive (Polynomial.C a * X ^ n)
⊢ motive (Polynomial.C a * X ^ (n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: case empty
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))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ motive (∑ n ∈ ∅, Polynomial.C (p.coeff n) * X ^ n)

pp: case insert
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))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ ∀ (a : ℕ) (s : Finset ℕ),
    a ∉ s →
      motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n) → motive (∑ n ∈ insert a s, Polynomial.C (p.coeff n) * X ^ n)

Tactic:
· convert! C 0
      exact C_0.symm

Goal state after:
case insert
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))
A : ∀ {n : ℕ} {a : R}, motive (Polynomial.C a * X ^ n)
⊢ ∀ (a : ℕ) (s : Finset ℕ),
    a ∉ s →
      motive (∑ n ∈ s, Polynomial.C (p.coeff n) * X ^ n) → motive (∑ n ∈ insert a s, Polynomial.C (p.coeff n) * X ^ n)
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : p ∈ f.invtSubmodule
hq : q ∈ f.invtSubmodule
⊢ IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl p q

Tactic:
by
  simp [isCompl_iff]

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

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ Nontrivial R[X]

Tactic:
have h : Nontrivial R[ℕ] := by infer_instance
  rcases h.exists_pair_ne with ⟨x, y, hxy⟩
  refine ⟨⟨⟨x⟩, ⟨y⟩, ?_⟩⟩
  simp [hxy]

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

Goal state before:
pp: case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (linearCombination R id) l - f ((linearCombination R id) ((lmapDomain R R g) l)) = 0

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply]

Goal state after:
case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ (l.sum fun i a ↦ a • id i) - f ((mapDomain g l).sum fun i a ↦ a • id i) = 0
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:
← not_ne_iff,

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
⊢ ¬s.length ≠ 0 ↔ {x | x ∈ s}.Subsingleton
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
⊢ (p.snoc newLast rel).head = p.head

Tactic:
delta snoc

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
⊢ (p.append (singleton r newLast) rel).head = p.head
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 1 = 1 % (p.length + 1)

Tactic:
rw [Nat.mod_eq_of_lt]

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 1 < p.length + 1
Module: Mathlib.Order.KrullDimension

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

Tactic:
exact length_le_height_last (p := LTSeries.range n)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case step
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
f : ℕ → ↑(Set.Ioi a)
hstrictmono : StrictMono f
m : ℕ
⊢ ∀ (i : Fin m),
    (if i.castSucc = 0 then a else ↑(f ↑i.castSucc), if i.succ = 0 then a else ↑(f ↑i.succ)) ∈ {(a, b) | a < b}

Tactic:
case step =>
    intro ⟨i, hi⟩
    by_cases hzero : i = 0
    · subst i
      exact (f 1).prop
    · suffices f i < f (i + 1) by simp [Fin.ext_iff, hzero, this]
      apply hstrictmono
      lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMinOrder α
⊢ krullDim α = ⊤

Tactic:
by
  simp [krullDim_eq_iSup_height, height_of_noMinOrder]

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
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑(RelSeries.take p i).length ≤ (↑m + 1) * ↑n' + ↑m
⊢ False

Tactic:
RelSeries.take_length,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑↑i ≤ (↑m + 1) * ↑n' + ↑m
⊢ False
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
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * ↑n' + (↑m + (↑m + 1))
⊢ False

Tactic:
add_comm _ (_ + 1),

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * ↑n' + (↑m + 1 + ↑m)
⊢ False
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: case le
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
sR : Set R
N : Submodule R M
inst✝ : SMulCommClass R R ↥N
⊢ map (N.subtype ∘ₗ (Finsupp.lsum R) (DistribSMul.toLinearMap R ↥N)) (Finsupp.supported (↥N) R sR) ≤ sR • N

Tactic:
intro x hx
    obtain ⟨c, hc, rfl⟩ := hx
    simp only [LinearMap.coe_comp, coe_subtype, Finsupp.coe_lsum, Finsupp.sum, Function.comp_apply]
    rw [AddSubmonoid.coe_finsetSum]
    refine Submodule.sum_mem (p := sR • N) (t := c.support) ?_ _ ⟨sR • N, ?_⟩
    · rintro r hr
      rw [mem_set_smul_def, Submodule.mem_sInf]
      rintro p hp
      exact hp (hc hr) (c r).2
    · ext x : 1
      simp only [Set.mem_iInter, SetLike.mem_coe]
      fconstructor
      · refine fun h ↦ h fun r n hr hn ↦ ?_
        rw [mem_set_smul_def, mem_sInf]
        exact fun p hp ↦ hp hr hn
      · simp_all

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

Goal state before:
pp: case succ
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 : ℕ
ih : map f g ^ n = map (f ^ n) (g ^ n)
⊢ map f g ^ (n + 1) = map (f ^ (n + 1)) (g ^ (n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
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 : ℕ
ih : congr f g ^ n = congr (f ^ n) (g ^ n)
⊢ congr f g ^ (n + 1) = congr (f ^ (n + 1)) (g ^ (n + 1))

Tactic:
| succ n ih =>

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime y z
hdvd : x ∣ y
⊢ IsCoprime x z

Tactic:
obtain ⟨d, rfl⟩ := hdvd

Goal state after:
R : Type u
inst✝ : CommSemiring R
x z d : R
h : IsCoprime (x * d) z
⊢ IsCoprime x z
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (y * z - x) y ↔ IsCoprime x y

Tactic:
sub_eq_neg_add,

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y z : R
⊢ IsCoprime (z * y - x) y ↔ IsCoprime x y

Tactic:
sub_eq_neg_add,

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (y * z - x) y ↔ IsRelPrime x y

Tactic:
sub_eq_neg_add,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x y z : R
⊢ IsRelPrime (-x + y * z) y ↔ IsRelPrime x y