mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : Mˣ →* Nˣ
k : ℕ
⊢ Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N

Tactic:
rintro _ ⟨ζ, h, rfl⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : Mˣ →* Nˣ
k : ℕ
ζ : Mˣ
h : ζ ∈ ↑(rootsOfUnity k M)
⊢ f ζ ∈ rootsOfUnity k N
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
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (↑f.mapMatrix ↑g).det = f (↑g).det

Tactic:
exact Eq.symm (RingHom.map_det f g.1)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
f g : Q₁ →qᵢ Q₂
h : (fun f ↦ ⇑f.toLinearMap) f = (fun f ↦ ⇑f.toLinearMap) g
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M₄
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
g : Q₁ →qᵢ Q₂
toLinearMap✝ : M₁ →ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ (toLinearMap✝.toFun m) = Q₁ m
h : (fun f ↦ ⇑f.toLinearMap) { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = (fun f ↦ ⇑f.toLinearMap) g
⊢ { toLinearMap := toLinearMap✝, map_app' := map_app'✝ } = g
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
f g : Q₁.IsometryEquiv Q₂
⊢ ⇑f.toLinearEquiv = ⇑g.toLinearEquiv → ⇑f.symm = ⇑g.symm → f = g

Tactic:
cases f

Goal state after:
case mk
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
g : Q₁.IsometryEquiv Q₂
toLinearEquiv✝ : M₁ ≃ₗ[R] M₂
map_app'✝ : ∀ (m : M₁), Q₂ ((↑toLinearEquiv✝).toFun m) = Q₁ m
⊢ ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.toLinearEquiv = ⇑g.toLinearEquiv →
    ⇑{ toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ }.symm = ⇑g.symm →
      { toLinearEquiv := toLinearEquiv✝, map_app' := map_app'✝ } = g
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
v : Fin 2 → R
hab : IsCoprime (v 0) (v 1)
A g : SL(2, R)
hg : ↑g 0 0 = v 0 ∧ ↑g 0 1 = v 1
this : v = ↑g 0
⊢ IsCoprime ((v ᵥ* ↑A) 0) ((v ᵥ* ↑A) 1)

Tactic:
simpa only [this] using! isCoprime_row (g * A) 0

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_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ (F.toLinearMap ∘ₗ ι Q) m * (F.toLinearMap ∘ₗ ι Q) m = (algebraMap R A) (Q m)

Tactic:
LinearMap.comp_apply,

Goal state after:
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_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : CliffordAlgebra Q →ₐ[R] A
m : M
⊢ F.toLinearMap ((ι Q) m) * F.toLinearMap ((ι Q) m) = (algebraMap R A) (Q m)
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 : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
x : ι
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) x = D x

Tactic:
by_cases hx : x = i₀

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
x : ι
hx : x = i₀
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) x = D x

case neg
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
x : ι
hx : ¬x = i₀
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) x = D x
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
⊢ (algebraMap R A) (Q (a + b) - Q a) - (algebraMap R A) (Q b) = (algebraMap R A) (Q (a + b) - Q a - Q b)

Tactic:
← map_sub

Goal state after:
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
⊢ (algebraMap R A) (Q (a + b) - Q a - Q b) = (algebraMap R A) (Q (a + b) - Q a - Q b)
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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * ((ι Q) a * (ι Q) b) = -(x * (ι Q) b * (ι Q) a)

Tactic:
ι_mul_ι_comm_of_isOrtho h,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ x * -((ι Q) b * (ι Q) a) = -(x * (ι Q) b * (ι Q) a)
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
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * (ι Q) b * x = -((ι Q) b * ((ι Q) a * x))

Tactic:
ι_mul_ι_comm_of_isOrtho h,

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ -((ι Q) b * (ι Q) a) * x = -((ι Q) b * ((ι Q) a * x))
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 b : M
⊢ (ι Q) (QuadraticMap.polar (⇑Q) a b • a) - (ι Q) (Q a • b) = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
← map_sub

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b) = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ n ∈ A (n • i)

Tactic:
match n with
  | 0 =>
    rw [pow_zero, zero_nsmul]
    exact one_mem_graded _
  | n + 1 =>
    rw [pow_succ', succ_nsmul']
    exact mul_mem_graded h (pow_mem_graded n h)

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

Goal state before:
pp: case zero
⊢ ↑(T ^ 0) = !![1, 0; 0, 1]

