mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e))

Tactic:
by
  ext
  simp [Basis.toMatrix_apply]

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ↑↑x ^ orderOf x - 1 = 0

Tactic:
norm_cast

Goal state after:
case calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ ↑↑(x ^ orderOf x) - 1 = 0
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
k : ℕ
ζ : Mˣ
⊢ ζ ^ k = 1 ↔ ↑ζ ^ k = 1

Tactic:
norm_cast

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

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : CommMonoid M✝
inst✝² : CommMonoid N
inst✝¹ : DivisionCommMonoid G
k l : ℕ
M : Type u_7
inst✝ : CommMonoid M
n : ℕ
ζ : ↥(rootsOfUnity n Mˣ)
⊢ (fun ζ ↦ ⟨toUnits ↑ζ, ⋯⟩) ((fun ζ ↦ ⟨↑↑ζ, ⋯⟩) ζ) = ζ

Tactic:
simp only [toUnits_val_apply, Subtype.coe_eta]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
hab : IsCoprime a b
i : Fin 2
⊢ ∃ g, ↑g i 0 = a ∧ ↑g i 1 = b

Tactic:
by
  obtain ⟨u, v, h⟩ := hab
  refine match i with
  | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩ <;>
  · rw [Matrix.det_fin_two_of, ← h]
    ring

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b₁ b₂ : F
⊢ ↑(transvection hij (b₁ + b₂)) = ↑(transvection hij b₁ * transvection hij b₂)

Tactic:
by simp [transvection_coe, mul_add, add_mul,
    single_mul_single_of_ne _ _ _ _ hij.symm, single_add, add_assoc]

Goal state after:
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
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A) One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)

Tactic:
intro i

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
⊢ ∀ (y : A i), ((mulHom A) One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
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
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), ((mulHom A).flip One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)

Tactic:
intro i

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
⊢ ∀ (y : A i), ((mulHom A).flip One.one) ((of A i) y) = (AddMonoidHom.id (⨁ (i : ι), A i)) ((of A i) y)
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: S : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Monoid S
inst✝ : DistribMulAction S N
f : M → N
s : S
x y : M
⊢ polar (s • f) x y = s • polar f x y

Tactic:
simp only [polar, Pi.smul_apply, smul_sub]

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ {i : ι} → A i →+ R

Tactic:
intro i

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i : ι
⊢ A i →+ R
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ ∀ {i j : ι} (ai : A i) (aj : A j),
    ((↑F).comp (of A (i + j))) (GradedMonoid.GMul.mul ai aj) = ((↑F).comp (of A i)) ai * ((↑F).comp (of A j)) aj

Tactic:
intro i

Goal state after:
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i : ι
⊢ ∀ {j : ι} (ai : A i) (aj : A j),
    ((↑F).comp (of A (i + j))) (GradedMonoid.GMul.mul ai aj) = ((↑F).comp (of A i)) ai * ((↑F).comp (of A j)) aj
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
⊢ ↑(((of (fun i ↦ ↥(𝒜 i)) 0) a * (decompose 𝒜) b) j) = ↑a * ↑(((decompose 𝒜) b) j)

Tactic:
coe_of_mul_apply_of_mem_zero

Goal state after:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
⊢ ↑a * ↑(((decompose 𝒜) b) j) = ↑a * ↑(((decompose 𝒜) b) j)
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
inst✝⁵ : SetLike σ R
inst✝⁴ : AddSubmonoidClass σ R
A : ι → σ
inst✝³ : AddCommMonoid ι
inst✝² : PartialOrder ι
inst✝¹ : CanonicallyOrderedAdd ι
inst✝ : SetLike.GradedMonoid A
i : ι
r : ↥(A i)
r' : ⨁ (i : ι), ↥(A i)
n : ι
h : ¬i ≤ n
⊢ ↑(((of (fun i ↦ ↥(A i)) i) r * r') n) = 0

Tactic:
rw [coe_mul_apply_eq_dfinsuppSum]
    apply (DFinsupp.sum_single_index _).trans
    swap
    · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
      exact DFinsupp.sum_zero
    · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
      exact fun x _ H => h ((self_le_add_right i x).trans_eq H)

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

Goal state before:
pp: ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
j : ι
hj : j ∈ univ
⊢ ∀ b ∈ univ, b ≠ j → (((associatedHom R) Q) (w b • v b)) (w j • v j) = 0

Tactic:
intro i

Goal state after:
ι : Type u_8
inst✝⁴ : Fintype ι
R : Type u_9
M : Type u_10
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
w : ι → R
j : ι
hj : j ∈ univ
i : ι
⊢ i ∈ univ → i ≠ j → (((associatedHom R) Q) (w i • v i)) (w j • v j) = 0
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
⊢ #{a} ≤ n

Tactic:
rw [Finset.card_singleton]; exact h

Goal state after:
Module: Mathlib.Order.Hom.PowersetCard

Goal state before:
pp: n : ℕ
I : Type u_1
inst✝ : LinearOrder I
f : Fin n ↪o I
⊢ (fun s ↦ (↑s).orderEmbOfFin ⋯) ((fun f ↦ ofFinEmb n I f.toEmbedding) f) = f

Tactic:
by symm; apply Finset.orderEmbOfFin_unique'; simp

Goal state after:
Module: Mathlib.Data.Set.PowersetCard

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

Tactic:
by
  have : Finite α := Nat.finite_of_card_ne_zero (ne_zero_of_lt h2)
  apply nontrivial h1
  simp [ENat.card_eq_coe_natCard α, h2]

Goal state after:
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
⊢ ExteriorAlgebra R M →ₗ[R] M

Tactic:
by
  letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
  haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
  exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M : ModuleCat R
n : ℕ
N : ModuleCat R
φ : M.AlternatingMap N n
x : Fin n → ↑M
⊢ (ConcreteCategory.hom (desc φ)) (mk x) = φ x

Tactic:
apply exteriorPower.alternatingMapLinearEquiv_apply_ιMulti

Goal state after:
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
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝ : IsCentralScalar R M
this : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv

Tactic:
have : IsCentralScalar R N := ⟨fun r m => rfl⟩

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this✝² : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this✝¹ : IsCentralScalar R M
this✝ : Module Rᵐᵒᵖ N := Module.compHom N ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R N
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
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
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
intro i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
⊢ 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
intro i

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasInjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
⊢ m ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
intro i

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
this : HasExt C := HasExt.standard C
i : ℕ
⊢ 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0

Tactic:
intro i

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasInjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
⊢ n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y X i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₂ i), e = 0

Tactic:
intro i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
⊢ n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₂ i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₃ i), e = 0

Tactic:
intro i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasInjectiveDimensionLT S.X₂ n
h₃ : HasInjectiveDimensionLT S.X₁ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
⊢ n ≤ i → ∀ ⦃Y : C⦄ (e : Ext Y S.X₃ i), e = 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i
⊢ ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i

Tactic:
intro i

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
h : Retract X Y
n : WithBot ℕ∞
hn : ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT Y i
i : ℕ
⊢ n < ↑i → HasInjectiveDimensionLT X i
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
⊢ Submodule.map (map n f) ⊤ = ⊤

Tactic:
← ιMulti_span,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
⊢ Submodule.map (map n f) (Submodule.span R (range ⇑(ιMulti R n))) = ⊤
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
⊢ Submodule.map (map n f) (Submodule.span R (range ⇑(ιMulti R n))) = ⊤

Tactic:
← ιMulti_span,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
⊢ Submodule.map (map n f) (Submodule.span R (range ⇑(ιMulti R n))) = Submodule.span R (range ⇑(ιMulti R n))
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case h
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
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ : Equiv.Perm.sign σ • (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
⊢ ↑↑(Equiv.Perm.sign σ) * ↑↑(Equiv.Perm.sign σ) = 1

Tactic:
norm_cast

Goal state after:
case h
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
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ : Equiv.Perm.sign σ • (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ span R (range (ExteriorAlgebra.ιMulti_family R n v))
⊢ ↑↑(Equiv.Perm.sign σ * Equiv.Perm.sign σ) = 1
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
⊢ (Functor.diag D).Final

Tactic:
have sq : (e.inverse ⋙ diag D ⋙ this.functor ≅ diag C) :=
        NatIso.ofComponents (fun c ↦ by dsimp [this]
                                        exact Iso.prod (e.counitIso.app c) (e.counitIso.app c))

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsSifted C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
e : D ≌ C
this : D × D ≌ C × C := e.prod e
sq : e.inverse ⋙ Functor.diag D ⋙ this.functor ≅ Functor.diag C
⊢ (Functor.diag D).Final
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
X Y : C ⥤ Type u
inst✝ : IsSifted C
⊢ IsIso (CartesianMonoidalCategory.prodComparison colim X Y)

Tactic:
by
  rw [← factorization_prodComparison_colim]
  infer_instance

Goal state after:
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'
N : ModuleCat ↑cR.pt
φ' : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
⊢ (homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ φ') = f ≫ (homEquiv hcR hcM') φ'

Tactic:
ext U m

Goal state after:
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'
N : ModuleCat ↑cR.pt
φ' : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
U : Cᵒᵖ
m : ↑(M.obj U)
⊢ (ModuleCat.Hom.hom (((homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ φ')).app U)) m =
    (ModuleCat.Hom.hom ((f ≫ (homEquiv hcR hcM') φ').app U)) m
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ pullbackArrows g R ≤ (Sieve.pullback g S).arrows

Tactic:
← Sieve.generate_le_iff,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
K : Pretopology C
X Y : C
S : Sieve X
g : Y ⟶ X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ Sieve.generate (pullbackArrows g R) ≤ Sieve.pullback g S
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
i : IsIso g
⊢ IsIso (pullback.snd g f)

Tactic:
refine ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨?_, by simp⟩⟩⟩
      ext
      · rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
        simp
      · simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2.mp.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Presieve.singleton (f ≫ g) (f ≫ g)

Tactic:
apply singleton.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_2.mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y✝ : C
f : Y✝ ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
Y : C
⊢ Presieve.singleton f f

Tactic:
apply singleton.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
i : ι
⊢ (ofArrows (fun j ↦ W (g i) ⋯ j) fun j ↦ p (g i) ⋯ j) ∈ J.coverings (Z i)

Tactic:
rw [← hp]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : sorry.HasPullbacks
inst✝³ : Limits.HasPullbacks C
J : Precoverage C
inst✝² : J.HasIsos
inst✝¹ : J.IsStableUnderBaseChange
inst✝ : J.IsStableUnderComposition
X : C
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Presieve Y
hR : ofArrows Z g ∈ J.coverings X
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : ofArrows Z g f), Ti f H ∈ J.coverings Y
κ : ⦃Y : C⦄ → (f : Y ⟶ X) → ofArrows Z g f → Type (max u v)
W : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → κ f hf → C
p : ⦃Y : C⦄ → (f : Y ⟶ X) → (hf : ofArrows Z g f) → (i : κ f hf) → W f hf i ⟶ Y
hp : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (hf : ofArrows Z g f), Ti f hf = ofArrows (W f hf) (p f hf)
this : (ofArrows Z g).bind Ti = ofArrows (fun ij ↦ W (g ij.fst) ⋯ ij.snd) fun ij ↦ p (g ij.fst) ⋯ ij.snd ≫ g ij.fst
i : ι
⊢ Ti (g i) ⋯ ∈ J.coverings (Z i)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
⊢ singleton f f

Tactic:
apply singleton.mk

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case h.right
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
W : C
x : FamilyOfElements (yoneda.obj W) S.arrows
hx : x.Compatible
H : IsColimit S.arrows.cocone
s : Cocone S.arrows.diagram := ⋯
⊢ ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = H.desc s

Tactic:
exact fun g hg => H.uniq s g (fun ⟨⟨f, _, hom⟩, hf⟩ => hg hom hf)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ ∀ (i : ι), singleton (f default) (f i)

Tactic:
intro i

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
ι : Type u_1
inst✝ : Unique ι
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
⊢ singleton (f default) (f i)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
⊢ ∀ (i : ι), pushforward f (ofArrows U g) (g i ≫ f)

Tactic:
intro i

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
U : ι → C
X Y : C
g : (i : ι) → U i ⟶ X
f : X ⟶ Y
i : ι
⊢ pushforward f (ofArrows U g) (g i ≫ f)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W : C
a : W ⟶ X'
⊢ (ofArrows Z fun i ↦ f i ≫ e.inv).arrows a → (pullback e.hom (ofArrows Z f)).arrows a

Tactic:
rintro ⟨_, a, _, ⟨i⟩, rfl⟩

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
X : C
Z : I → C
f : (i : I) → Z i ⟶ X
X' : C
e : X' ≅ X
W Y : C
i : I
a : W ⟶ Z i
⊢ (pullback e.hom (ofArrows Z f)).arrows (a ≫ f i ≫ e.inv)