mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.ofFn fun a ↦ (of A (fι a)) (fA a)).prod =
    (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)

Tactic:
List.ofFn_eq_map,

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ (List.map (fun a ↦ (of A (fι a)) (fA a)) (List.finRange n)).prod =
    (of A ((List.finRange n).dProdIndex fι)) ((List.finRange n).dProd fι fA)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
Q : QuadraticMap R M N
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : SMul S M
inst✝² : IsScalarTower S R M
inst✝¹ : Module S N
inst✝ : IsScalarTower S R N
a : S
x : M
⊢ Q (a • x) = (a * a) • Q x

Tactic:
by
  rw [← IsScalarTower.algebraMap_smul R a x, Q.map_smul, ← map_mul, algebraMap_smul]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
a : R
x y : M
⊢ polar (⇑Q) (a • y) x = a • polar (⇑Q) y x

Tactic:
polar_smul_left

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
a : R
x y : M
⊢ a • polar (⇑Q) y x = a • polar (⇑Q) y x
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ Finset.map (Sym2.mkEmbedding a) (Finset.cons a s ha),
            if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))

Tactic:
Finset.sum_map,

Goal state after:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_8
inst✝ : DecidableEq ι
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 (⇑Q) (Sym2.map f ij)
⊢ Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0) + polar (⇑Q) (f a) (∑ i ∈ s, f i))) =
    Q (f a) +
      (∑ i ∈ s, Q (f i) +
        ((∑ x ∈ Finset.cons a s ha,
            if ¬((Sym2.mkEmbedding a) x).IsDiag then polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) x)) else 0) +
          ∑ a ∈ s.sym2, if ¬a.IsDiag then polarSym2 (⇑Q) (Sym2.map f a) else 0))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i)) =
    ∑ ij ∈ Finset.map (Sym2.mkEmbedding a) (Finset.cons a s ha), polarSym2 (⇑Q) (Sym2.map f ij) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))

Tactic:
Finset.sum_map,

Goal state after:
case cons
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
ι : Type u_8
Q : QuadraticMap R M N
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
⊢ Q (f a) + (∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i) + polar (⇑Q) (f a) (∑ i ∈ s, f i)) =
    ∑ x ∈ Finset.cons a s ha, polarSym2 (⇑Q) (Sym2.map f ((Sym2.mkEmbedding a) x)) +
        ∑ ij ∈ s.sym2, polarSym2 (⇑Q) (Sym2.map f ij) -
      (Q (f a) + ∑ i ∈ s, Q (f i))
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
h : ∀ (x : M), Q x = 0
⊢ associated' 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
hB₁ : associated' Q ≠ 0
h : ∀ (x : M), Q x = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
⊢ (B x) x + (B y) x + ((B y) y + (B x) y) = (B y) y + (B x) x ↔ (B x) y = 0

Tactic:
add_add_add_comm _ _ (B y y),

Goal state after:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
⊢ (B x) x + (B y) y + ((B y) x + (B x) y) = (B y) y + (B x) x ↔ (B x) y = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) ((algebraMap R (CliffordAlgebra Q)) r) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩

Tactic:
rw [AlgHom.commutes, DirectSum.algebraMap_apply]

Goal state after:
case mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x' x : CliffordAlgebra Q
i : ℕ
r : R
⊢ (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) 0) (DirectSum.GAlgebra.toFun r) =
    (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) ↑0) ⟨(algebraMap R (CliffordAlgebra Q)) r, ⋯⟩
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case e_fst.ι_mul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m✝ : M
m : CliffordAlgebra Q
x : M
hx : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m).1 = m
⊢ ((ι Q) x * (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m).1, (f x) (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m)).1 = (ι Q) x * m

Tactic:
hx

Goal state after:
case e_fst.ι_mul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
n : N
m✝ : M
m : CliffordAlgebra Q
x : M
hx : (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m).1 = m
⊢ ((ι Q) x * m, (f x) (((foldr Q (foldr'Aux Q f) ⋯) (1, n)) m)).1 = (ι Q) x * m
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ ((lift Q) ⟨GradedAlgebra.ι Q, ⋯⟩) 0 = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨0, ⋯⟩

Tactic:
map_zero

Goal state after:
case zero
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
i' : ZMod 2
x' : CliffordAlgebra Q
⊢ 0 = (DirectSum.of (fun i ↦ ↥(evenOdd Q i)) i') ⟨0, ⋯⟩
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ Nat.card ↑(powersetCard α n) = (Nat.card α).choose n

Tactic:
cases fintypeOrInfinite α

Goal state after:
case inl
α : Type u_1
n : ℕ
val✝ : Fintype α
⊢ Nat.card ↑(powersetCard α n) = (Nat.card α).choose n

case inr
α : Type u_1
n : ℕ
val✝ : Infinite α
⊢ Nat.card ↑(powersetCard α n) = (Nat.card α).choose n
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
⊢ Nontrivial ↑(powersetCard α n)

Tactic:
cases fintypeOrInfinite α

Goal state after:
case inl
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Fintype α
⊢ Nontrivial ↑(powersetCard α n)

case inr
α : Type u_1
n : ℕ
h1 : 0 < n
h2 : ↑n < ENat.card α
val✝ : Infinite α
⊢ Nontrivial ↑(powersetCard α n)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
⊢ g 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ (ι R) x = (ι R) 0

Tactic:
map_zero

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ (ι R) x = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case refine_2
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ 0 = (algebraMap R (ExteriorAlgebra R M)) 0

Tactic:
map_zero

Goal state after:
case refine_2
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
h : (algebraMap R (ExteriorAlgebra R M)) r ∈ 1
⊢ (algebraMap R (ExteriorAlgebra R M)) 0 = 0

Tactic:
map_zero

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
hx : x = 0 ∧ r = 0
h : (algebraMap R (ExteriorAlgebra R M)) r ∈ 1
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case pos
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f x = f y
h : x < y
hx : x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
hx

Goal state after:
case pos
R✝ : Type u1
inst✝⁵ : CommRing R✝
M✝ : Type u2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R✝ M✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
x y : Fin (n + 1)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case ι_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : CliffordAlgebra 0
m✝ : M
hx : (liftAlternating (ιMulti R)) x✝ = x✝
⊢ (ι R) m✝ * (liftAlternating (ιMulti R)) x✝ = (CliffordAlgebra.ι 0) m✝ * x✝

Tactic:
hx

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ Mono F'.m

pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯))

Tactic:
· infer_instance

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯))
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ Mono F'.m

pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((RingHom.id R) c •
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))

Tactic:
· infer_instance

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((RingHom.id R) c •
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
⊢ HasInjectiveDimensionLT X 0

Tactic:
let := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi Y e
  rw [← e.comp_mk₀_id, hX.eq_zero_of_tgt (𝟙 X), Ext.mk₀_zero, Ext.comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map (Λ.chainComplexXIso X n).hom ≫
      Λ.π.app (kernel (ι.map ((Λ.chainComplex X).d (n + 1) n))) ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))

Tactic:
rw [← this, ← Functor.map_comp]

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))
⊢ ι.map ((Λ.chainComplex X).d (n + 2) (n + 1)) =
    ι.map
      ((Λ.chainComplexXIso X n).hom ≫
        ι.preimage
          (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
            kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)) = ⋀[R]^n M

Tactic:
by
  apply le_antisymm
  · rw [Submodule.span_le, Set.range_subset_iff]
    intro
    rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]
    exact Submodule.coe_mem _
  · rw [← ιMulti_span_fixedDegree_of_span_eq_top R n M hv, Submodule.span_le]
    rintro - ⟨f, ⟨f_range, rfl⟩⟩
    rw [Set.mem_ofPred] at f_range
    obtain ⟨α, rfl⟩ := Set.range_subset_range_iff_exists_comp.mp f_range
    exact ιMulti_family_span_fixedDegree_aux R v α

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings

Goal state before:
pp: C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
⊢ (ConcreteCategory.hom (R'.map f)) ((ConcreteCategory.hom (α.app X)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x

Tactic:
have eq := RingHom.congr_fun (congrArg RingCat.Hom.hom <| α.naturality f) r

Goal state after:
C : Type u'
inst✝ : Category.{v', u'} C
R R' : Cᵒᵖ ⥤ RingCat
M' : PresheafOfModules R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
x : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X))
eq : (RingCat.Hom.hom (R.map f ≫ α.app Y)) r = (RingCat.Hom.hom (α.app X ≫ R'.map f)) r
⊢ (ConcreteCategory.hom (R'.map f)) ((ConcreteCategory.hom (α.app X)) r) • (ConcreteCategory.hom (M'.map f)) x =
    (RingHom.id ↑(R.obj X)) r • (ConcreteCategory.hom (M'.map f)) x
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
⊢ snd A I ≫ t.to (A ⊗ I) = 𝟙 (A ⊗ I)

Tactic:
have : snd A I = uncurry (t.to _) := by
      rw [← curry_eq_iff]
      apply t.hom_ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ snd A I ≫ t.to (A ⊗ I) = 𝟙 (A ⊗ I)
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
c₁ c₂ : C
⊢ IsConnected (StructuredArrow (c₁, c₂) (Functor.diag C))

Tactic:
have : _root_.Nonempty <| StructuredArrow (c₁, c₂) (diag C) :=
      ⟨.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂))⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
c₁ c₂ : C
this : Nonempty (StructuredArrow (c₁, c₂) (Functor.diag C))
⊢ IsConnected (StructuredArrow (c₁, c₂) (Functor.diag C))
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
X : C₀
f : StructuredArrow X (fromFinalModel C₀) := Classical.arbitrary (StructuredArrow X (fromFinalModel C₀))
⊢ ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)

Tactic:
exact ⟨_, ObjectProperty.strictMap_obj _ _ (X := f.right) (by tauto), ⟨f.hom⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j ≫ 𝟙 s.pt
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
simp only [Category.comp_id] at n

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
r₁ r₂ : ↑(R.obj U)
m : ↑(M.obj U)
⊢ ((ιR cR) r₁ + (ιR cR) r₂) • ιM m = (ιR cR) r₁ • ιM m + (ιR cR) r₂ • ιM m

Tactic:
simp only [smul_eq, ← map_add, add_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : ∀ (X : D), (F.op ⋙ yoneda.obj X).IsRepresentable
⊢ F.IsLeftAdjoint

Tactic:
exact (Adjunction.adjunctionOfEquivRight
    (fun X Y ↦ (F.op ⋙ yoneda.obj Y).representableBy.homEquiv.symm)
    (fun X Y Y' g f ↦ (RepresentableBy.comp_homEquiv_symm ..).symm)).isLeftAdjoint

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
S : Set (Subfunctor F)
U✝ V✝ : C
f : U✝ ⟶ V✝
x : F.obj U✝
hx : x ∈ sInf ((fun T ↦ T.obj U✝) '' S)
⊢ x ∈ ⇑(hom (F.map f)) ⁻¹' sInf ((fun T ↦ T.obj V✝) '' S)

Tactic:
rintro _ ⟨F, h, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G G' : Subfunctor F✝
S : Set (Subfunctor F✝)
U✝ V✝ : C
f : U✝ ⟶ V✝
x : F✝.obj U✝
hx : x ∈ sInf ((fun T ↦ T.obj U✝) '' S)
F : Subfunctor F✝
h : F ∈ S
⊢ (hom (F✝.map f)) x ∈ (fun T ↦ T.obj V✝) F