Tactic:
rw [zpow_zero, coe_one, Matrix.one_fin_two]

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

Goal state before:
pp: R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
⊢ (toLinearMap₂' R) J' ∘ₗ toLin' A = ((toLinearMap₂' R) J).compl₂ (toLin' A') ↔ J.IsAdjointPair J' A A'

Tactic:
have h :
    ∀ B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R,
      B = B' ↔ LinearMap.toMatrix₂' R B = LinearMap.toMatrix₂' R B' := by
    intro B B'
    constructor <;> intro h
    · rw [h]
    · exact (LinearMap.toMatrix₂' R).injective h

Goal state after:
R : Type u_1
n : Type u_11
n' : Type u_13
inst✝⁴ : CommRing R
inst✝³ : Fintype n
inst✝² : Fintype n'
J : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
h : ∀ (B B' : (n → R) →ₗ[R] (n' → R) →ₗ[R] R), B = B' ↔ (toMatrix₂' R) B = (toMatrix₂' R) B'
⊢ (toLinearMap₂' R) J' ∘ₗ toLin' A = ((toLinearMap₂' R) J).compl₂ (toLin' A') ↔ J.IsAdjointPair J' A A'
Module: Mathlib.RingTheory.GradedAlgebra.Basic

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u_2
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
c : A
hc : c ∈ 𝒜 i
j : ι
c' : A
hc' : c' ∈ 𝒜 j
h : ¬i + j = 0
h' : j ≠ 0
⊢ 0 = ↑(((decompose 𝒜) c) 0) * ↑(((decompose 𝒜) c') 0)

Tactic:
· simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero]

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

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * (x * ↑u) = y

Tactic:
v.inv_mul_eq_iff_eq_mul

Goal state after:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ A₂ : Matrix n n R
inst✝ : DecidableEq n
P : Matrix n n R
h : IsUnit P
h' : IsUnit P.det
u : (Matrix n n R)ˣ := P.nonsingInvUnit h'
v : (Matrix n n R)ˣ := Pᵀ.nonsingInvUnit ⋯
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₂
⊢ x * ↑u = ↑v * y ↔ x * ↑u = ↑v * y
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ ¬Q.Anisotropic ↔ ∃ x, x ≠ 0 ∧ Q x = 0

Tactic:
simp only [Anisotropic, not_forall, exists_prop, and_comm]

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

Goal state before:
pp: R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
a : R
Q : QuadraticForm R (n → R)
⊢ (a • Q).toMatrix' = a • Q.toMatrix'

Tactic:
simp [toMatrix']

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

Goal state before:
pp: R : Type u_3
N : Type u_5
P : Type u_6
n : Type w
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : CommRing R
inst✝⁴ : Invertible 2
inst✝³ : AddCommGroup N
inst✝² : Module R N
b : Basis n R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
b' : Basis n R P
Q : QuadraticForm R P
f : N →ₗ[R] P
⊢ discr b (QuadraticMap.comp Q f) = ((LinearMap.toMatrix b b') f).det * ((LinearMap.toMatrix b b') f).det * discr b' Q

Tactic:
simp [mul_left_comm, toMatrix_comp b b', mul_comm, discr]

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

Goal state before:
pp: K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
c : K
y : V
hy : y ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : c • x + y = 0
⊢ c = 0

Tactic:
add_eq_zero_iff_neg_eq

Goal state after:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : (B x) x ≠ 0
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K] K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ : (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))).IsOrthoᵢ ⇑v'
c : K
y : V
hy : y ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
⊢ c = 0
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
⊢ 1 ≤ evenOdd Q 0

Tactic:
by
  refine le_trans ?_ (le_iSup _ ⟨0, Nat.cast_zero⟩)
  exact (pow_zero _).ge

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

Goal state before:
pp: n : ℕ
β : Type u_2
f : Fin n ↪ β
⊢ ↑(ofFinEmb n β f) = range ⇑f

Tactic:
by
  ext
  simp [mem_ofFinEmb_iff_mem_range]

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ a ∈ s

Tactic:
by simpa using a_mem

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

Goal state before:
pp: case h
α : Type u_1
n : ℕ
h : 0 < n
inst✝ : Infinite α
a : α
s : Finset α
a_mem : {a} ⊆ s
s_card : #s = n
⊢ s ∈ powersetCard α n ∧ a ∈ s

Tactic:
exact ⟨mem_iff.mp s_card, by simpa using a_mem⟩

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 : (Nat.card α).choose n = 1
⊢ False

Tactic:
Nat.choose_eq_one_iff

Goal state after:
case inl.inr
α : Type u_1
n : ℕ
h1 : 0 < n
val✝ : Fintype α
h2 : n < Nat.card α
h : n = 0 ∨ Nat.card α = n
⊢ False
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ ¬Nat.card α < n ∧ ¬(Nat.card α).choose n = 1 ↔ 0 < n ∧ n < Nat.card α

Tactic:
Nat.choose_eq_one_iff

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Finite α
⊢ ¬Nat.card α < n ∧ ¬(n = 0 ∨ Nat.card α = n) ↔ 0 < n ∧ n < Nat.card α
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✝
⊢ (LinearMap.mulLeft R ((ι R) m✝) ∘ₗ liftAlternating (ιMulti R)) x✝ = (CliffordAlgebra.ι 0) m✝ * x✝

Tactic:
LinearMap.comp_apply,

Goal state after:
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✝
⊢ (LinearMap.mulLeft R ((ι R) m✝)) ((liftAlternating (ιMulti R)) x✝) = (CliffordAlgebra.ι 0) m✝ * x✝
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
m : M
⊢ toExterior ((ι R) m) = (ExteriorAlgebra.ι R) m

Tactic:
simp [toExterior]

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
⊢ HasInjectiveDimensionLE M n ↔ HasInjectiveDimensionLE N n

Tactic:
let eN : N ≃ₗ[R'] ModuleCat.of R' (ULift.{v} N) := ULift.moduleEquiv.symm

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 M n ↔ HasInjectiveDimensionLE N n
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
⊢ F.Final ↔
    (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨fun hF => ⟨?_, ?_⟩, fun h => final_of_exists_of_isFiltered F h.1 h.2⟩

Goal state after:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
hF : F.Final
⊢ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
X : C × C
this : ∀ (Y : C), IsFiltered (StructuredArrow Y (Under.forget X.1))
⊢ IsFiltered (StructuredArrow X (Functor.diag C))

Tactic:
apply IsFiltered.of_equivalence (StructuredArrow.ofDiagEquivalence X).symm

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)
j : J
k k' : K
f : k ⟶ k'
| ((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')

Tactic:
arg 1; rw [← uncurry_obj_map F (𝟙 j ×ₘ f)]

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)
j : J
k k' : K
f : k ⟶ k'
| (uncurry.obj F).map (𝟙 j ×ₘ f)
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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
j : J
k : K
⊢ m ≫ c.π.app (j, k) = s.π.app j ≫ (D.obj j).π.app k

Tactic:
rw [← w j]

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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
j : J
k : K
⊢ m ≫ c.π.app (j, k) = (m ≫ (coneOfConeUncurry Q c).π.app j) ≫ (D.obj j).π.app k
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
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
j : J
k : K
⊢ c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ s.ι.app j

Tactic:
rw [← w j]

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
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
j : J
k : K
⊢ c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ (coconeOfCoconeUncurry Q c).ι.app j ≫ m
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
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) = limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
← cancel_epi (limitUncurryIsoLimitCompLim F).hom

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
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) =
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
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
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j

Tactic:
rw [← cancel_mono (colimitUncurryIsoColimitCompColim F).inv]
  simp

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'✝ G G' : Subfunctor F
h : G ≤ G'
Z✝ : C ⥤ Type w
x✝¹ x✝ : Z✝ ⟶ G.toFunctor
e : x✝¹ ≫ homOfLe h = x✝ ≫ homOfLe h
U : C
x : Z✝.obj U
⊢ (hom (x✝¹.app U)) x = (hom (x✝.app U)) x

Tactic:
by
    exact Subtype.ext (congr_arg Subtype.val <| (congr_hom (congr_app e U) x) :)

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ ((isoMk (fun X ↦ β_ (x✝¹.obj X) (x✝.obj X)) ⋯).hom ≫ (isoMk (fun X ↦ β_ (x✝.obj X) (x✝¹.obj X)) ⋯).hom).app X✝ =
    (𝟙 (x✝¹ ⊗ x✝)).app X✝

Tactic:
apply SymmetricCategory.symmetry (C := ModuleCat (R.obj _))

Goal state after: