mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hl : LowerSemicontinuousOn (fun x ↦ x ^ p) (Ici 0)
this : (fun x ↦ x ^ p) ∘ μ[fun a ↦ ‖f a‖ | m] ≤ᵐ[μ] μ[(fun x ↦ x ^ p) ∘ fun a ↦ ‖f a‖ | m]
a : α
ha : ‖μ[f | ?m.214] a‖ ≤ μ[fun x ↦ ‖f x‖ | ?m.214] a
⊢ ((fun x ↦ x ^ p) ∘ μ[fun a ↦ ‖f a‖ | m]) a ≤ μ[(fun x ↦ x ^ p) ∘ fun a ↦ ‖f a‖ | m] a →
    ‖μ[f | m] a‖ ^ p ≤ μ[fun x ↦ ‖f x‖ ^ p | m] a

Tactic:
hb

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
p : ℝ
hp : 1 ≤ p
hfint : Integrable (fun x ↦ ‖f x‖ ^ p) μ
hp' : 0 < p
hm : m ≤ mα
hμm : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hl : LowerSemicontinuousOn (fun x ↦ x ^ p) (Ici 0)
this : (fun x ↦ x ^ p) ∘ μ[fun a ↦ ‖f a‖ | m] ≤ᵐ[μ] μ[(fun x ↦ x ^ p) ∘ fun a ↦ ‖f a‖ | m]
a : α
ha : ‖μ[f | ?m.214] a‖ ≤ μ[fun x ↦ ‖f x‖ | ?m.214] a
hb : ((fun x ↦ x ^ p) ∘ μ[fun a ↦ ‖f a‖ | m]) a ≤ μ[(fun x ↦ x ^ p) ∘ fun a ↦ ‖f a‖ | m] a
⊢ ‖μ[f | m] a‖ ^ p ≤ μ[fun x ↦ ‖f x‖ ^ p | m] a
Module: Mathlib.LinearAlgebra.Basis.Flag

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
n : ℕ
b : Basis (Fin n) K V
i : Fin n
⊢ b.flag i.castSucc ⋖ b.flag i.succ

Tactic:
by
  rw [flag_succ]
  apply covBy_span_singleton_sup
  simp

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁷ : Ring k
inst✝⁶ : PartialOrder k
inst✝⁵ : IsOrderedAddMonoid k
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Module k V
n : ℕ
inst✝¹ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
inst✝ : ZeroLEOneClass k
⊢ {s.points i} ⊆ s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) 0)

Tactic:
by simp [s.point_mem_closedInterior i]

Goal state after:
Module: Mathlib.LinearAlgebra.FixedSubmodule

Goal state before:
pp: case a
R : Type u_1
inst✝² : Semiring R
V : Type u_3
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
e : V ≃ₗ[R] V
W : Submodule R V
hW : W ≤ (↑e).fixedSubmodule
⊢ W ≤ map (DistribSMul.toLinearMap R V e) W

Tactic:
· intro x hx
    refine ⟨x, hx, ?_⟩
    simp only [DistribSMul.toLinearMap_apply, LinearEquiv.smul_def]
    rw [← coe_toLinearMap, ← mem_fixedSubmodule_iff]
    exact hW hx

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
this : f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v) = 0
⊢ (f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v)) • v = 0

Tactic:
by rw [this, zero_smul]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ (f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v)) • v = 0

Tactic:
suffices (f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v)) = 0 by rw [this, zero_smul]

Goal state after:
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
f : Dual R V
v : V
h : IsUnit (1 + f v)
x : V
⊢ f x * ↑(-h.unit⁻¹) + f (x + (f x * ↑(-h.unit⁻¹)) • v) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
m : M × R
⊢ (algebraMap R (CliffordAlgebra Q)) (Q m.1) -
      (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
    (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)

Tactic:
← map_mul,

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
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
m : M × R
⊢ (algebraMap R (CliffordAlgebra Q)) (Q m.1) - (algebraMap R (CliffordAlgebra Q)) (m.2 * m.2) =
    (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft (B' m✝)) ((changeForm ⋯) x✝) -
      (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝)) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft ((B + B') m✝)) ((changeForm ⋯) x✝)

Tactic:
sub_sub,

Goal state after:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' Q'' : QuadraticForm R M
B B' : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
h' : BilinMap.toQuadraticMap B' = Q'' - Q'
x✝ : CliffordAlgebra Q
m✝ : M
hx : (changeForm h') ((changeForm h) x✝) = (changeForm ⋯) x✝
⊢ (ι Q'') m✝ * (changeForm ⋯) x✝ -
      ((contractLeft (B' m✝)) ((changeForm ⋯) x✝) + (changeForm h') ((contractLeft (B m✝)) ((changeForm h) x✝))) =
    (ι Q'') m✝ * (changeForm ⋯) x✝ - (contractLeft ((B + B') m✝)) ((changeForm ⋯) x✝)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion

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
m : M
inst✝ : Invertible (Q m)
⊢ (algebraMap R (CliffordAlgebra Q)) ⅟(Q m) * (algebraMap R (CliffordAlgebra Q)) (Q m) = 1

Tactic:
← map_mul,

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
m : M
inst✝ : Invertible (Q m)
⊢ (algebraMap R (CliffordAlgebra Q)) (⅟(Q m) * Q m) = 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (↑((toEven Q) ((ι Q) (m₁, r₁).1)) + ↑((algebraMap R ↥(even (Q' Q))) (m₁, r₁).2)) *
      (↑((toEven Q) ((ι Q) (m₂, r₂).1)) - ↑((algebraMap R ↥(even (Q' Q))) (m₂, r₂).2)) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)

Tactic:
toEven_ι,

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (e0 Q * (v Q) (m₁, r₁).1 + ↑((algebraMap R ↥(even (Q' Q))) (m₁, r₁).2)) *
      (↑((toEven Q) ((ι Q) (m₂, r₂).1)) - ↑((algebraMap R ↥(even (Q' Q))) (m₂, r₂).2)) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (e0 Q * (v Q) (m₁, r₁).1 + ↑((algebraMap R ↥(even (Q' Q))) (m₁, r₁).2)) *
      (↑((toEven Q) ((ι Q) (m₂, r₂).1)) - ↑((algebraMap R ↥(even (Q' Q))) (m₂, r₂).2)) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)

Tactic:
toEven_ι,

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (e0 Q * (v Q) (m₁, r₁).1 + ↑((algebraMap R ↥(even (Q' Q))) (m₁, r₁).2)) *
      (e0 Q * (v Q) (m₂, r₂).1 - ↑((algebraMap R ↥(even (Q' Q))) (m₂, r₂).2)) =
    (e0 Q * (v Q) m₁ + (algebraMap R (CliffordAlgebra (Q' Q))) r₁) *
      (e0 Q * (v Q) m₂ - (algebraMap R (CliffordAlgebra (Q' Q))) r₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • (e0 Q * (v Q) m₂) -
      ((algebraMap R (CliffordAlgebra (Q' Q))) r₂ * (e0 Q * (v Q) m₁) +
        (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (algebraMap R (CliffordAlgebra (Q' Q))) r₂) =
    e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)

Tactic:
← map_mul,

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
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • (e0 Q * (v Q) m₂) -
      ((algebraMap R (CliffordAlgebra (Q' Q))) r₂ * (e0 Q * (v Q) m₁) +
        (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)) =
    e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case zero
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ i₂ : ZMod 2
hm₂ : m₂ ∈ evenOdd Q₂ i₂
⊢ (map f₁) 0 * (map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((map f₂) m₂ * (map f₁) 0)

Tactic:
rw [map_zero, zero_mul, mul_zero, smul_zero]

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

Goal state before:
pp: case mem.mem_mul.e_a.e_a.zero
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₂ : ZMod 2
m₁' : CliffordAlgebra Q₁
i₁n i : ℕ
x₁ : CliffordAlgebra Q₁
_hx₁ : x₁ ∈ (ι Q₁).range ^ i
v₁ : M₁
⊢ (ι Qₙ) (f₁ v₁) * (map f₂) 0 = (-1) ^ i₂ • ((map f₂) 0 * (ι Qₙ) (f₁ v₁))

Tactic:
rw [map_zero, zero_mul, mul_zero, smul_zero]

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

Goal state before:
pp: case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b : M
⊢ involute ↑y * (involute ↑z * (ι Q) b * ↑z⁻¹) * ↑y⁻¹ ∈ (ι Q).range

Tactic:
obtain ⟨z', hz'⟩ := hz b

Goal state after:
case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b z' : M
hz' : (ι Q) z' = involute ↑z * (ι Q) b * ↑z⁻¹
⊢ involute ↑y * (involute ↑z * (ι Q) b * ↑z⁻¹) * ↑y⁻¹ ∈ (ι Q).range
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
⊢ ∀ (s_1 : Finset ↑s) (g : ↑s → R), Submodule.Quotient.mk (∑ x ∈ s_1, g x • ↑x) = 0 → ∀ i ∈ s_1, g i = 0

Tactic:
Quotient.mk_eq_zero

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
hN : M' ≤ torsion R M
a✝ : Nontrivial R
x✝ : { s // LinearIndepOn R id s }
s : Set M
hs✝ : LinearIndepOn R id s
hs : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • id ↑i = 0 → ∀ i ∈ s_1, g i = 0
⊢ ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ x ∈ s_1, g x • ↑x ∈ M' → ∀ i ∈ s_1, g i = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
r : R
x : 𝒜 ᵍ⊗[R] ℬ
⊢ (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((decompose 𝒜) ((algebraMap R A) r) ⊗ₜ[R] (decompose ℬ) 1))
        ((auxEquiv R 𝒜 ℬ) x)) =
    (auxEquiv R 𝒜 ℬ).symm
      (((gradedMul R (fun x ↦ ↥(𝒜 x)) fun x ↦ ↥(ℬ x)) ((auxEquiv R 𝒜 ℬ) x))
        ((decompose 𝒜) ((algebraMap R A) r) ⊗ₜ[R] (decompose ℬ) 1))

Tactic:
simp_rw [DirectSum.decompose_algebraMap, DirectSum.decompose_one, algebraMap_gradedMul,
      gradedMul_algebraMap]

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

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)ˣ
hx : ↑x ∈ spinGroup Q
y : M
⊢ ↑x * (ι Q) y * ↑x⁻¹ =
    ↑(ConjAct.ofConjAct (ConjAct.toConjAct x)) * (ι Q) y * ↑(ConjAct.ofConjAct (ConjAct.toConjAct x))⁻¹

Tactic:
@ConjAct.ofConjAct_toConjAct

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)ˣ
hx : ↑x ∈ spinGroup Q
y : M
⊢ ↑x * (ι Q) y * ↑x⁻¹ = ↑x * (ι Q) y * ↑x⁻¹
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] 1) * F (1 ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • (F (1 ᵍ⊗ₜ[R] ↑b) * F (↑a ᵍ⊗ₜ[R] 1))

Tactic:
← map_mul,

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
⊢ F (↑a ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • (F (1 ᵍ⊗ₜ[R] ↑b) * F (↑a ᵍ⊗ₜ[R] 1))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Goal state before:
pp: R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
x✝¹ : A
x✝ : B
⊢ F (x✝¹ ᵍ⊗ₜ[R] 1) * F (1 ᵍ⊗ₜ[R] x✝) = F ((of R 𝒜 ℬ) (x✝¹ ⊗ₜ[R] x✝))

Tactic:
← map_mul,

Goal state after:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : Ring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Module ι (Additive ℤˣ)
C : Type ?u.46
inst✝¹ : Ring C
inst✝ : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
x✝¹ : A
x✝ : B
⊢ F (x✝¹ ᵍ⊗ₜ[R] 1 * 1 ᵍ⊗ₜ[R] x✝) = F ((of R 𝒜 ℬ) (x✝¹ ⊗ₜ[R] x✝))
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑⟨m, hm⟩ ∈ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd)

Tactic:
apply Set.mem_of_mem_of_subset hm

Goal state after:
case homogeneous
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i✝ : ℕ
hm✝ : ↥(⋀[R]^i✝ M)
m : ExteriorAlgebra R M
hm : m ∈ ⋀[R]^i✝ M
⊢ ↑(⋀[R]^i✝ M) ⊆ ↑(Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd))
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ ((((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatFst.mkQ.prodMap
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatSnd.mkQ).ker ≤
    (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range

Tactic:
convert! goursatFst_prod_goursatSnd_le (range <| P.prod Q)

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ ((((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatFst.mkQ.prodMap
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatSnd.mkQ).ker =
    (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type v
A : Matrix m n R
inst✝³ : Zero R
inst✝² : LinearOrder m
inst✝¹ : LT n
inst✝ : One R
i₁ i₂ : m
c : n
hA : A.IsReducedRowEchelon
hne : i₁ ≠ i₂
hlead : A.IsLeadingEntry i₂ c
⊢ A i₁ c = 0

Tactic:
rcases hne.lt_or_gt with hlt | hlt
  · exact hA.eq_zero hlt hlead
  · exact hA.isRowEchelon hlt hlead.1

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

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : { s // LinearIndependent 𝔽 s }
⊢ IsUnit (↑M)ᵀ.det

Tactic:
let b := basisOfPiSpaceOfLinearIndependent M.2
    have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b
    rw [← Basis.coePiBasisFun.toMatrix_eq_transpose,
      ← coe_basisOfPiSpaceOfLinearIndependent M.2]
    exact isUnit_det_of_invertible _

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ v j = 0 j

Tactic:
rw [Pi.zero_apply, ← norm_le_zero_iff]

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i = 0
j : n
⊢ ‖v j‖ ≤ 0
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁵ : Finite ι
M : ι → Type u_3
N : Type u_4
γ : ι → Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : MultilinearMap R M N
h : ∀ (j : (i : ι) → γ i), (φ fun i ↦ g (j i)) = φ' fun i ↦ g (j i)
j : (i : ι) → γ i
⊢ (lift φ) (⨂ₜ[R] (i : ι), g (j i)) = (lift φ') (⨂ₜ[R] (i : ι), g (j i))

Tactic:
simpa using h j

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
⊢ Nat.card V = Nat.card V - 1 + 1

Tactic:
have : Nat.card V > 0 := Nat.card_pos

Goal state after:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
this : Nat.card V > 0
⊢ Nat.card V = Nat.card V - 1 + 1
Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ ⋯.choose ≠ 0

Tactic:
← mul_self_eq_zero.ne,

Goal state after:
ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ ⋯.choose * ⋯.choose ≠ 0
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
h : (2 * 2) • Q m - Q m - Q m = 0
⊢ Q m = 0

Tactic:
sub_sub,

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
m : M
h : (2 * 2) • Q m - (Q m + Q m) = 0
⊢ Q m = 0