mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k + n.val)), motive xv ⋯

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv : CliffordAlgebra Q
⊢ ∀ (hx : xv ∈ (ι Q).range ^ (2 * k + n.val)), motive xv ⋯
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
r : R
⊢ motive ((algebraMap R (CliffordAlgebra Q)) r * b) ⋯

Tactic:
[

Goal state after:
case mem_mul_mem.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
r : R
⊢ motive ((algebraMap R (CliffordAlgebra Q)) r * b) ⋯
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ ((ι Q).range ^ 2) ^ n
hy : y ∈ ((ι Q).range ^ 2) ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
⊢ motive ((x + y) * b) ⋯

Tactic:
[

Goal state after:
case mem_mul_mem.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx✝ : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x y : CliffordAlgebra Q
n : ℕ
hx : x ∈ ((ι Q).range ^ 2) ^ n
hy : y ∈ ((ι Q).range ^ 2) ^ n
ihx : motive (x * b) ⋯
ihy : motive (y * b) ⋯
⊢ motive ((x + y) * b) ⋯
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
⊢ ∀ (hx : x ∈ (ι Q).range ^ 2), motive (x * y * b) ⋯

Tactic:
[

Goal state after:
case mem_mul_mem.mem_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
⊢ ∀ (hx : x ∈ (ι Q).range ^ 2), motive (x * y * b) ⋯
Module: Mathlib.Data.Set.PowersetCard

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
⊢ Infinite ↑(powersetCard α n)

Tactic:
rw [← not_finite_iff_infinite]

Goal state after:
α : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Infinite α
⊢ ¬Finite ↑(powersetCard α n)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
⊢ motive (m * n * y * b) ⋯

Tactic:
[

Goal state after:
case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n✝ : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n✝ → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n✝.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝) (hy : y ∈ evenOdd Q n✝),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n✝), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n✝
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n✝.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m : CliffordAlgebra Q
hm : m ∈ (ι Q).range
n : CliffordAlgebra Q
hn : n ∈ (ι Q).range
⊢ motive (m * n * y * b) ⋯
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : (ι Q) m₁ ∈ (ι Q).range
m₂ : M
hn : (ι Q) m₂ ∈ (ι Q).range
⊢ motive ((ι Q) m₁ * (ι Q) m₂ * y * b) ⋯

Tactic:
[

Goal state after:
case mem_mul_mem.mem_mul.mem_mul_mem
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝ : CliffordAlgebra Q
hx : x✝ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x : CliffordAlgebra Q
n'' : ℕ
y : CliffordAlgebra Q
hy : y ∈ ((ι Q).range ^ 2) ^ n''
ihy : motive (y * b) ⋯
m₁ : M
hm : (ι Q) m₁ ∈ (ι Q).range
m₂ : M
hn : (ι Q) m₂ ∈ (ι Q).range
⊢ motive ((ι Q) m₁ * (ι Q) m₂ * y * b) ⋯
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Grading

Goal state before:
pp: case mem_mul_mem.mem_mul.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝¹ : CliffordAlgebra Q
hx✝ : x✝¹ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ ((ι Q).range ^ 2) ^ n''
ihy✝ : motive (y✝ * b) ⋯
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range * (ι Q).range
y : CliffordAlgebra Q
hy : y ∈ (ι Q).range * (ι Q).range
ihx : motive (x * y✝ * b) ⋯
ihy : motive (y * y✝ * b) ⋯
⊢ motive ((x + y) * y✝ * b) ⋯

Tactic:
[

Goal state after:
case mem_mul_mem.mem_mul.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
motive : (x : CliffordAlgebra Q) → x ∈ evenOdd Q n → Prop
range_ι_pow : ∀ (v : CliffordAlgebra Q) (h : v ∈ (ι Q).range ^ n.val), motive v ⋯
add :
  ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) (hy : y ∈ evenOdd Q n),
    motive x hx → motive y hy → motive (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n), motive x hx → motive ((ι Q) m₁ * (ι Q) m₂ * x) ⋯
x✝¹ : CliffordAlgebra Q
hx✝ : x✝¹ ∈ evenOdd Q n
k : ℕ
xv a b : CliffordAlgebra Q
hb : b ∈ (ι Q).range ^ n.val
x✝ : CliffordAlgebra Q
n'' : ℕ
y✝ : CliffordAlgebra Q
hy✝ : y✝ ∈ ((ι Q).range ^ 2) ^ n''
ihy✝ : motive (y✝ * b) ⋯
x : CliffordAlgebra Q
hx : x ∈ (ι Q).range * (ι Q).range
y : CliffordAlgebra Q
hy : y ∈ (ι Q).range * (ι Q).range
ihx : motive (x * y✝ * b) ⋯
ihy : motive (y * y✝ * b) ⋯
⊢ motive ((x + y) * y✝ * b) ⋯
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
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
⊢ ∀ (h : ιv ∈ (CliffordAlgebra.ι Q).range ^ ZMod.val 1), P ιv ⋯

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : (x : CliffordAlgebra Q) → x ∈ evenOdd Q 1 → Prop
ι : ∀ (v : M), P ((CliffordAlgebra.ι Q) v) ⋯
add : ∀ (x y : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) (hy : y ∈ evenOdd Q 1), P x hx → P y hy → P (x + y) ⋯
ι_mul_ι_mul :
  ∀ (m₁ m₂ : M) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1),
    P x hx → P ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂ * x) ⋯
x : CliffordAlgebra Q
hx : x ∈ evenOdd Q 1
ιv : CliffordAlgebra Q
⊢ ∀ (h : ιv ∈ (CliffordAlgebra.ι Q).range ^ ZMod.val 1), P ιv ⋯
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 ((ι R) m * (ι R) m) = 0

Tactic:
ι_sq_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
⊢ g 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
⊢ Disjoint (ι R).range 1

Tactic:
rw [Submodule.disjoint_def]
  rintro _ ⟨x, hx⟩ h
  obtain ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩ := Submodule.mem_one.mp h
  rw [ι_eq_algebraMap_iff x] at hx
  rw [hx.2, map_zero]

Goal state after:
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
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : i = 0
⊢ (ι R) (f 0) * (ι R) (f 0) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
ι_sq_zero,

Goal state after:
case pos
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i)).prod = 0
f : Fin (n + 1) → M
i : Fin (n + 1)
h : i = 0
⊢ 0 * (List.ofFn fun i ↦ (ι R) (f i.succ)).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✝
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:
rw [hx] at hfxy h

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
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ : CliffordAlgebra 0
m✝ : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ (g.compAlternatingMap (f i.succ)).curryLeft m✝) x✝ =
    (liftAlternating fun i ↦ g.compAlternatingMap ((f i.succ).curryLeft m✝)) x✝

Tactic:
[

Goal state after:
case ι_mul
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
g : N →ₗ[R] N'
x✝ : CliffordAlgebra 0
m✝ : M
hx :
  ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N),
    (liftAlternating fun i ↦ g.compAlternatingMap (f i)) x✝ = g ((liftAlternating f) x✝)
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (liftAlternating fun i ↦ (g.compAlternatingMap (f i.succ)).curryLeft m✝) x✝ =
    (liftAlternating fun i ↦ g.compAlternatingMap ((f i.succ).curryLeft m✝)) x✝
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✝
⊢ (liftAlternating (ιMulti R)) ((CliffordAlgebra.ι 0) m✝ * x✝) = (CliffordAlgebra.ι 0) m✝ * x✝

Tactic:
[

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✝
⊢ (liftAlternating (ιMulti R)) ((CliffordAlgebra.ι 0) m✝ * x✝) = (CliffordAlgebra.ι 0) m✝ * x✝
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
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)

Tactic:
[

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'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(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
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c •
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)

Tactic:
[

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'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯) =
    (RingHom.id R) c •
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a.refine_1
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ ⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f ∈ {a | range a ⊆ s}

Tactic:
rw [Set.mem_ofPred_eq, Set.range_comp, Set.image_subset_iff]
      apply Subset.trans ?_ (s.image_subset_preimage_of_inverse ExteriorAlgebra.ι_leftInverse)
      grind

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'
ι : Type u_4
inst✝³ : DecidableEq ι
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s : (relations R ι M).Solution N
inst✝ : DecidableEq ι
m : ι → M
i : ι
x y : M
⊢ s.var (update m i (x + y)) = s.var (update m i x) + s.var (update m i y)

Tactic:
by
        have := s.linearCombination_var_relation (.add m i x y)
        dsimp at this ⊢
        rw [map_sub, map_add, Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, one_smul, sub_eq_zero] at this
        convert! this.symm

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Module.rank R ↑S.X₂ = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃

Tactic:
Module.Free.rank_eq_card_chooseBasisIndex,

Goal state after:
R : Type u_3
inst✝³ : Ring R
S : ShortComplex (ModuleCat R)
hS' : S.ShortExact
inst✝² : Free R ↑S.X₁
inst✝¹ : Free R ↑S.X₃
inst✝ : StrongRankCondition R
this : Free R ↑S.X₂
⊢ Cardinal.mk (Free.ChooseBasisIndex R ↑S.X₂) = Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃
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 (range v) = ⊤
⊢ Submodule.span R (range (ιMulti_family R n v)) = ⊤

Tactic:
apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))
  rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]
  simpa using ιMulti_family_span_fixedDegree_of_span R hv

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

Goal state before:
pp: case succ
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 : ℕ
hn : (Λ.chainComplexMap (𝟙 X)).f n = (𝟙 (Λ.chainComplex X)).f n
⊢ (Λ.chainComplexMap (𝟙 X)).f (n + 1) = (𝟙 (Λ.chainComplex X)).f (n + 1)

Tactic:
obtain _ | n := n <;> simp [hn]

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

Goal state before:
pp: case succ
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 Y : A
inst✝⁴ : ι.Full
inst✝³ : ι.Faithful
inst✝² : HasZeroMorphisms C
inst✝¹ : Abelian A
inst✝ : Λ.F.PreservesZeroMorphisms
n : ℕ
hn : (Λ.chainComplexMap 0).f n = HomologicalComplex.Hom.f 0 n
⊢ (Λ.chainComplexMap 0).f (n + 1) = HomologicalComplex.Hom.f 0 (n + 1)

Tactic:
obtain _ | n := n <;> simp [hn]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Connected

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
T : Type w
inst✝ : Unique T
F : C ⥤ Discrete T
⊢ IsConnected C ↔ F.Initial

Tactic:
rw [← isConnected_iff_of_equivalence
    (Discrete.costructuredArrowEquivalenceOfUnique F default)]
  refine ⟨fun _ ↦ ⟨?_⟩, fun _ ↦ inferInstance⟩
  rintro ⟨d⟩
  obtain rfl := Subsingleton.elim d default
  infer_instance

Goal state after: