mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
⊢ ∀ᵐ (x : X) ∂μ, ∀ (n : ι), x ∈ s n → ∑' (n : ι), ‖f n x‖ₑ < ∞

Tactic:
apply ae_all_iff.2 (fun n ↦ ?_)

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
n : ι
⊢ ∀ᵐ (a : X) ∂μ, a ∈ s n → ∑' (n : ι), ‖f n a‖ₑ < ∞
Module: Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Goal state before:
pp: X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
n : ι
this : ∀ᵐ (x : X) ∂μ, ∀ (i : ℕ), x ∈ s n ∩ spanningSets (μ.restrict (s n)) i → ∑' (n : ι), ‖f n x‖ₑ < ∞
⊢ ∀ᵐ (a : X) ∂μ, a ∈ s n → ∑' (n : ι), ‖f n a‖ₑ < ∞

Tactic:
filter_upwards [this] with x hx h'x

Goal state after:
X : Type u_1
E : Type u_2
x✝ : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
ι : Type u_3
inst✝ : Countable ι
p : ℝ≥0∞
hp : 1 ≤ p
f : ι → X → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ∞
h'p : p < ∞
A : ∀ (s : Set X), MeasurableSet s → μ s ≠ ∞ → ∀ᵐ (x : X) ∂μ, x ∈ s → ∑' (n : ι), ‖f n x‖ₑ < ∞
s : ι → Set X
s_meas : ∀ (n : ι), MeasurableSet (s n)
hs : ∀ (n : ι), f n =ᵐ[μ.restrict (s n)ᶜ] 0
h's : ∀ (n : ι), SigmaFinite (μ.restrict (s n))
n : ι
this : ∀ᵐ (x : X) ∂μ, ∀ (i : ℕ), x ∈ s n ∩ spanningSets (μ.restrict (s n)) i → ∑' (n : ι), ‖f n x‖ₑ < ∞
x : X
hx : ∀ (i : ℕ), x ∈ s n ∩ spanningSets (μ.restrict (s n)) i → ∑' (n : ι), ‖f n x‖ₑ < ∞
h'x : x ∈ s n
⊢ ∑' (n : ι), ‖f n x‖ₑ < ∞
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ↑↑(condExpL1 hm μ (f + g)) =ᵐ[μ] μ[f | m] + μ[g | m]

Tactic:
condExpL1_add hf hg

Goal state after:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ↑↑(condExpL1 hm μ f + condExpL1 hm μ g) =ᵐ[μ] μ[f | m] + μ[g | m]
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case neg
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : ¬CompleteSpace ↥(Lp F' 1 μ)
⊢ 0 =ᵐ[μ] ↑0

Tactic:
exact (coeFn_zero _ 1 _).symm

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

Goal state before:
pp: case pos
α : Type u_1
F' : Type u_3
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : α → F'
hF' : CompleteSpace ↥(Lp F' 1 μ)
hf : Integrable f μ
hf' : f =ᵐ[μ] 0
⊢ 0 =ᵐ[μ] ↑0

Tactic:
exact (coeFn_zero _ 1 _).symm

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic

Goal state before:
pp: α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : PartialOrder E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
⊢ μ[f | m] ≤ᵐ[μ] μ[g | m]

Tactic:
by_cases hm : m ≤ m₀
  swap; · simp_rw [condExp_of_not_le hm]; rfl
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; rfl
  exact (condExp_ae_eq_condExpL1 hm _).trans_le
    ((condExpL1_mono hf hg hfg).trans_eq (condExp_ae_eq_condExpL1 hm _).symm)

Goal state after:
Module: Mathlib.Lean.Thunk

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
a b : Thunk α
a✝ : a.get = b.get
⊢ a.get = b.get

Tactic:
assumption

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

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
B₁ : LinearMap.BilinForm R M₁
B₂ : LinearMap.BilinForm R M₂
B₃ : LinearMap.BilinForm R M₃
f : B₁.IsometryEquiv B₂
g : B₂.IsometryEquiv B₃
⊢ ∀ (n m : M₁),
    (B₃ ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun n)) ((↑(f.toLinearEquiv ≪≫ₗ g.toLinearEquiv)).toFun m) =
      (B₁ n) m

Tactic:
intro n m; rw [← f.map_app, ← g.map_app]; rfl

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

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) (1 - w i)

Tactic:
shift_eq ⟨p j, mem_affineSpan k <| Set.mem_image_of_mem _ hj⟩

