mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ x ∈ {i, j}, g x • f x = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
ht' : t ⊆ {i, j}
⊢ ∀ x ∈ {i, j}, x ∉ t → g x • f x = 0

Tactic:
Finset.sum_pair hij

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
ht' : t ⊆ {i, j}
⊢ ∀ x ∈ {i, j}, x ∉ t → g x • f x = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep p
⊢ Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroup N ≃o _)] at h

Goal state after:
ι : Type u_1
N : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : AddCommGroup N
p : ι → AddSubgroup N
h : iSupIndep (⇑AddSubgroup.toIntSubmodule ∘ p)
⊢ Function.Injective ⇑(sumAddHom fun i ↦ (p i).subtype)
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

Tactic:
simp only [← h, eval_cons, add_smul, add_assoc]

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (r₂ • x + l₂.eval)) = r₁ • x + (r₂ • x + (l₁.eval + l₂.eval))
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
this : (a * d) • t = (b * c) • t
ht : ¬t = 0
⊢ False

Tactic:
exact h (_root_.smul_left_injective S ht ‹_›)

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

Goal state before:
pp: X : Type u_1
a : FreeAbelianGroup X
⊢ a.support.Nonempty ↔ a ≠ 0

Tactic:
contrapose!

Goal state after:
X : Type u_1
a : FreeAbelianGroup X
⊢ a.support = ∅ ↔ a = 0
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
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
⊢ y ∉ K ∙ x

Tactic:
simpa [mem_span_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image₂ f s t ⊆ image₂ f s' t'

Tactic:
rw [← coe_subset, coe_image₂, coe_image₂]
  exact image2_subset hs ht

Goal state after:
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 β
u : Finset γ
⊢ image₂ f s t ⊆ u ↔ ∀ b ∈ t, image (fun a ↦ f a b) s ⊆ u

Tactic:
simp_rw [image₂_subset_iff, image_subset_iff, @forall₂_comm α]

Goal state after:
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 β
⊢ image₂ f s t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
contrapose!

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ (image₂ f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2

Tactic:
calc
    (x * y).coeff m = ∑ m₁ ∈ x.coeff.support, ∑ m₂ ∈ y.coeff.support, F (m₁, m₂) := coeff_mul ..
    _ = ∑ p ∈ x.coeff.support ×ˢ y.coeff.support with p.1 * p.2 = m, x.coeff p.1 * y.coeff p.2 := by
      rw [Finset.sum_filter, Finset.sum_product]
    _ = ∑ p ∈ s with p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support, x.coeff p.1 * y.coeff p.2 := by
      congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
    _ = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2 :=
      sum_subset (filter_subset _ _) fun p hps hp => by
        simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
        by_cases h1 : x.coeff p.1 = 0
        · rw [h1, zero_mul]
        · rw [hp hps h1, mul_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Nontrivial R
a b : M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
by
  simpa [← coeff_inj, Finsupp.single_eq_single_iff] using h

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
m : M
r : R
⊢ motive (ofCoeff (Finsupp.single m r))

Tactic:
by simpa using smul r (.of R M m) (of m)

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

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

Tactic:
simp [curryAddEquiv]

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

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

Tactic:
simp [curryAddEquiv]

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

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x * y).coeff g = x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)

Tactic:
rw [coeff_mul]; gcongr; simp +contextual [← eq_inv_mul_iff_mul_eq]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : AddZeroClass M
a b : Multiplicative M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
by
  simpa [← coeff_inj, Finsupp.single_eq_single_iff] using h

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

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

Tactic:
contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.zpow
    · simp

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
a : (i : κ) → π i
⊢ a ∈ pi ∅ L ↔ a ∈ ⊤

Tactic:
by simp [mem_pi]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
a : (i : κ) → π i
⊢ (a ∈ pi s fun x ↦ ⊤) ↔ a ∈ ⊤

Tactic:
by simp [mem_pi]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeffs = ∅ → p = 0

Tactic:
contrapose!

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p ≠ 0 → p.coeffs.Nonempty
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
G : Type u_3
inst✝² : Monoid G
inst✝¹ : DistribMulAction G M
inst✝ : SMulCommClass G R M
x : M
g : G
⊢ span R (MulAction.orbit G x) ∈ invtSubmodule (DistribSMul.toLinearMap R M g)

Tactic:
by
  rw [mem_invtSubmodule, Submodule.span_le, Submodule.comap_coe]
  intro y hy
  simp only [Set.mem_preimage, DistribSMul.toLinearMap_apply, SetLike.mem_coe]
  exact Submodule.subset_span <| MulAction.mem_orbit_of_mem_orbit g hy

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

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

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
hpq : IsCompl p q
x : E
⊢ x - (p.projection q hpq) x = 0 ↔ x ∈ p
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = ↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯).symm

Tactic:
rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
  ext x
  · simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inl, coprod_apply, coe_subtype,
      map_zero, add_zero, h.map_id x x.2, prodMap_apply, id_apply]
  · simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, map_zero,
      coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊤ ↔ f = id

Tactic:
constructor <;> rintro rfl

Goal state after:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊤ f
⊢ f = id

case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m id
⊢ m = ⊤
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
⊢ m = ⊥ ↔ f = 0

Tactic:
constructor <;> rintro rfl

Goal state after:
case mp
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
hf : IsProj ⊥ f
⊢ f = 0

case mpr
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
hf : IsProj m 0
⊢ m = ⊥
Module: Mathlib.Data.Rel

Goal state before:
pp: case mpr.mp
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ Function.graph f → (a, b) ∈ R

pp: case mpr.mpr
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ R → (a, b) ∈ Function.graph f

Tactic:
· aesop

Goal state after:
case mpr.mpr
α : Type u_1
β : Type u_2
R : SetRel α β
h : ∀ (a : α), ∃! b, (a, b) ∈ R
f : α → β
hf : ∀ (x : α), (x, f x) ∈ R
a : α
b : β
⊢ (a, b) ∈ R → (a, b) ∈ Function.graph f
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_1.left
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring 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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
z : M
hz : f z = x - y
⊢ x = y

Tactic:
← sub_eq_zero,

Goal state after:
case refine_1.left
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring 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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring 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 : Exact ⇑f ⇑g
hg : Surjective ⇑g
l : { l // l ∘ₗ f = LinearMap.id }
h₁ : ∀ (x : M), ↑l (f x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : N
e : ↑l x = ↑l y ∧ g x = g y
z : M
hz : f z = x - y
⊢ x - y = 0
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
⊢ (p.smash q h).last = q.last

Tactic:
dsimp only [smash, last]

Goal state after:
α : Type u_1
r : SetRel α α
p q : RelSeries r
h : p.last = q.head
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.last (p.length + q.length)) = q.toFun (Fin.last q.length)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: 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 : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑f ↔ g.ker = ⊤

Tactic:
h.linearMap_ker_eq,

Goal state after:
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 : Function.Exact ⇑f ⇑g
⊢ Function.Surjective ⇑f ↔ f.range = ⊤
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case mp
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (x : RelSeries r), ∃ y, x.length < y.length) → ∀ (n : ℕ), ∃ x, x.length = n

pp: case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length

Tactic:
· intro H n
    induction n with
    | zero => refine ⟨⟨0, ![_root_.Nonempty.some ‹_›], by simp⟩, by simp⟩
    | succ n IH =>
      obtain ⟨l, hl⟩ := IH
      obtain ⟨l', hl'⟩ := H l
      exact ⟨l'.take ⟨n + 1, by simpa [hl] using hl'⟩, rfl⟩

Goal state after:
case mpr
α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ (∀ (n : ℕ), ∃ x, x.length = n) → ∀ (x : RelSeries r), ∃ y, x.length < y.length
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: 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 : Function.Exact ⇑f ⇑g
⊢ g.ker = ⊥ ↔ f = 0

Tactic:
h.linearMap_ker_eq,

Goal state after:
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 : Function.Exact ⇑f ⇑g
⊢ f.range = ⊥ ↔ f = 0
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
⊢ f = g

Tactic:
have feq := fun i ↦ congr($(e).toFun i)

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝¹ : Preorder α
inst✝ : Preorder β
n : ℕ
lf : Fin n
f : Fin (↑lf + 1) → α
mf : StrictMono f
g : Fin (↑lf + 1) → α
mg : StrictMono g
e : mk (↑lf) f ⋯ = mk (↑lf) g ⋯
feq : ∀ (i : Fin ((mk (↑lf) f ⋯).length + 1)), (mk (↑lf) f ⋯).toFun i = (mk (↑lf) g ⋯).toFun i
⊢ f = g
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
m : ℕ
h : n ≤ m
ha : ⨆ x, ↑(↑x).length = ↑m
p : LTSeries α
hlast : RelSeries.last p = a
hlen : p.length = m
⊢ (RelSeries.drop p ⟨m - n, ⋯⟩).length = n

Tactic:
· simp [hlen]; lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.mp
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.head p = x ∧ p.length = n) → ∃ p, RelSeries.last p = x ∧ p.length = n

Tactic:
intro ⟨p, hp, hl⟩

Goal state after:
case e'_2.mp
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ ∃ p, RelSeries.last p = x ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case e'_2.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
⊢ (∃ p, RelSeries.last p = x ∧ p.length = n) → ∃ p, RelSeries.head p = x ∧ p.length = n

Tactic:
intro ⟨p, hp, hl⟩

Goal state after:
case e'_2.mpr
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ ∃ p, RelSeries.head p = x ∧ p.length = n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ 0 ≤ krullDim α ↔ Nonempty α

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α < 0 ↔ IsEmpty α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ (∀ (i : LTSeries α), ↑i.length ≤ 1) ↔ ∀ (x : α), (∀ (b : α), ¬b < x) ∨ ∀ (b : α), ¬x < b

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ (∃ i, 1 < ↑i.length) ↔ ∃ x, (∃ b, b < x) ∧ ∃ b, x < b
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ 0 < krullDim α ↔ ∃ x y, x < y

Tactic:
contrapose!

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x y : α), ¬x < y
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: n : ℕ
⊢ coheight ↑n = ⊤

Tactic:
apply (coheight_coe_withTop _).trans

Goal state after:
n : ℕ
⊢ coheight n + 1 = ⊤
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
⊢ map LinearMap.id LinearMap.id = LinearMap.id

Tactic:
by
  ext
  simp only [mk_apply, id_coe, compr₂ₛₗ_apply, _root_.id, map_tmul]

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✝ : IdemSemiring α
a✝ b✝ c✝ a b c : α
hbc : (fun x1 x2 ↦ x1 ≤ x2) b c
⊢ (fun x1 x2 ↦ x1 * x2) a c + (fun x1 x2 ↦ x1 * x2) a b = (fun x1 x2 ↦ x1 * x2) a c

Tactic:
by rw [← mul_add, hbc.add_eq_left]

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

Goal state before:
pp: case refine_2
M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
m : R
hm : m ∈ x
n : R
hn : n ∈ y
⊢ -m * n ∈ -x * y

Tactic:
exact mul_mem_mul (neg_mem_neg.2 hm) hn

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Finite α
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
⊢ ∃ x₀, ∀ (x : α), f x₀ ≤ f x

Tactic:
cases nonempty_fintype α
  simpa using exists_min_image univ f univ_nonempty

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ ↑u * ↑a + ↑v * ↑b = 1

Tactic:
rw_mod_cast [H]

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ ↑1 = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
A : Type v
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
M : Submodule R A
⊢ M ^ 1 = M

Tactic:
rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 ↦ x • x_1) y' = y
⊢ y ∈ ↑I

Tactic:
rw [← xy'_eq_y]; exact h _ hy'

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : (⊤.prod I).IsPrime
⊢ I.IsPrime

Tactic:
apply isPrime_of_isPrime_prod_top (S := R)

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal S
h : (⊤.prod I).IsPrime
⊢ (I.prod ⊤).IsPrime
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).IsPrime → I = ⊤ ∨ J = ⊤

Tactic:
contrapose!

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
E : Type u_4
inst✝¹ : EquivLike E R S
inst✝ : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ y ∈ map e I ↔ ∃ x ∈ I, e x = y

Tactic:
constructor
  · intro h
    simp_rw [show map e I = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : R ≃+* S)] at h
    exact ⟨(EquivLike.toEquiv e).symm y, h, (EquivLike.toEquiv e).apply_symm_apply y⟩
  · rintro ⟨x, hx, rfl⟩
    exact mem_map_of_mem e hx

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K.radical = (comap f K).radical

Tactic:
by
  ext
  simp [radical]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : g * s / g = 0
⊢ g * s = 0

Tactic:
rw [mul_div_cancel_left₀ _ hgxy] at hy

Goal state after:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : s = 0
⊢ g * s = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - y * z) / y = x / y - z

Tactic:
exact sub_mul_div_left _ _ _ h1 h2

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x ↦ a * x) s).gcd = normalize a * s.gcd
⊢ (map (fun x ↦ a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd

Tactic:
· simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
    rw [ih]
    apply ((normalize_associated a).mul_right _).gcd_eq_right

Goal state after: