mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
inst✝⁵ : DecidableEq ι
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : (i : ι) → Zero (β₁ i)
inst✝³ : (i : ι) → Zero (β₂ i)
inst✝² : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
h : (i : ι) → β₂ i → γ
h0 : ∀ (i : ι), h i 0 = 1
⊢ (mapRange f hf g).prod h = g.prod fun i b ↦ h i (f i b)

Tactic:
rw [mapRange_def]
  refine (Finset.prod_subset support_mk_subset ?_).trans ?_
  · intro i h1 h2
    simp only [mem_support_toFun, ne_eq] at h1
    simp only [Finset.coe_sort_coe, mem_support_toFun, mk_apply, ne_eq, h1, not_false_iff,
      dite_eq_ite, ite_true, not_not] at h2
    simp [h2, h0]
  · refine Finset.prod_congr rfl ?_
    intro i h1
    simp only [mem_support_toFun, ne_eq] at h1
    simp [h1]

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
⊢ comapDomain' ⇑h.symm ⋯ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f) = f

Tactic:
ext k

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst✝ : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β (h.symm k)
k : κ
⊢ (comapDomain' ⇑h.symm ⋯ ((fun f ↦ mapRange (fun i ↦ ⇑(Equiv.cast ⋯)) ⋯ (comapDomain' ⇑h ⋯ f)) f)) k = f k
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) ↔ ∀ w ∈ Set.range ⇑f, x✝ w = 0

Tactic:
Set.forall_mem_range,

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) ↔ ∀ (i : M₁), x✝ (f i) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case refine_1
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
x✝ : x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f)
i : ι
hi : i ∈ Set.univ
y : Π₀ (i : ι), β₁ i
hy : (mapRange.addMonoidHom f) y = x
⊢ x i ∈ (fun i ↦ ((fun i ↦ AddMonoidHom.mrange (f i)) i).carrier) i

Tactic:
simp [← hy]

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

Goal state before:
pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
η : Type u_6
s : η → Set ι
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ (i : η), LinearIndepOn R v (s i)
hη : ¬Nonempty η
⊢ LinearIndepOn R v (⋃ i, s i)

Tactic:
refine (linearIndepOn_empty R v).mono (t := iUnion (s ·)) ?_
    rintro _ ⟨_, ⟨i, _⟩, _⟩
    exact hη ⟨i⟩

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝⁴ : Semiring R
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝³ : (i : ι) → AddCommMonoid (β₁ i)
inst✝² : (i : ι) → AddCommMonoid (β₂ i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (r • g) = r • mapRange f hf g

Tactic:
by
  ext
  simp only [mapRange_apply f, coe_smul, Pi.smul_apply, hf']

Goal state after:
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
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ ∃ f_1, (f_1.sum fun x xi ↦ ↑xi) = f.sum fun _i xi ↦ xi

Tactic:
refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
⊢ (DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩).support = f.support

case refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
f : ι →₀ N
hf : ∀ (i : ι), f i ∈ p i
i : ι
hi : i ∈ f.support
⊢ (fun x xi ↦ ↑xi) i ((DFinsupp.mk f.support fun i ↦ ⟨f ↑i, ⋯⟩) i) = (fun _i xi ↦ xi) i (f i)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl.inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑s
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝)
⊢ Sum.inl val✝¹ = Sum.inl val✝

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

Goal state after:
case inl.inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑s
eq : ↑val✝¹ = ↑val✝
⊢ Sum.inl val✝¹ = Sum.inl val✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl.inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ : ↑s
val✝ : ↑t
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝)
⊢ Sum.inl val✝¹ = Sum.inr val✝

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

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

Goal state before:
pp: case inr.inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ : ↑t
val✝ : ↑s
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝)
⊢ Sum.inr val✝¹ = Sum.inl val✝

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

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

Goal state before:
pp: case inr.inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑t
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝)
⊢ Sum.inr val✝¹ = Sum.inr val✝

Tactic:
simp [hs.ne_zero, ht.ne_zero] at eq

Goal state after:
case inr.inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑t
eq : ↑val✝¹ = ↑val✝
⊢ Sum.inr val✝¹ = Sum.inr val✝
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval) = -(a₂.1 • a₂.2) + a₁.1 • a₁.2 + l₁.eval

Tactic:
add_assoc

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval) = -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval)
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -l₀.eval = (-l).eval

Tactic:
← hl,

Goal state after:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -l.eval = (-l).eval
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ r • l₀.eval = (r • l).eval

Tactic:
← hl,

Goal state after:
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ r • l.eval = (r • l).eval
Module: Mathlib.Algebra.Algebra.Pi

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
ι : Type u_4
A₁ : ι → Type u_5
A₂ : ι → Type u_6
A₃ : ι → Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → Semiring (A₁ i)
inst✝⁶ : (i : ι) → Semiring (A₂ i)
inst✝⁵ : (i : ι) → Semiring (A₃ i)
inst✝⁴ : (i : ι) → Algebra R (A₁ i)
inst✝³ : (i : ι) → Algebra R (A₂ i)
inst✝² : (i : ι) → Algebra R (A₃ i)
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
⊢ ∀ (x : R),
    (RingEquiv.sumArrowEquivProdArrow α β S) ((algebraMap R (α ⊕ β → S)) x) = (algebraMap R ((α → S) × (β → S))) x

Tactic:
by intro; ext <;> simp

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
η : 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
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ ⟨x₁, x₂⟩ = ⟨x₁, y₂⟩

Tactic:
refine Sigma.eq rfl ?_

Goal state after:
case pos
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
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ Eq.recOn ⋯ ⟨x₁, x₂⟩.snd = ⟨x₁, y₂⟩.snd
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: 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)
⊢ ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0

Tactic:
by
  split_ifs with h
  · simp [h]
  obtain ⟨x, hx⟩ := ne_one_iff.1 h
  refine eq_zero_of_mul_eq_self_left hx ?_
  rw [Finset.mul_sum]
  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm

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

Goal state before:
pp: case refine_2
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ LinearIndepOn K v (⋃₀ c)

pp: case refine_3
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set ι
⊢ x ∈ c → x ⊆ ⋃₀ c

Tactic:
· exact linearIndepOn_sUnion_of_directed cc.directedOn fun x xc => (hc xc).2

Goal state after:
case refine_3
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
c : Set (Set ι)
hc : c ⊆ {b | b ⊆ t ∧ LinearIndepOn K v b}
cc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
x : Set ι
⊢ x ∈ c → x ⊆ ⋃₀ c
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
af : a0 ∉ f.coeff.support
⊢ f.coeff a0 * g.coeff b0 = 0

Tactic:
notMem_support_iff.mp af,

Goal state after:
case refine_2.inl
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
hnotMem : ¬(a0 ∈ f.coeff.support ∧ b0 ∈ g.coeff.support)
x✝ : True
af : a0 ∉ f.coeff.support
⊢ 0 * g.coeff b0 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (single m r * x).coeff m₁ = r * x.coeff m₂

Tactic:
classical
  calc
    (single m r * x).coeff m₁
    _ = x.coeff.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0 := by simp [coeff_mul]
    _ = x.coeff.sum fun m' r' ↦ if m' = m₂ then r * r' else 0 := by gcongr; simp [*]
    _ = r * x.coeff m₂ := by simp +contextual [Finsupp.sum_eq_single m₂]

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
inst✝ : Subsingleton M
r : R
⊢ (uniqueRingEquiv M).symm r = single 1 r

Tactic:
by ext; simp [uniqueRingEquiv]

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 s * s) = ↑s ^ n * ↑s

Tactic:
coe_mul,

Goal state after:
case succ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec n s) * ↑s = ↑s ^ n * ↑s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

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

pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

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

Goal state after:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ Set.range f = Set.range ⇑(s.orderEmbOfFin h)

Tactic:
range_orderEmbOfFin,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
f : Fin k → α
hfs : ∀ (x : Fin k), f x ∈ s
hmono : StrictMono f
⊢ Set.range f = ↑s
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n

Tactic:
by simp_all [card_compl]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
⊢ ↑(s * t) = ↑1 ↔ ∃ a b, ↑s = ↑{a} ∧ ↑t = ↑{b} ∧ a * b = 1

Tactic:
coe_mul,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s t : Finset α
⊢ ↑s * ↑t = ↑1 ↔ ∃ a b, ↑s = ↑{a} ∧ ↑t = ↑{b} ∧ a * b = 1
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: 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
⊢ 1 < #C ∨ 1 < #D

Tactic:
simp_rw [C, D, card_map]

Goal state after:
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
⊢ 1 < #A ∨ 1 < #B
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).toFinsupp = single 1 a

Tactic:
C_mul_X_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
⊢ ((monomial 1) a).toFinsupp = single 1 a
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
C_mul_X_eq_monomial,

Goal state after:
R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ ((monomial 1) c).support = {1}
Module: Mathlib.Algebra.Polynomial.Basic

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

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

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: case pos
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j', i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j', i'⟩

Tactic:
subst hj

Goal state after:
case pos
R : Type u_2
η : Type u_4
ιs : η → Type u_5
Ms : η → Type u_6
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j, i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j, i'⟩
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case codisjoint
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
x : E
a✝ : x ∈ ⊤
⊢ x - ↑(f x) ∈ f.ker

Tactic:
rw [mem_ker, map_sub, hf, sub_self]

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

Goal state before:
pp: case top
s : Set ℕ∞
h : s.Infinite
hx : ⊤ < ⊤
⊢ ∃ a ∈ s, ⊤ < a

Tactic:
| top =>

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

Goal state before:
pp: case mp.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
hx₂ : g' (τ₂ x₂) = 1
⊢ τ₂ x₂ ∈ Set.range ⇑f'

Tactic:
obtain ⟨x₁, rfl⟩ := (h x₂).1 (h₃ (by simpa only [map_one, comm₂₃] using hx₂))

Goal state after:
case mp.mp
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₁ : M₁
hx₂ : g' (τ₂ (f x₁)) = 1
⊢ τ₂ (f x₁) ∈ Set.range ⇑f'
Module: Mathlib.Data.ENat.Lattice

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

Tactic:
| top =>

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑T → Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm

Tactic:
exact Commute.units_inv_right

Goal state after:
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
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ (q.mapQ r g hqr).ker = (p.mapQ q f hpq).range ↔ g.range ⊓ r ≤ map g q

Tactic:
← (comap_injective_of_surjective (mkQ_surjective _)).eq_iff

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
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (q.mapQ r g hqr).ker = comap q.mkQ (p.mapQ q f hpq).range ↔ g.range ⊓ r ≤ map g q
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ ⊤ + 1 ≤ height b

Tactic:
| top =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ ⊤ + 1 ≤ coheight b

Tactic:
| top =>

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case top
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ height a
hne : Nonempty { p // RelSeries.last p = a }
ha : height a = ⊤
⊢ ∃ p, RelSeries.last p = a ∧ p.length = n

Tactic:
| top =>

Goal state after:
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 h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries α
hp : RelSeries.head p = x
hl : p.length = n
⊢ (RelSeries.reverse p).last = x ∧ (RelSeries.reverse p).length = n

Tactic:
constructor <;> simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
p : LTSeries αᵒᵈ
hp : RelSeries.last p = x
hl : p.length = n
⊢ (RelSeries.reverse p).head = x ∧ (RelSeries.reverse p).length = n

Tactic:
constructor <;> simpa

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ¬krullDim α = ⊥ ↔ Nonempty α

Tactic:
krullDim_eq_bot_iff,

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ ¬IsEmpty α ↔ Nonempty α