mathlib-initiative/mathlib-tactics huggingface dataset:
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'

pp: case neg
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 i ≤ f j
⊢ ∃ 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:
case neg
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 i ≤ f j
⊢ ∃ i', ∃ (hi' : i' < type r'), f i ≤ bfamilyOfFamily' r' (fun i ↦ f ↑i) i' hi'
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : ¬Bounded r s
⊢ (type r).cof ≤ #↑s

Tactic:
rw [not_bounded_iff] at hs

Goal state after:
case inr.a
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
s : Set α
hs : Unbounded r s
⊢ (type r).cof ≤ #↑s
Module: Mathlib.Data.DFinsupp.Submonoid

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

Tactic:
refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) (single i ⟨y, hy⟩) = y
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ filter p (single i x) = 0

Tactic:
rw [filter_single, if_neg h]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : Semiring γ
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → Module γ (β i)
c : Π₀ (i : ι), β i
i : ι
⊢ (0 • c) i = 0 i

Tactic:
by simp only [smul_apply, zero_smul, zero_apply]

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

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

Tactic:
congr 1

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

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

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

Tactic:
(hf i).resolve_left H2,

Goal state after:
case mk.mk.e_a.refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
a✝ : i ∈ (sf + sg).toFinset
H2 : i ∉ sf
⊢ (φ i) 0 = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ((subtypeDomain p v).prod fun i b ↦ h (↑i) b) = v.prod h

Tactic:
refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, ↑a ∈ v.support

case refine_2
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ a₁ ∈ (subtypeDomain p v).support, ∀ a₂ ∈ (subtypeDomain p v).support, ↑a₁ = ↑a₂ → a₁ = a₂

case refine_3
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ b ∈ v.support, ∃ a, ∃ (_ : a ∈ (subtypeDomain p v).support), ↑a = b

case refine_4
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ∀ a ∈ (subtypeDomain p v).support, (fun i b ↦ h (↑i) b) a ((subtypeDomain p v) a) = h (↑a) (v ↑a)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s • x + 0 • y = 0 • x + t • y

Tactic:
by simpa using h'

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

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

Tactic:
refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ (((lsum ℕ) fun i ↦ (S i).subtype) ∘ₗ filterLinearMap R (fun i ↦ ↥(S i)) p) (single i ⟨y, hy⟩) = y
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
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
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
suffices ¬ LinearIndependent R ![a • x + b • y, c • x + d • y] by simpa [h]

Goal state after:
case inl
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
⊢ ¬LinearIndependent R ![a • x + b • y, c • x + d • y]
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_2
x : FreeAbelianGroup X
⊢ toFreeAbelianGroup (toFinsupp x) = x

Tactic:
rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun i j ↦ (f i) (v j) = 0
h2 : ∀ (i : ι), (f i) (v i) = 1
s : Finset ι
g : ι → R
hrel : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = 0

Tactic:
have aux (j : ι) (hjs : j ∈ s) (hji : j ≠ i) : g j * (f i) (v j) = 0 := by simp [h1 hji.symm]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
f : ι → Dual R M
h1 : Pairwise fun i j ↦ (f i) (v j) = 0
h2 : ∀ (i : ι), (f i) (v i) = 1
s : Finset ι
g : ι → R
hrel : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
aux : ∀ j ∈ s, j ≠ i → g j * (f i) (v j) = 0
⊢ g i = 0
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
x✝ : R
⊢ 1 = 1 x✝

Tactic:
one_apply

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ 1 = 1
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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

Tactic:
by
  rw [h.mem_span_iff, Classical.not_imp]

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s✝ : Set ι
M : Type u_4
M' : Type u_5
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set V
x y : V
n : ℕ
x✝ : { s // LinearIndependent K s }
⊢ (fun s ↦ ⟨Fin.cons ↑s.snd ↑s.fst, ⋯⟩) ((fun s ↦ ⟨⟨Fin.tail ↑s, ⋯⟩, ⟨↑s 0, ⋯⟩⟩) x✝) = x✝

Tactic:
by simp only [Fin.cons_self_tail, Subtype.coe_eta]

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'
⊢ image2 f ↑s ↑t ⊆ image2 f ↑s' ↑t'

Tactic:
exact image2_subset hs ht

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

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
l : List α
⊢ (∀ (b : α), b ∈ Quot.mk (⇑(isSetoid α)) l → r a b) →
    (a ::ₘ Quot.mk (⇑(isSetoid α)) l).sort r = a :: sort (Quot.mk (⇑(isSetoid α)) l) r

Tactic:
simpa [mergeSort_eq_insertionSort] using insertionSort_cons_of_forall_rel r (a := a) (l := l)

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

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid α
n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ ↑(univ ^ n) = ↑univ

Tactic:
coe_pow,

Goal state after:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Monoid α
n : ℕ
inst✝ : Fintype α
hn : n ≠ 0
⊢ ↑univ ^ n = ↑univ
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
⊢ Free R' M'

Tactic:
let I := Module.Free.ChooseBasisIndex R M

Goal state after:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Semiring R'
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst✝ : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
⊢ Free R' M'
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ span R (⇑((lsum R) fun x ↦ f x • φ) '' {x | ∃ i x_1, single i x_1 = x}) = span R (Set.range f • ⇑φ '' univ)

Tactic:
congr 1

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
σ : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
φ : M →ₗ[R] N
f : σ → R
⊢ ⇑((lsum R) fun x ↦ f x • φ) '' {x | ∃ i x_1, single i x_1 = x} = Set.range f • ⇑φ '' univ
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ n ∈ p.support ↔ p.coeff n ≠ 0

Tactic:
by
  rcases p with ⟨⟩
  simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a} = ⊤

Tactic:
by
  apply top_unique
  rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ← addSubmonoidClosure_single,
    AddMonoidHom.map_mclosure]
  refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)
  rintro _ ⟨n, a, rfl⟩
  exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
n : ℕ
⊢ (↑n).succ = ↑n + 1

Tactic:
← WithBot.coe_natCast,

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
n : ℕ
⊢ (↑↑n).succ = ↑n + 1
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
R : SetRel α α
inst✝ : R.IsRefl
fst✝ : α
⊢ (fst✝, fst✝) ∈ R

Tactic:
exact R.rfl

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:
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⟩

Goal state after:
α : Type u_1
r : SetRel α α
s : RelSeries r
inst✝ : r.IsIrrefl
h : s.length ≠ 0
rid : s.toFun 0 = s.toFun 1
⊢ (s.toFun 0, s.toFun 0) ∈ r
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 : (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
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
⊢ False

Tactic:
refine (min'_lt_max' _ (mul_mem_mul ha0 hb0) (mul_mem_mul h2.1 h2.2) fun he ↦ hne ?_).ne he0

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
a2 b2 : G
h2 : (a2, b2).1 ∈ A ∧ (a2, b2).2 ∈ B
hne : (a2, b2) ≠ (a0, b0)
he : a0 * b0 = (a2, b2).1 * (a2, b2).2
⊢ (a2, b2) = (a0, b0)
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ (LinearMap.snd R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inl R M N)

Tactic:
simp only [LinearMap.snd_apply, @eq_comm _ y, LinearMap.coe_inl, Set.mem_range, Prod.mk.injEq,
    exists_eq_left]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4.h
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ i.succ.castSucc < m.succ

Tactic:
change i.1 + 1 < m.1 + 1; lia

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
⊢ ∃ y ∈ Set.range fun x_1 ↦ (↑x_1).length, n < y

Tactic:
obtain ⟨p, hlast, hp⟩ := h (n + 1)

Goal state after:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
p : LTSeries α
hlast : RelSeries.last p = x
hp : p.length = n + 1
⊢ ∃ y ∈ Set.range fun x_1 ↦ (↑x_1).length, n < y
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Subsingleton α
⊢ krullDim α ≤ 0

Tactic:
rw [krullDim_nonpos_iff_forall_isMax]
  exact fun x y h ↦ (Subsingleton.elim x y).ge

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
ih : ∀ (hj : j < p.length + 1), p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, hj⟩ + i
hj : j + 1 < p.length + 1
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i

Tactic:
specialize ih (Nat.lt_of_succ_lt hj)

Goal state after:
case succ
p : LTSeries ℕ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + j ≤ p.toFun ⟨j, ⋯⟩ + i
⊢ p.toFun ⟨i, hi⟩ + (j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ
p : LTSeries ℤ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
ih : ∀ (hj : j < p.length + 1), p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun ⟨j, hj⟩ + ↑i
hj : j + 1 < p.length + 1
⊢ p.toFun ⟨i, hi⟩ + ↑(j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + ↑i

Tactic:
specialize ih (Nat.lt_of_succ_lt hj)

Goal state after:
case succ
p : LTSeries ℤ
i✝ j✝¹ : Fin (p.length + 1)
i : ℕ
hi : i < p.length + 1
j✝ j : ℕ
_hij : i ≤ j
hj : j + 1 < p.length + 1
ih : p.toFun ⟨i, hi⟩ + ↑j ≤ p.toFun ⟨j, ⋯⟩ + ↑i
⊢ p.toFun ⟨i, hi⟩ + ↑(j + 1) ≤ p.toFun ⟨j + 1, hj⟩ + ↑i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ Fintype.card α < Fintype.card (Fin (s.length + 1))

Tactic:
by rw [Fintype.card_fin]; lia

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

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 0 • x = 0
ihy : 0 • y = 0
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 0 • x = 0
ihy : 0 • y = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
r s : R''
x : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 0 = 0 + 0

Tactic:
add_zero

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ -0 + 0 = 0

Tactic:
add_zero

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ -0 = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ x y : M ⊗[R] N
hx : -x + x = 0
hy : -y + y = 0
⊢ 0 = 0