Goal state after:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
i : ι
w : ι → k
hw : ∑ i, w i = 1
h✝ : Nontrivial k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈
    map (↑(AffineEquiv.constVAdd k P ((1 - (1 - w i)) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (affineSpan k (p '' {i}ᶜ))
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✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈ (affineSpan k (p '' {i}ᶜ)).shift (p i) c → w i = 1 - c

Tactic:
shift_eq ⟨p j, mem_affineSpan k <| Set.mem_image_of_mem _ hj⟩

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : AddTorsor V P
inst✝² : Module k V
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
p : ι → P
h : AffineIndependent k p
i : ι
w : ι → k
hw : ∑ i, w i = 1
c : k
j : ι
hj : j ≠ i
⊢ (affineCombination k univ p) w ∈
      map (↑(AffineEquiv.constVAdd k P ((1 - c) • (p i -ᵥ ↑⟨p j, ⋯⟩)))) (affineSpan k (p '' {i}ᶜ)) →
    w i = 1 - c
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p : P
⊢ (∃ y ∈ s, (1 - r) • (c -ᵥ ↑h.some) +ᵥ y = p) ↔ ∃ y ∈ s, r • (y -ᵥ c) +ᵥ c = p

Tactic:
constructor <;> intro ⟨x, hmem, heq⟩ <;> rw [← heq]

Goal state after:
case inr.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ ∃ y ∈ s, r • (y -ᵥ c) +ᵥ c = (1 - r) • (c -ᵥ ↑h.some) +ᵥ x

case inr.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : r • (x -ᵥ c) +ᵥ c = p
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑h.some) +ᵥ y = r • (x -ᵥ c) +ᵥ c
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeHom

Goal state before:
pp: R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
⊢ IsBaseChange S (compRight R ε)

Tactic:
apply of_equiv (linearMapRightBaseChangeEquiv M ibc)

Goal state after:
R : Type u_1
inst✝¹² : CommSemiring R
S : Type u_2
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_5
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : Module S P
inst✝² : IsScalarTower R S P
inst✝¹ : Free R M
inst✝ : Module.Finite R M
ε : N →ₗ[R] P
ibc : IsBaseChange S ε
⊢ ∀ (x : M →ₗ[R] N), (linearMapRightBaseChangeEquiv M ibc) (1 ⊗ₜ[R] x) = (compRight R ε) x
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
f : V →ₗ[R] V
a : R
hf : ∀ (x : V), f x = a • x
⊢ f ∈ center (End R V)

Tactic:
simp [mem_center_iff, isMulCentral_iff, commute_iff_eq, mul_assoc, LinearMap.ext_iff, hf]

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)
⊢ dilatransvection h ∈ dilatransvections R V

Tactic:
by
  simp only [dilatransvections, Set.mem_ofPred_eq]
  refine ⟨f, v, by simp⟩

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

Goal state before:
pp: R : Type u_3
V : Type u_4
A : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : CommRing A
inst✝ : Algebra R A
e : V ≃ₗ[R] V
he : e ∈ dilatransvections R V
⊢ LinearEquiv.baseChange R A V V e ∈ dilatransvections A (A ⊗[R] V)

Tactic:
by
  obtain ⟨f, v, he⟩ := he
  use (f.baseChange A), (1 ⊗ₜ[R] v)
  simp [he, LinearMap.transvection.baseChange]

Goal state after:
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
⊢ (ofEven Q) ⟨↑((toEven Q) ((ι Q) m)), ⋯⟩ =
    ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 0)

Tactic:
simp_rw [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
⊢ (ofEven Q) ⟨e0 Q * (v Q) m, ⋯⟩ =
    ((ι Q) 0 + (algebraMap R (CliffordAlgebra Q)) 1) * ((ι Q) m - (algebraMap R (CliffordAlgebra Q)) 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 ℬ
⊢ (auxEquiv R 𝒜 ℬ) 1 = 1

Tactic:
← of_one,

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 ℬ
⊢ (auxEquiv R 𝒜 ℬ) ((of R 𝒜 ℬ) 1) = 1
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra) (toTensorAlgebra a)) b

Tactic:
← LinearMap.comp_apply

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : ⨂[R]^i M
b : ⨂[R]^j M
⊢ ((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra) a) b =
    (((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra) a) b
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk (1 + n) ((PiTensorProduct.tprod R) (Fin.append (fun x ↦ x₀) x)) =
    GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))

Tactic:
refine TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) ?_

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  (List.map (fun a ↦ GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 ↦ x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
⊢ (TensorPower.cast R M ⋯) (GradedMonoid.mk (1 + n) ((PiTensorProduct.tprod R) (Fin.append (fun x ↦ x₀) x))).snd =
    (GradedMonoid.mk (n + 1) ((PiTensorProduct.tprod R) (Fin.cons x₀ x))).snd
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ringConGen (rel R A) = (ringConGen (rel' R A)).comap (powerAlgebraEquivFreeTensorAlgebra R A).symm

Tactic:
rel'

Goal state after:
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ringConGen (rel R A) = (ringConGen (rel R A on ⇑ofDirectSum)).comap (powerAlgebraEquivFreeTensorAlgebra R A).symm
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
⊢ g i = ∑ x, if i = f x then ⋯.choose • a x else 0

Tactic:
rw [eq_comm]

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i
i : ι
⊢ (∑ x, if i = f x then ⋯.choose • a x else 0) = g i
Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
σ : Perm n
x✝ : σ ∈ univ
⊢ abv (Perm.sign σ • ∏ i, A (σ i) i) = ∏ i, abv (A (σ i) i)

Tactic:
abv.map_units_int_smul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
σ : Perm n
x✝ : σ ∈ univ
⊢ abv (∏ i, A (σ i) i) = ∏ i, abv (A (σ i) i)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ j : Fin (n + 1)
⊢ (M.submatrix j.succAbove id).det = (↑↑j).negOnePow • (M.submatrix (Fin.succAbove 0) id).det

Tactic:
induction j using Fin.induction with

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
hc : Fintype.card (Fin n) = Fintype.card ι
⊢ n = Fintype.card ι

Tactic:
simpa using hc

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
x✝ : Nonempty (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
⊢ n = Fintype.card ι

Tactic:
have hc := card_eq_of_linearEquiv ℤ <| bN.equivFun.symm.trans e
    simpa using hc

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

Goal state before:
pp: 𝔽 : Type u_1
inst✝¹ : Field 𝔽
inst✝ : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
⊢ LinearIndependent 𝔽 (↑M).col

Tactic:
by
    apply linearIndependent_iff_card_eq_finrank_span.2
    rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
hι : Nat.card ι = n + 1
this : Nonempty ι
i₀ : ι
e : (⨂[R] (i : ι), M i) ≃ₗ[R] M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) :=
  equivPiTensorComplSingletonTensor R M i₀ ≪≫ₗ TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀)
ψ ψ' : M i₀ ⊗[R] (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) →ₗ[R] N
h :
  ∀ (j : (i : ι) → γ i),
    ψ
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i)))) =
      ψ'
        ((TensorProduct.comm R (⨂[R] (i : ↑{i₀}ᶜ), M ↑i) (M i₀))
          ((equivPiTensorComplSingletonTensor R M i₀) (⨂ₜ[R] (i : ι), g (j i))))
g₀ : γ i₀
j : (i : ↑{i₀}ᶜ) → γ ↑i
x : ι
hx : x ∈ {i₀}ᶜ
⊢ ↑⟨x, hx⟩ ≠ i₀

Tactic:
assumption

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

Goal state before:
pp: k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)

Tactic:
let e : V ≃ₗ[k] (Fin n → k) := LinearEquiv.ofFinrankEq _ _ (by simpa)

Goal state after:
k✝ : Type u_1
V✝ : Type u_2
inst✝⁶ : Field k✝
inst✝⁵ : AddCommGroup V✝
inst✝⁴ : Module k✝ V✝
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
n : ℕ
h : Module.finrank k V = n
hf : Finite V
this : 1 < Nat.card k
e : V ≃ₗ[k] Fin n → k := LinearEquiv.ofFinrankEq V (Fin n → k) ⋯
⊢ Nat.card (ℙ k V) * (Nat.card k - 1) = (∑ i ∈ Finset.range n, Nat.card k ^ i) * (Nat.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Subspace

Goal state before:
pp: case of
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ⊆ ↑B
x x✝ : ℙ K V
hx✝ : x✝ ∈ A
⊢ x✝ ∈ A

Tactic:
assumption

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

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
y : ℙ K V
p q : Submodule K V
hp1 : Module.finrank K ↥p = 2
hq1 : Module.finrank K ↥q = 2
hp3 : y ∈ Submodule.projectivization p
hq3 : y ∈ Submodule.projectivization q
v : V
hv : v ≠ 0
hxy : mk K v hv ≠ y
hp2 : mk K v hv ∈ Submodule.projectivization p
hq2 : mk K v hv ∈ Submodule.projectivization q
⊢ p = q

Tactic:
induction y using ind with | h w hw =>
  rw [← independent_pair_iff_ne, independent_mk_iff_LinearIndependent] at hxy
  rw [line_unique' hv hw hxy p hp1 hp2 hp3, line_unique' hv hw hxy q hq1 hq2 hq3]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
⊢ ⨆ p, lineStab p.submodule = ⊤

Tactic:
refine le_antisymm le_top (SL2Gen.SL_card_two_lineStab_sup_eq_top (F := F) ▸
    sup_le ?_ ?_)
  <;> rw [← Projectivization.submodule_mk (K := F) _ (Pi.single_ne_zero_iff.2 one_ne_zero)]
  <;> exact le_iSup_iff.2 fun b a ↦ a _

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: case refine_2
R : Type u_3
V : Type u_4
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
v : V
A : V →ₗ[R] V
hAv : A v ∈ R ∙ v
c : R
hc : c • v = A v
x✝ : ↥(R ∙ v)
a : R
hw : a • v ∈ R ∙ v
⊢ (A.restrict ⋯) ⟨a • v, hw⟩ = (c • id) ⟨a • v, hw⟩

Tactic:
· simp [Subtype.ext_iff, ← hc, smul_comm a c v]

Goal state after: