mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case hl
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₁
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m, 0))) = (ι (QuadraticMap.prod Q₁ Q₂)) (m, 0)

Tactic:
ofProd_ι_mk,

Goal state after:
case hl
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₁
⊢ (toProd Q₁ Q₂) ((ι Q₁) m ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) 0) = (ι (QuadraticMap.prod Q₁ Q₂)) (m, 0)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Goal state before:
pp: case hr
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (0, m))) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m)

Tactic:
ofProd_ι_mk,

Goal state after:
case hr
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ (toProd Q₁ Q₂) ((ι Q₁) 0 ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι Q₂) m) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m)
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst✝³ : LinearOrder I
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : Basis I R M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : ¬Disjoint ↑s ↑t
⊢ b.ExteriorAlgebra ↑s * b.ExteriorAlgebra ↑t = 0

Tactic:
simpa only [basis_apply_powersetCard] using ιMulti_family_mul_of_not_disjoint R b s t h

Goal state after:
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)) (toTensorAlgebra a)) (toTensorAlgebra b)

Tactic:
←
    LinearMap.compl₂_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: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : Fin i → M
b : Fin j → M
⊢ ((((((TensorProduct.mk R (⨂[R]^i M) (⨂[R]^j M)).compr₂ ↑mulEquiv).compr₂ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b =
    (((((LinearMap.mul R (TensorAlgebra R M)).compl₂ toTensorAlgebra ∘ₗ toTensorAlgebra).compMultilinearMap
              (PiTensorProduct.tprod R))
            a).compMultilinearMap
        (PiTensorProduct.tprod R))
      b

Tactic:
simp only [LinearMap.compMultilinearMap_apply, LinearMap.compr₂_apply, ← gMul_def,
    TensorProduct.mk_apply, LinearEquiv.coe_coe, tprod_mul_tprod, toTensorAlgebra_tprod,
    TensorAlgebra.tprod_apply, LinearMap.comp_apply, LinearMap.compl₂_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 : Fin i → M
b : Fin j → M
⊢ (List.ofFn fun i_1 ↦ (TensorAlgebra.ι R) (Fin.append a b i_1)).prod =
    ((LinearMap.mul R (TensorAlgebra R M)) (List.ofFn fun i ↦ (TensorAlgebra.ι R) (a i)).prod)
      (List.ofFn fun i ↦ (TensorAlgebra.ι R) (b i)).prod
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ M →ₗ[R] ⨁ (i : ℕ), ↥(⋀[R]^i M)

Tactic:
by apply GradedAlgebra.ι R M

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Fintype ι
inst✝¹ : Infinite R
inst✝ : Module R M
N : Submodule R M
snf : SmithNormalForm N ι n
⊢ N.toAddSubgroup.index = if n = Fintype.card ι then ∏ i, (Submodule.toAddSubgroup (Ideal.span {snf.a i})).index else 0

Tactic:
rw [snf.toAddSubgroup_index_eq_pow_mul_prod]
  split_ifs with h
  · simp [h]
  · have hlt : n < Fintype.card ι :=
      Ne.lt_of_le h (by simpa using Fintype.card_le_of_embedding snf.f)
    simp [hlt]

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

Goal state before:
pp: case e'_2
ι : Type u_1
inst✝ : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ Nonempty (↥H ≃+ (ι → ℤ)) ↔ Nonempty (↥(AddSubgroup.toIntSubmodule H) ≃ₗ[ℤ] ι → ℤ)

Tactic:
exact ⟨fun ⟨e⟩ ↦ ⟨e.toIntLinearEquiv⟩, fun ⟨e⟩ ↦ ⟨e.toAddEquiv⟩⟩

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
hk : k ≤ n
⊢ Nat.card { s // LinearIndependent K s } = ∏ i, (q ^ n - q ^ ↑i)

Tactic:
rw [Nat.card_eq_fintype_card]

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
hk : k ≤ n
⊢ card { s // LinearIndependent K s } = ∏ i, (q ^ n - q ^ ↑i)
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (T • B)
⊢ C (T⁻¹ • T • B)

Tactic:
← T_S_rel_smul

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (T • B)
⊢ C (S • S • S • T • S • T • S • T • B)
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
i j : n
p : Path i j
this : Quiver n := A.toQuiver
⊢ Path j i

Tactic:
induction p with
  | nil =>
    exact (@Quiver.Path.nil _ (toQuiver Aᵀ) _)
  | @cons b c q e ih =>
    have eT : 0 < (Aᵀ) c b := by
      simpa [Matrix.transpose_apply] using e.down
    exact (@Quiver.Path.comp n (toQuiver Aᵀ) c b i (@Quiver.Hom.toPath n (toQuiver Aᵀ) c b
      (PLift.up eT)) ih)

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

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = (mk K (ff i) ⋯).rep
⊢ LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)

Tactic:
convert! hh.units_smul a

Goal state after:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = (mk K (ff i) ⋯).rep
⊢ (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯) = a • ff
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg : g ∈ PSLAction.toPermHom.ker
⊢ g = 1

Tactic:
PSLAction.toPermHom,

Goal state after:
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
g : Matrix.ProjectiveSpecialLinearGroup ι K
hg :
  g ∈
    (QuotientGroup.lift (Subgroup.center (Matrix.SpecialLinearGroup ι K))
        (toPermHom (Matrix.SpecialLinearGroup ι K) (ℙ K (ι → K))) ⋯).ker
⊢ g = 1
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
⊢ P.pairingIn ℤ (twoShortAddLong P) i = 2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
rw [pairingIn_eq_add_of_root_eq_smul_add_smul (x := 2) (y := 1) (i := short P) (l := long P)]
  · simp
  · simp only [twoShortAddLongRoot_eq, one_smul, add_left_inj]
    norm_cast

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
⊢ genWeightSpace (↥b.support ⊕ ι → K) χ ≠ ⊥

Tactic:
contrapose hw₀

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw : w ∈ genWeightSpace (↥b.support ⊕ ι → K) χ
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
hw₀ : genWeightSpace (↥b.support ⊕ ι → K) χ = ⊥
⊢ w = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
hw : w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x
⊢ (w (Sum.inr i))⁻¹ • w = v b i

Tactic:
aux (Sum.elim 0 d) x rfl

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
hw : ∃ k, diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
⊢ (w (Sum.inr i))⁻¹ • w = v b i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
hki' : P.pairingIn ℤ k i < 0
hkj' : 0 < P.pairingIn ℤ k j
this✝³ : Module.IsReflexive R M := Module.IsReflexive.of_isPerfPair P.toLinearMap
him_mem : P.root i + P.root m ∈ range ⇑P.root
hjl_mem : P.root j + P.root (-l) ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
this✝² : InvolutiveNeg ι := P.indexNeg
this✝¹ : P.IsNotG2
this✝ : IsAddTorsionFree M
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hlj_mem : P.root l - P.root j ∈ range ⇑P.root
this : ¬(P.pairingIn ℤ m i = 0 ∧ P.pairingIn ℤ l j ≠ 0)
⊢ ¬(chainBotCoeff i m = 1 ∧ chainBotCoeff j (-l) = 0)

Tactic:
contrapose this
    rcases ne_or_eq (P.pairingIn ℤ m i) 0 with hmi | hmi
    · simpa [hmi, this.1, P.pairingIn_eq_zero_iff (i := i)] using chainBotCoeff_if_one_zero him_mem
    refine ⟨hmi, fun hlj ↦ ?_⟩
    rw [chainBotCoeff_if_one_zero hjl_mem] at this
    simp [P.pairingIn_eq_zero_iff (i := j), hlj] at this

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

Goal state before:
pp: case ι.ι
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ Commute ((ι R M) y) ((ι R M) x)

Tactic:
| ι y =>

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

Goal state before:
pp: case ι
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
ι : ∀ (x : M), motive (f x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
y : M
⊢ motive ((SymmetricAlgebra.lift f) ((SymmetricAlgebra.ι R M) y))

Tactic:
| ι y =>

Goal state after:
Module: Mathlib.LinearAlgebra.TensorPower.Symmetric

Goal state before:
pp: R ι : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Submodule.span R (Set.range ⇑(tprod R)) = ⊤

Tactic:
rw [tprod, LinearMap.coe_compMultilinearMap, Set.range_comp, Submodule.span_image,
    PiTensorProduct.span_tprod_eq_top, Submodule.map_top, range_mk]

Goal state after:
Module: Mathlib.Logic.Godel.GodelBetaFunction

Goal state before:
pp: m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < supOfSeq a
h₂ : supOfSeq a ≤ (↑i + 1) * (supOfSeq a)! + 1
⊢ a i < coprimes a i

Tactic:
simpa only [coprimes] using lt_of_lt_of_le h₁ h₂

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_1
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
⊢ (fun i ↦ t₁' i ∩ t₂' i) ∈ univ.pi C

Tactic:
rw [mem_univ_pi]

Goal state after:
case refine_1
ι : Type u_2
α : ι → Type u_1
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsPiSystem (C i)
hC_univ : ∀ (i : ι), univ ∈ C i
s₁ : Finset ι
t₁ : (i : ι) → Set (α i)
h₁ : t₁ ∈ univ.pi C
s₂ : Finset ι
t₂ : (i : ι) → Set (α i)
h₂ : t₂ ∈ univ.pi C
hst_nonempty : ((↑s₁).pi t₁ ∩ (↑s₂).pi t₂).Nonempty
t₁' : (i : ι) → Set (α i) := s₁.piecewise t₁ fun i ↦ univ
t₂' : (i : ι) → Set (α i) := s₂.piecewise t₂ fun i ↦ univ
h1 : ∀ i ∈ ↑s₁, t₁ i = t₁' i
h1' : ∀ i ∉ ↑s₁, t₁' i = univ
h2 : ∀ i ∈ ↑s₂, t₂ i = t₂' i
h2' : ∀ i ∉ ↑s₂, t₂' i = univ
⊢ ∀ (i : ι), t₁' i ∩ t₂' i ∈ C i
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : ↥I) → α ↑i)
hs : MeasurableSet s
⊢ (Measure.map I.restrict μ) s = (P I) s

pp: ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : ↥I) → α ↑i)
hs : MeasurableSet s
⊢ Measurable I.restrict

Tactic:
h I

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : ↥I) → α ↑i)
hs : MeasurableSet s
⊢ (P I) s = (P I) s

ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
μ : Measure ((i : ι) → α i)
h : IsProjectiveLimit μ P
I : Finset ι
s : Set ((i : ↥I) → α ↑i)
hs : MeasurableSet s
⊢ Measurable I.restrict
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
hu : LinearIndependent K ![(↑e).fixedSubmodule.mkQ u, e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
f : Dual K V
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
v_def : v = (f u)⁻¹ • u
hspan : K ∙ (e v - v) = K ∙ (e u - u)
⊢ LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]

Tactic:
← LinearIndependent.pair_smul_smul_iff (Ne.isUnit hfu).inv (Ne.isUnit hfu).inv

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
u : V
f : Dual K V
hu : LinearIndependent K ![(f u)⁻¹ • (↑e).fixedSubmodule.mkQ u, (f u)⁻¹ • e.fixedReduce ((↑e).fixedSubmodule.mkQ u)]
hfu : f u ≠ 0
v : V := (f u)⁻¹ • u
hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ ker f
v_def : v = (f u)⁻¹ • u
hspan : K ∙ (e v - v) = K ∙ (e u - u)
⊢ LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)]
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case compl.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
a : Set (Set α)
ha : a ∈ {x | ∃ f, {x | ∃ a, (↑(f a))ᶜ = x} = x}
t : Set α
ht : t ∈ a
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
rcases ha with ⟨f, rfl⟩

Goal state after:
case compl.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
t : Set α
f : (a : ↑A) → ↑↑a
ht : t ∈ {x | ∃ a, (↑(f a))ᶜ = x}
⊢ t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.top.inl.refine_1
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
hb : ⊤ ∈ Ioi ↑a
ha : Ioi a = ∅
⊢ Ioi ↑x₁ ⊆ Ioi ↑a

Tactic:
have : Ioi x₁ = ∅ := by
              have h : ∃ x, Ioi x = ∅ := ⟨a, ha⟩
              simp only [x₁, h, ↓reduceDIte]
              exact h.choose_spec
            simp [WithTop.Ioi_coe, this]

Goal state after:
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case compl
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
u_ind : ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ u = ⋃ a ∈ A, ⋂ t ∈ a, t
⊢ ∃ A, A.Finite ∧ (∀ a ∈ A, a.Finite) ∧ (∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜) ∧ uᶜ = ⋃ a ∈ A, ⋂ t ∈ a, t

Tactic:
| compl u _ u_ind =>

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case refine_2
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
t : Set α
ht : ∃ x ∈ ↑I, f x = t
i : ℕ
left✝ : i ∈ ↑I
hst : f i ≠ t
⊢ (Disjoint on id) (f i) t

Tactic:
obtain ⟨j, _, rfl⟩ := ht

Goal state after:
case refine_2
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
I : Finset ℕ
i : ℕ
left✝¹ : i ∈ ↑I
j : ℕ
left✝ : j ∈ ↑I
hst : f i ≠ f j
⊢ (Disjoint on id) (f i) (f j)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetSemiring C
m_subadd :
  ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Disjoint on f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ i, f i ∈ C
hf_disj : Pairwise (Disjoint on f)
⊢ m (⋃ i, f i) = ∑' (i : ℕ), m (f i)

Tactic:
by
  refine le_antisymm (m_subadd f hf hf_Union hf_disj) ?_
  refine ENNReal.summable.tsum_le_of_sum_le fun I ↦ ?_
  rw [← Finset.sum_image_of_disjoint addContent_empty (hf_disj.pairwiseDisjoint _)]
  refine sum_addContent_le_of_subset hC (I := I.image f) ?_ ?_ hf_Union ?_
  · simp only [coe_image, Set.image_subset_iff]
    refine (subset_preimage_image f I).trans (preimage_mono ?_)
    rintro i ⟨j, _, rfl⟩
    exact hf j
  · simp only [coe_image]
    intro s hs t ht hst
    rw [Set.mem_image] at hs ht
    obtain ⟨i, _, rfl⟩ := hs
    obtain ⟨j, _, rfl⟩ := ht
    have hij : i ≠ j := by intro h_eq; rw [h_eq] at hst; exact hst rfl
    exact hf_disj hij
  · simp only [Finset.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    exact fun i _ ↦ subset_iUnion _ i

Goal state after: