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

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP : P ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg))
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)), ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) = MemLp.toLp f ⋯
⊢ P (MemLp.toLp f ⋯ + ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp g hg)))

Tactic:
rw [h_eq g hg] at hgP ⊢

Goal state after:
case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP : P (MemLp.toLp g ⋯)
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)), ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) = MemLp.toLp f ⋯
⊢ P (MemLp.toLp f ⋯ + MemLp.toLp g ⋯)
Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝² : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
hp_ne_top : p ≠ ∞
P : ↥(Lp F p μ) → Prop
h_ind : ∀ (c : F) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P ↑(simpleFunc.indicatorConst p ⋯ ⋯ c)
h_add :
  ∀ ⦃f g : α → F⦄ (hf : MemLp f p μ) (hg : MemLp g p μ),
    AEStronglyMeasurable f μ →
      AEStronglyMeasurable g μ →
        Disjoint (Function.support f) (Function.support g) →
          P (MemLp.toLp f hf) → P (MemLp.toLp g hg) → P (MemLp.toLp f hf + MemLp.toLp g hg)
h_closed : IsClosed {f | P ↑f}
f✝ : ↥(Lp F p μ)
hf✝ : AEStronglyMeasurable (↑↑f✝) μ
f' : ↥(lpMeas F ℝ m p μ) := ⟨f✝, hf✝⟩
g✝ : ↥(Lp F p (μ.trim hm)) := (lpMeasToLpTrimLie F ℝ p μ hm) f'
hfg : f' = (lpMeasToLpTrimLie F ℝ p μ hm).symm g✝
f g : α → F
hf : MemLp f p (μ.trim hm)
hg : MemLp g p (μ.trim hm)
h_disj : Disjoint (Function.support f) (Function.support g)
hfP : P (MemLp.toLp f ⋯)
hgP : P (MemLp.toLp g ⋯)
h_eq :
  ∀ (f : α → F) (hf : MemLp f p (μ.trim hm)), ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (MemLp.toLp f hf)) = MemLp.toLp f ⋯
⊢ P (MemLp.toLp f ⋯ + MemLp.toLp g ⋯)

Tactic:
exact h_add (memLp_of_memLp_trim hm hf) (memLp_of_memLp_trim hm hg)
      (hf.aestronglyMeasurable.of_trim hm) (hg.aestronglyMeasurable.of_trim hm) h_disj hfP hgP

Goal state after:
Module: Mathlib.MeasureTheory.Function.ConditionalLExpectation

Goal state before:
pp: case pos.e_f
Ω : Type u_1
mΩ₀ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
mΩ : MeasurableSpace Ω
inst✝ : Countable ι
X : ι → Ω → ℝ≥0∞
hX : ∀ (i : ι), AEMeasurable (X i) P
hm : mΩ ≤ mΩ₀
hσ : SigmaFinite (P.trim hm)
s : Set Ω
hs : MeasurableSet s
i : ι
⊢ ∫⁻ (a : Ω) in s, P⁻[X i | mΩ] a ∂P = ∫⁻ (a : Ω) in s, X i a ∂P

Tactic:
exact setLIntegral_condLExp hm P (X i) hs

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ b.flag k.succ

Tactic:
by rw [flag_succ]; exact le_sup_right

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₂
⊢ ∀ (n m : M₂), (B₁ ((↑f.symm).toFun n)) ((↑f.symm).toFun m) = (B₂ n) m

Tactic:
intro _

Goal state after:
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₂
n✝ : M₂
⊢ ∀ (m : M₂), (B₁ ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m) = (B₂ n✝) m
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
f : M₁ ≃ₗ[R] M
⊢ ∀ (n m : M), ((B.comp ↑f ↑f) ((↑f.symm).toFun n)) ((↑f.symm).toFun m) = (B n) m

Tactic:
intro _

Goal state after:
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
f : M₁ ≃ₗ[R] M
n✝ : M
⊢ ∀ (m : M), ((B.comp ↑f ↑f) ((↑f.symm).toFun n✝)) ((↑f.symm).toFun m) = (B n✝) m
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
t : Finset ι
w' : ι → k
ht✝ : ↑t ⊆ {i}ᶜ
hw' : ∑ i ∈ t, w' i = 1
hqmem : (affineCombination k t p) w' ∈ affineSpan k (p '' {i}ᶜ)
heq : ∀ i_1 ∈ univ, ((1 - c) • (Pi.single i 1 - Pi.single j 1) + (↑t).indicator w') i_1 = w i_1
ht : (↑t).indicator w' i = 0
⊢ w i = 1 - c

Tactic:
simpa [hj.symm, ht] using (heq i (mem_univ i)).symm

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 : f v = 0
x y : V
⊢ (LinearMap.transvection f v) (x + y) = (LinearMap.transvection f v) x + (LinearMap.transvection f v) y

Tactic:
simp [map_add]

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 y : V
⊢ (LinearMap.transvection f v) (x + y) = (LinearMap.transvection f v) x + (LinearMap.transvection f v) y

Tactic:
simp [map_add]

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

Goal state before:
pp: case refine_2
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
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) * ((ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2) *
        ((ι Q) m₂.1 + (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      (Q' Q) m₂ • ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)

Tactic:
mul_assoc (_ + _),

Goal state after:
case refine_2
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
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
        (((ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2) *
          ((ι Q) m₂.1 + (algebraMap R (CliffordAlgebra Q)) m₂.2)) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      (Q' Q) m₂ • ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)
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:
rw [← of_one, Algebra.TensorProduct.one_def, auxEquiv_tmul 𝒜 ℬ, DirectSum.decompose_one,
    DirectSum.decompose_one, Algebra.TensorProduct.one_def]

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)ˣ
⊢ ↑x ∈ Submonoid.map (Units.coeHom (CliffordAlgebra Q)) (lipschitzGroup Q).toSubmonoid ∧
      ↑x ∈ unitary (CliffordAlgebra Q) ↔
    x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)

Tactic:
lipschitzGroup.coe_mem_iff_mem

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)ˣ
⊢ x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q) ↔ x ∈ lipschitzGroup Q ∧ ↑x ∈ unitary (CliffordAlgebra Q)
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a.e_a
ι : 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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ {x | ¬∃ j, f j = x}.card = Fintype.card ι - n

pp: case e_a
ι : 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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ ∏ x ∈ {x | ∃ j, f j = x}.attach, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index

Tactic:
· convert! Finset.card_compl {x | ∃ j, f j = x} using 2
    · exact (Finset.compl_filter _).symm
    · convert! (Finset.card_image_of_injective Finset.univ f.injective).symm <;> simp

Goal state after:
case e_a
ι : 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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
⊢ ∏ x ∈ {x | ∃ j, f j = x}.attach, (Submodule.toAddSubgroup (Ideal.span {a ⋯.choose})).index =
    ∏ i, (Submodule.toAddSubgroup (Ideal.span {a i})).index
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ A.IsTotallyUnimodular

Tactic:
intro _

Goal state after:
case mpr
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
⊢ ∀ (f : Fin k✝ → m) (g : Fin k✝ → n),
    Function.Injective f → Function.Injective g → (A.submatrix f g).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f_1 : Fin k → m') (g_1 : Fin k → n'), (A.submatrix (f ∘ f_1) (g ∘ g_1)).det ∈ Set.range SignType.cast

Tactic:
intro _

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
⊢ ∀ (f_1 : Fin k✝ → m') (g_1 : Fin k✝ → n'), (A.submatrix (f ∘ f_1) (g ∘ g_1)).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f : Fin k → n) (g : Fin k → m), (A.submatrix g f).det ∈ Set.range SignType.cast

Tactic:
intro _

Goal state after:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
⊢ ∀ (f : Fin k✝ → n) (g : Fin k✝ → m), (A.submatrix g f).det ∈ Set.range SignType.cast
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case e_a.a
ι : 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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ ⋯.choose = i

Tactic:
rw [← f.injective.eq_iff]

Goal state after:
case e_a.a
ι : 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
hN' :
  N'.toAddSubgroup =
    AddSubgroup.pi Set.univ fun i ↦ Submodule.toAddSubgroup (Ideal.span {if h : ∃ j, f j = i then a h.choose else 0})
f' : Fin n → ↥{x | ∃ j, f j = x} := fun i ↦ ⟨f i, ⋯⟩
hf' : Function.Injective f'
f'' : Fin n ↪ ↥{x | ∃ j, f j = x} := { toFun := f', inj' := hf' }
hu : Finset.univ = Finset.map f'' Finset.univ
i : Fin n
a✝ : i ∈ Finset.univ
⊢ f ⋯.choose = f i
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
⊢ reduce A ∈ reps m

Tactic:
induction A using reduce_rec with
  | step A h1 h2 => simpa only [reduce_reduceStep h1] using h2
  | base A h =>
    have hd := A_d_ne_zero h hm
    by_cases h1 : 0 < A.1 0 0
    · simp only [reduce_of_pos h h1]
      have h2 := Int.emod_def (A.1 0 1) (A.1 1 1)
      have h4 := Int.ediv_mul_le (A.1 0 1) hd
      set n : ℤ := A.1 0 1 / A.1 1 1
      have h3 := Int.emod_lt_abs (A.1 0 1) hd
      rw [← abs_eq_self.mpr <| Int.emod_nonneg _ hd] at h3
      simp only [smul_def, coe_T_zpow]
      suffices A.1 1 0 = 0 ∧ n * A.1 1 0 < A.1 0 0 ∧
          n * A.1 1 1 ≤ A.1 0 1 ∧ |A.1 0 1 + -(n * A.1 1 1)| < |A.1 1 1| by
        simpa only [reps, Fin.isValue, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, empty_mul,
          Equiv.symm_apply_apply, Set.mem_ofPred_eq, of_apply, cons_val', vecMul, cons_dotProduct,
          vecHead, one_mul, vecTail, Function.comp_apply, Fin.succ_zero_eq_one, neg_mul,
          dotProduct_of_isEmpty, add_zero, zero_mul, zero_add, empty_val', cons_val_fin_one,
          cons_val_one, cons_val_zero, lt_add_neg_iff_add_lt, le_add_neg_iff_add_le]
      simp_all only [mul_comm n, zero_mul, ← sub_eq_add_neg, ← h2,
        Fin.isValue, and_true]
    · simp only [reps, Fin.isValue, reduce_of_not_pos h h1, Int.ediv_neg, neg_neg, smul_def, ←
        mul_assoc, S_mul_S_eq, neg_mul, one_mul, coe_T_zpow, mul_neg, cons_mul, Nat.succ_eq_add_one,
        Nat.reduceAdd, empty_mul, Equiv.symm_apply_apply, neg_of, neg_cons, neg_empty,
        Set.mem_ofPred_eq, of_apply, cons_val', Pi.neg_apply, vecMul, cons_dotProduct, vecHead,
        vecTail, Function.comp_apply, Fin.succ_zero_eq_one, h, mul_zero, dotProduct_of_isEmpty,
        add_zero, zero_mul, neg_zero, empty_val', cons_val_fin_one, cons_val_one, cons_val_zero,
        lt_neg, neg_add_rev, zero_add, le_add_neg_iff_add_le, ← le_neg, abs_neg, true_and]
      refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩
      · simp only [Int.lt_iff_le_and_ne]
        exact ⟨not_lt.mp h1, A_a_ne_zero h hm⟩
      · rw [mul_comm, add_comm, ← Int.sub_eq_add_neg, ← Int.emod_def,
         abs_eq_self.mpr <| Int.emod_nonneg _ hd]
        exact Int.emod_lt_abs _ hd

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible

Tactic:
by_cases hA_nonneg : ∀ i j, 0 ≤ A i j

Goal state after:
case pos
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ∀ (i j : n), 0 ≤ A i j
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible

case neg
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ Aᵀ.IsIrreducible ↔ A.IsIrreducible
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ ¬Aᵀ.IsIrreducible

Tactic:
rw [isIrreducible_iff]

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ ¬A.IsIrreducible

Tactic:
rw [isIrreducible_iff]

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ ¬((∀ (i j : n), 0 ≤ A i j) ∧ IsSStronglyConnected n)
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
⊢ IsRightRegular A ↔ A.Nonsingular

Tactic:
isRightRegular_iff_vecMul_injective,

Goal state after:
R : Type u_1
n : Type u_3
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Matrix n n R
inst✝ : IsCancelAdd R
⊢ (Function.Injective fun v ↦ v ᵥ* A) ↔ A.Nonsingular
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
M : SL(2, F)
x✝ : M ∈ ⊤
i j : Fin 2
hij : i ≠ j
a : F
⊢ SpecialLinearGroup.transvection hij a ∈ lineStab (F ∙ Pi.single 0 1) ⊔ lineStab (F ∙ Pi.single 1 1)

Tactic:
by simpa using transvection_mem_lineStab_sup ⟨i, j, hij, a⟩

Goal state after: