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

Goal state after:
α : 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 ∈ l → r a b) → orderedInsert r a (insertionSort r l) = a :: insertionSort r l
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 (map { toFun := op, inj' := ⋯ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0)
a b : G
aA : a ∈ A
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul (map { toFun := op, inj' := ⋯ } B) (map { toFun := op, inj' := ⋯ } A) (op b0) (op a0)
a b : G
aA : a ∈ A
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
hs : 1 ∈ s
⊢ 1 ∈ s ^ n
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ #s - 1 < #s
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (s.sort fun a b ↦ a ≤ b).length - 1 < (s.sort fun a b ↦ a ≤ b).length

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ #s - 1 < #s
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ (n + 1)).Nonempty
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
x : M
⊢ f x = (b.repr (f (b i))) i • x

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
x : M
⊢ f x = (b.repr (f (b i))) i • x
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
H : ∀ (x : M), f x = (b.repr (f (b i))) i • x
r : R
⊢ r * (b.coord i) (f (b i)) = (b.coord i) (f (b i)) * r

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
H : ∀ (x : M), f x = (b.repr (f (b i))) i • x
r : R
⊢ r * (b.repr (f (b i))) i = (b.repr (f (b i))) i * r
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker

Tactic:
classical
    by_cases his : i ∈ s
    · by_cases hit : i ∈ t
      · exact (hs.le_bot ⟨his, hit⟩).elim
      exact inf_le_of_right_le (iInf_le_of_le i <| iInf_le _ hit)
    exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ (n + 2)).Nontrivial

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
hs : s.Nontrivial
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (s ^ n * s * s).Nontrivial
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
n : ℕ
hn : n ≠ 0
⊢ #s ≤ #(s ^ n)

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
n : ℕ
hn : n ≠ 0
⊢ #s ≤ #(s ^ n)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : (fun x ↦ s • x) { toFinsupp := f } = (fun x ↦ s • x) { toFinsupp := g }
⊢ (fun x ↦ s • x) f = (fun x ↦ s • x) g

Tactic:
simpa using

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : (fun x ↦ s • x) { toFinsupp := f } = (fun x ↦ s • x) { toFinsupp := g }
⊢ s • f = s • g
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
he : X = C a
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
he : X = C a
⊢ False
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set σ
f : σ → R
⊢ f '' s • ⊤ = ((lsum R) fun i ↦ f ↑i • LinearMap.id).range

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set σ
f : σ → R
⊢ f '' s • ⊤ = ((lsum R) fun i ↦ f ↑i • LinearMap.id).range
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ s • ⊤ = ((lsum R) fun i ↦ ↑i • LinearMap.id).range

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ s • ⊤ = ((lsum R) fun i ↦ ↑i • LinearMap.id).range
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ Subsingleton R[X] ↔ Subsingleton R
Module: Mathlib.Algebra.Polynomial.Basic

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

Tactic:
simpa using

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
c : R
⊢ (C c * X ^ n).support ⊆ {n}

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
⊢ ((monomial n) c).support ⊆ {n}
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case pos
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 D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
h21 : c2 ≠ 1 ∨ d1 ≠ 1
c4 d4 : G
hu : d4⁻¹ * 1 * (1 * c4⁻¹) = d1⁻¹ * 1 * (1 * c2⁻¹) → d4⁻¹ * 1 = d1⁻¹ * 1 ∧ 1 * c4⁻¹ = 1 * c2⁻¹
hc4 : c4 ∈ C
hd4 : d4 ∈ D
he : c4 * d4 = c2 * d1
⊢ c4 = c2 ∧ d4 = d1

Tactic:
simpa using

Goal state after:
case pos
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 D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
h21 : c2 ≠ 1 ∨ d1 ≠ 1
c4 d4 : G
hu : d4⁻¹ * 1 * (1 * c4⁻¹) = d1⁻¹ * 1 * (1 * c2⁻¹) → d4⁻¹ * 1 = d1⁻¹ * 1 ∧ 1 * c4⁻¹ = 1 * c2⁻¹
hc4 : c4 ∈ C
hd4 : d4 ∈ D
he : c4 * d4 = c2 * d1
⊢ c4 = c2 ∧ d4 = d1
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n n✝ : ℕ
⊢ (p.update n 0).coeff n✝ = (erase n p).coeff n✝

Tactic:
rw [coeff_update_apply, coeff_erase]

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

Goal state before:
pp: case neg.inl
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 D : Finset G
hC✝ : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
hc1✝ : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hC : 1 < #C
c : G
hc : c ∈ C
hc1 : c ≠ 1
⊢ c = 1

Tactic:
simpa using

Goal state after:
case neg.inl
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 D : Finset G
hC✝ : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
hc1✝ : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hC : 1 < #C
c : G
hc : c ∈ C
hc1 : c ≠ 1
⊢ c = 1
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 : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hq : ⟨f ↑⟨x, hx⟩, ⋯⟩ ∈ q
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Tactic:
simpa using

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hq : ⟨f ↑⟨x, hx⟩, ⋯⟩ ∈ q
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ f x ∈ p
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case neg.inr
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 D : Finset G
hC : 1 ∈ C
hD✝ : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1✝ : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hD : 1 < #D
d : G
hd : d ∈ D
hd1 : d ≠ 1
⊢ d = 1

Tactic:
simpa using

Goal state after:
case neg.inr
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 D : Finset G
hC : 1 ∈ C
hD✝ : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hc2 : 1 ∈ C
hd1✝ : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = 1⁻¹ * 1 * (1 * 1⁻¹) → a = 1⁻¹ * 1 ∧ b = 1 * 1⁻¹
hD : 1 < #D
d : G
hd : d ∈ D
hd1 : d ≠ 1
⊢ d = 1
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : Surjective ⇑g
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (map g ⊤).FG

Tactic:
rw [← LinearMap.range_eq_top] at h_surj

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup P
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact ⇑f ⇑g
h_surj : g.range = ⊤
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R P
⊢ (map g ⊤).FG
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 0 = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 0 = 1
Module: Mathlib.Algebra.Order.SuccPred.WithBot

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 1 = 2

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 1 = 2
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_1
f : ι → ℕ∞
⊢ ⨅ i, f i = 0 ↔ ∃ i, f i = 0

Tactic:
simpa using

Goal state after:
ι : Sort u_1
f : ι → ℕ∞
⊢ ⨅ i, f i = 0 ↔ ∃ i, f i = 0
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: 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
⊢ τ₃ (g x₂) = τ₃ 1

Tactic:
simpa using

Goal state after:
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
⊢ τ₃ (g x₂) = 1
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case fst
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
x : ↥p
⊢ ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) ((ofIsComplProd h).toFun φ)).1 x = φ.1 x

pp: case snd
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
x : ↥q
⊢ ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) ((ofIsComplProd h).toFun φ)).2 x = φ.2 x

Tactic:
· exact ofIsCompl_apply_left h x

Goal state after:
case snd
R : Type u_1
inst✝¹² : Ring R
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module R E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R F
G : Type u_4
inst✝⁷ : AddCommGroup G
inst✝⁶ : Module R G
p✝ q✝ : Submodule R E
S : Type u_5
inst✝⁵ : Semiring S
M : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : Module S M
m : Submodule S M
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
x : ↥q
⊢ ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) ((ofIsComplProd h).toFun φ)).2 x = φ.2 x
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: 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₂
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂

Tactic:
simpa using

Goal state after:
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₂
x₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: 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₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂

Tactic:
simpa using

Goal state after:
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₁ : M₁
hy₁ : f' (τ₁ x₁) = τ₂ x₂
⊢ τ₂ (f x₁) = τ₂ x₂
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
f : ι → ℕ∞
c : R
⊢ c • ⨆ i, f i = ⨆ i, c • f i

Tactic:
simpa using

Goal state after:
ι : Sort u_2
R : Type u_4
inst✝¹ : SMul R ℕ∞
inst✝ : IsScalarTower R ℕ∞ ℕ∞
f : ι → ℕ∞
c : R
⊢ c • ⨆ i, f i = ⨆ i, c • f i
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: 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
x✝ : M
⊢ f x✝ = 0 x✝

Tactic:
simpa using

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
x✝ : M
⊢ f x✝ = 0
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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : M × P
e : f x.1 + ↑l x.2 = f y.1 + ↑l y.2
⊢ x.2 = y.2

Tactic:
simpa using

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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
x y : M × P
e : f x.1 + ↑l x.2 = f y.1 + ↑l y.2
⊢ x.2 = y.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
E : Type u_7
inst✝¹ : AddCommGroup E
inst✝ : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
x : E
hx : x ∈ (id - p).ker
⊢ p x = x

Tactic:
simpa using

Goal state after:
S : Type u_5
inst✝² : Semiring S
E : Type u_7
inst✝¹ : AddCommGroup E
inst✝ : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
x : E
hx : x ∈ (id - p).ker
⊢ p x = x
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
R : SetRel α α
inst✝ : R.IsRefl
⊢ SetRel.id ⊆ R

Tactic:
rintro ⟨_, _⟩ rfl

Goal state after:
α : Type u_1
R : SetRel α α
inst✝ : R.IsRefl
fst✝ : α
⊢ (fst✝, fst✝) ∈ R
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
S : SetRel β β
R : SetRel α β
inst✝ : S.IsRefl
⊢ R ⊆ R ○ S

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
S : SetRel β β
R : SetRel α β
inst✝ : S.IsRefl
⊢ R ⊆ R ○ S
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α α
inst✝ : R.IsRefl
S : SetRel α β
⊢ S ⊆ R ○ S

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
R : SetRel α α
inst✝ : R.IsRefl
S : SetRel α β
⊢ S ⊆ R ○ S
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length
⊢ i < x.length

Tactic:
simpa using

Goal state after:
α : Type u_1
r : SetRel α α
x : RelSeries r
i : ℕ
h : i < x.length
⊢ i < x.length
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
inst✝ : R.IsSymm
⊢ (R ○ R).IsSymm

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
R✝ R₁✝ R₂✝ : SetRel α β
S✝ : SetRel β γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
a✝ a₁ a₂ : α
b✝ : β
c✝ : γ
R R₁ R₂ : SetRel α α
S : SetRel β β
a b c : α
inst✝ : R.IsSymm
⊢ (R ○ R).IsSymm