mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
⊢ h.desc s ∘ₗ solution.π = s.π

Tactic:
aesop

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

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
⊢ solution.postcomp (h.desc s) = s

Tactic:
aesop

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

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
e : M ≃ₗ[A] N
⊢ (solution.postcomp ↑e).fromQuotient = ↑e ∘ₗ solution.fromQuotient

Tactic:
aesop

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

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
⊢ (ofQuotient relations).fromQuotient = LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
⊢ solution.postcomp (solution.fromQuotient ∘ₗ h.down.desc (ofQuotient relations)) = solution.postcomp LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
⊢ h.down.desc (ofQuotient relations) ∘ₗ solution.fromQuotient = LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : ∀ (g : ι → R), ∑ i, g i • v i = 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this✝ : Fintype κ
w : κ → R
hw : ∑ i, w i • ∑ j, A i j • v j = 0
this : w = 0
⊢ ∀ (i : κ), w i = 0

Tactic:
aesop

Goal state after:
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ ∃ d, a = d ^ n

Tactic:
by
  refine exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one ?_) h
  obtain ⟨x, y, hxy⟩ := cp
  rw [← hxy]
  exact dvd_add (dvd_mul_of_dvd_right (gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (gcd_dvd_right _ _) _)

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

Goal state before:
pp: case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Finite κ
inst✝³ : Fintype ι
inst✝² : Fintype κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
val✝ : Fintype κ
⊢ c.toMatrix ⇑c' * (toMatrix b' c') f * b'.toMatrix ⇑b = (toMatrix b c) f

Tactic:
rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nonempty n
r : Rˣ
i : n
⊢ ∃ a, det a = r

Tactic:
refine ⟨⟨diagonal fun j ↦ if j = i then r else 1, diagonal fun j ↦ if j = i then r⁻¹.1 else 1,
    ?_, ?_⟩, by simp [det]⟩
  <;> simp only [diagonal_mul_diagonal, mul_ite, ite_mul, Units.mul_inv, one_mul, mul_one,
      diagonal_eq_one]
  <;> funext j <;> split_ifs <;> simp

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

Goal state before:
pp: K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)

Tactic:
have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ

Goal state after:
K : Type u_3
V : Type u_8
inst✝⁴ : Field K
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Q : QuadraticForm K V
hQ : LinearMap.SeparatingLeft (associated Q)
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ ((associatedHom K) Q) ⇑v
hv₂ : ∀ (i : Fin (finrank K V)), (((associatedHom K) Q) (v i)) (v i) ≠ 0
⊢ ∃ w, Equivalent Q (weightedSumSquares K w)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Subsingleton n
⊢ Subsingleton (SpecialLinearGroup n R)

Tactic:
by
  refine ⟨fun ⟨A, hA⟩ ⟨B, hB⟩ ↦ ?_⟩
  ext i j
  rcases isEmpty_or_nonempty n with hn | hn; · exfalso; exact IsEmpty.false i
  rw [det_eq_elem_of_subsingleton _ i] at hA hB
  simp only [Subsingleton.elim j i, hA, hB]

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

Goal state before:
pp: n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : SpecialLinearGroup n R
hn : IsEmpty n
⊢ A ∈ center (SpecialLinearGroup n R) → ∃ r, r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑A

Tactic:
aesop

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

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
⊢ (a • 1).det = 1

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f (a + b) * f (a + b) - f a * f a - f b * f b =
    (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b)

Tactic:
rw [hf, hf, hf]

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ diagonal D = {i | i ≠ i₀}.noncommProd (fun x ↦ if h : x ≠ i₀ then ↑(diag2n ⋯ (D x) ⋯) else 1) ⋯

Tactic:
rw [Finset.noncommProd_congr (s₂ := {i | i ≠ i₀}) rfl (fun i hi ↦
      (dif_pos (Finset.mem_filter.1 hi).2 : _ = (diag2n (Finset.mem_filter.1 hi).2 _ _).1))]

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ diagonal D =
    {i | i ≠ i₀}.noncommProd
      (fun i i_1 j ↦ if i_1 = j then (fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) i_1 else 0) ⋯
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ (diagonalRingHom ι F) D = {i | i ≠ i₀}.noncommProd (fun x ↦ (diagonalRingHom ι F) (g x)) ⋯

Tactic:
rw [← Finset.map_noncommProd _ _ (fun _ _ _ _ _ ↦ Commute.all _ _), Finset.noncommProd_eq_prod]

Goal state after:
case convert_3
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : (diagonal D).det = 1
g : ι → ι → F := fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
hg_def : g = fun i k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1
⊢ (diagonalRingHom ι F) D = (diagonalRingHom ι F) ({i | i ≠ i₀}.prod g)
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : Std.Associative fun x y ↦ x * y
⊢ mulLeft₃ = mulRight₃

Tactic:
ext x y z; simp [Std.Associative.assoc]

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

Goal state before:
pp: R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹¹ : Semiring R₁
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring R₂
inst✝⁸ : Semiring S₂
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : Module S₁ N₂
inst✝⁵ : Module S₂ N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : Matrix n m N₂
i : n
j : m
this : ∑ i', ∑ j', (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ σ₂ (Pi.single j 1 x✝¹) •> σ₁ (Pi.single i 1 x✝³) •> f x✝³ x✝¹ =
    (if i = x✝³ then 1 else 0) •> (if j = x✝¹ then 1 else 0) •> f x✝³ x✝¹

Tactic:
aesop

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

Goal state before:
pp: case succ
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ !![1 * 1 + ↑n * 0, 1 * 1 + ↑n * 1; 0 * 1 + 1 * 0, 0 * 1 + 1 * 1] = !![1, ↑n + 1; 0, 1]

Tactic:
congrm !![_, ?_; _, _]

Goal state after:
case succ
n : ℕ
h : ↑(T ^ ↑n) = !![1, ↑n; 0, 1]
⊢ 1 * 1 + ↑n * 1 = ↑n + 1
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
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) (a * b)) (i + j)) = a * ↑(((decompose 𝒜) b) j)

Tactic:
by
  lift a to 𝒜 i using a_mem
  rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]

Goal state after:
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
𝒜 : ι → σ
i : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 0
⊢ ↑(((decompose 𝒜) (a * b)) i) = ↑(((decompose 𝒜) a) i) * b

Tactic:
lift b to 𝒜 0 using b_mem

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

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
⊢ ((toLinearMap₂' R) M).SeparatingLeft ↔ M.SeparatingLeft

Tactic:
refine ⟨fun h ↦ separatingLeft_def.mpr ?_, SeparatingLeft.toLinearMap₂'⟩
  exact fun v hv => h v fun w => (M.toLinearMap₂'_apply' _ _).trans <| hv w

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ ⨆ i, (ι Q).range ^ i = ⊤

Tactic:
rw [← (DirectSum.Decomposition.isInternal (evenOdd Q)).submodule_iSup_eq_top, eq_comm]
  calc
    -- Porting note: needs extra annotations, no longer unifies against the goal in the face of
    -- ambiguity
    ⨆ (i : ZMod 2) (j : { n : ℕ // ↑n = i }), LinearMap.range (ι Q) ^ (j : ℕ) =
        ⨆ i : Σ i : ZMod 2, { n : ℕ // ↑n = i }, LinearMap.range (ι Q) ^ (i.2 : ℕ) := by
      rw [iSup_sigma]
    _ = ⨆ i : ℕ, LinearMap.range (ι Q) ^ i :=
      Function.Surjective.iSup_congr (fun i => i.2) (fun i => ⟨⟨_, i, rfl⟩, rfl⟩) fun _ => rfl

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : ↑(powersetCard α n)
⊢ (↑s).ncard = n

Tactic:
rw [← coe_coe, Set.ncard_coe_finset, s.prop]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
finite : Finite ↑(powersetCard α n)
this : ⋃₀ (SetLike.coe '' powersetCard α n) = univ
⊢ ∀ t ∈ SetLike.coe '' powersetCard α n, t.Finite

Tactic:
aesop

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

Goal state before:
pp: case inl.inr
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : n = 0 ∨ Nat.card α = n
⊢ False

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
⊢ ∀ (x y : MultilinearMap R N M₂), (x + y).currySum = x.currySum + y.currySum

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
⊢ ∀ (m : R) (x : MultilinearMap R N M₂), (m • x).currySum = (RingHom.id R) m • x.currySum

Tactic:
aesop

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✝
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
h : x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 0

Tactic:
clear hxy

Goal state after:
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 : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
h : x < y
⊢ (List.ofFn fun i ↦ (ι R) (f i)).prod = 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
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : ↑i < m
⊢ (v ∘ ⇑(ofFinEmbEquiv.symm s)) (i.castLT hi) =
    v
      ↑((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
          (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (Sum.inl (i.castLT hi))))

Tactic:
aesop

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

Goal state before:
pp: case neg
R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
i : Fin (m + n)
e : Fin (m + n) ≃o ↥↑(disjUnion h) := orderIsoOfFin (disjUnion h)
hi : m ≤ ↑i
⊢ (v ∘ ⇑(ofFinEmbEquiv.symm t)) (Fin.subNat m (Fin.cast ⋯ i) hi) =
    v
      ↑((Equiv.Finset.disjUnionEquiv (↑s) (↑t) h)
          (↑((orderIsoOfFin s).sumCongr (orderIsoOfFin t)) (Sum.inr (Fin.subNat m (Fin.cast ⋯ i) hi))))

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
inst✝ : HasExt C
h : ∀ ⦃Y : C⦄, Subsingleton (Ext Y X 1)
X✝ Y✝ : C
f : X✝ ⟶ X
g : X✝ ⟶ Y✝
x✝ : Mono g
⊢ ⋯.extClass.comp (Ext.mk₀ f) ⋯ = 0

Tactic:
by subsingleton

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
N✝ : Type ?u.42
inst✝¹ : AddCommGroup N✝
inst✝ : Module R N✝
s : (relations R (Fin n) M).Solution N✝
⊢ (relationsSolutionEquiv.symm (ιMulti R n)).postcomp
      (ExteriorAlgebra.liftAlternating (update 0 n (relationsSolutionEquiv s)) ∘ₗ (⋀[R]^n M).subtype) =
    s

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : Small.{v, u} R
inst✝ : Small.{v', u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
eM : ↑M ≃ₗ[R] ↑(of R (ULift.{v', v} ↑M)) := ULift.moduleEquiv.symm
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
hasInjectiveDimensionLE_iff_of_linearEquiv_aux eM,

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : Small.{v, u} R
inst✝ : Small.{v', u} R
M : ModuleCat R
N : ModuleCat R
e : ↑M ≃ₗ[R] ↑N
n : ℕ
eM : ↑M ≃ₗ[R] ↑(of R (ULift.{v', v} ↑M)) := ULift.moduleEquiv.symm
⊢ HasInjectiveDimensionLE (of R (ULift.{v', v} ↑M)) n ↔ HasInjectiveDimensionLE N 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
⊢ map n LinearMap.id = LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
f : M →ₗ[R] N
g : N →ₗ[R] N'
⊢ map n (g ∘ₗ f) = map n g ∘ₗ map n f

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v', u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
n : ℕ
eM : ↑M ≃ₗ[R] ↑(of R (ULift.{v', v} ↑M)) := ULift.moduleEquiv.symm
eN : ↑N ≃ₗ[R'] ↑(of R' (ULift.{v, v'} ↑N)) := ULift.moduleEquiv.symm
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
hasInjectiveDimensionLE_iff_of_linearEquiv_aux eM,

Goal state after:
R : Type u
inst✝³ : Ring R
inst✝² : Small.{v, u} R
R' : Type u'
inst✝¹ : Ring R'
eR : R ≃+* R'
inst✝ : Small.{v', u'} R'
M : ModuleCat R
N : ModuleCat R'
e : ↑M ≃ₛₗ[↑eR] ↑N
n : ℕ
eM : ↑M ≃ₗ[R] ↑(of R (ULift.{v', v} ↑M)) := ULift.moduleEquiv.symm
eN : ↑N ≃ₗ[R'] ↑(of R' (ULift.{v, v'} ↑N)) := ULift.moduleEquiv.symm
⊢ HasInjectiveDimensionLE (of R (ULift.{v', v} ↑M)) n ↔ HasInjectiveDimensionLE N n
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
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:
rw [Submodule.span_le, Set.range_subset_iff]
    intro
    rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]
    exact Submodule.coe_mem _

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R M (Fin 0) 1) ∘ₗ
      { toFun := fun r ↦ r • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim, map_add' := ⋯, map_smul' := ⋯ } =
    LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ { toFun := fun r ↦ r • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      alternatingMapLinearEquiv (AlternatingMap.constOfIsEmpty R M (Fin 0) 1) =
    LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
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
⊢ ↑(zeroEquiv R N) ∘ₗ map 0 f = ↑(zeroEquiv R M)

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ (alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id) ∘ₗ
      have h := ⋯;
      { toFun := fun m ↦ (ιMulti R 1) fun x ↦ m, map_add' := ⋯, map_smul' := ⋯ }) =
    LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
⊢ (have h := ⋯;
      { toFun := fun m ↦ (ιMulti R 1) fun x ↦ m, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ
      alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id) =
    LinearMap.id

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
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
⊢ ↑(oneEquiv R N) ∘ₗ map 1 f = f ∘ₗ ↑(oneEquiv R M)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.StructuredArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
F : C ⥤ Discrete T
t : T
inst✝ : Subsingleton T
X : C
⊢ { as := t } = F.obj X

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Discrete.StructuredArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
F : C ⥤ Discrete T
t : T
inst✝ : Subsingleton T
X : C
⊢ F.obj X = { as := t }

Tactic:
by subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Types

Goal state before:
pp: C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
⊢ Closed F

Tactic:
haveI : ∀ X : Type v₁, PreservesColimits (tensorLeft X) := by infer_instance

Goal state after:
C✝ : Type v₂
inst✝¹ : Category.{v₁, v₂} C✝
C : Type v₁
inst✝ : SmallCategory C
F : C ⥤ Type v₁
this : ∀ (X : Type v₁), PreservesColimits (tensorLeft X)
⊢ Closed F