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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (ι (Q c₁ c₂)) (0, 1) * (ι (Q c₁ c₂)) (1, 0) = 0 • (ι (Q c₁ c₂)) (0, 1) - (ι (Q c₁ c₂)) (1, 0) * (ι (Q c₁ c₂)) (0, 1)

Tactic:
rw [zero_smul, zero_sub, eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) ((0, 1) + (1, 0)) - (Q c₁ c₂) (0, 1) - (Q c₁ c₂) (1, 0)) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Goal state before:
pp: R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
⊢ (ι Q') m = (ι Q') m - (contractLeft (B m)) 1

Tactic:
contractLeft_one,

Goal state after:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
m : M
⊢ (ι Q') m = (ι Q') m - 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m ∈ (ι (Q' Q)).range ^ 2

Tactic:
pow_two

Goal state after:
case refine_1.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (LinearMap.mulLeft R (e0 Q) ∘ₗ v Q) m ∈ (ι (Q' Q)).range * (ι (Q' Q)).range
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 ∈ lipschitzGroup Q
inst✝ : Invertible 2
this : ∀ x ∈ lipschitzGroup Q, ConjAct.toConjAct x • (ι Q).range ≤ (ι Q).range
⊢ ConjAct.toConjAct x • (ι Q).range = (ι Q).range

Tactic:
by
    apply le_antisymm
    · exact this _ hx
    · have := smul_mono_right (ConjAct.toConjAct x) <| this _ (inv_mem hx)
      refine Eq.trans_le ?_ this
      simp only [map_inv, smul_inv_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: 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)
x : N
⊢ x ∈ L.goursatSnd.toAddSubgroup ↔ x ∈ L.toAddSubgroup.goursatSnd

Tactic:
simp [goursatSnd, AddSubgroup.mem_goursatSnd]

Goal state after:
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: 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)
⊢ L.goursatFst.prod L.goursatSnd ≤ L

Tactic:
simpa only [← toAddSubgroup_le, goursatFst_toAddSubgroup, goursatSnd_toAddSubgroup]
    using! L.toAddSubgroup.goursatFst_prod_goursatSnd_le

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
h_inj : Injective v'
⊢ LinearIndependent L fun i ↦ ⇑(algebraMap K L) ∘ v i

Tactic:
← hv'

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
h_inj : Injective v'
⊢ LinearIndependent L (⇑b' ∘ v')
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ (M ^ p).charpoly = M.charpoly

Tactic:
have h := FiniteField.Matrix.charpoly_pow_card M

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).charpoly = M.charpoly
⊢ (M ^ p).charpoly = M.charpoly
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ : m
⊢ ∀ ⦃b : m⦄, i₁ < b → l i₁ ≤ l b

Tactic:
i₂

Goal state after:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : PartialOrder m
hA : A.IsPivotedBy l
i₁ i₂ : m
⊢ i₁ < i₂ → l i₁ ≤ l i₂
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ ↑(g • A) = ↑g * ↑A

Tactic:
by
  rw [smul_def]

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]
  induction k with
  | zero =>
      have : Unique { s : Fin 0 → V // (⊤ : Submodule K (Fin 0 →₀ K)) = ⊥ } :=
        uniqueOfSubsingleton ⟨0, Subsingleton.elim ..⟩
      simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
  | succ k ih =>
      have (s : { s : Fin k → V // LinearIndependent K s }) :
          card ((Submodule.span K (Set.range (s : Fin k → V)))ᶜ : Set (V)) =
          (q) ^ n - (q) ^ k := by
            rw [card_compl_set, Module.card_eq_pow_finrank (K := K)
            (V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]
            simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
            rw [Module.card_eq_pow_finrank (K := K)]
      simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk),
        mul_comm, Fin.prod_univ_succAbove _ (Fin.last k), -Set.fintypeCard_eq_ncard]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
⊢ (↑A.den)⁻¹ • A.num.map Int.cast = A

Tactic:
by
  ext
  simp [← Matrix.num_div_den A, div_eq_inv_mul]

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
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
c : n
p' : Path i c
e : c ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ False

Tactic:
obtain ⟨rfl⟩ : i = c := Quiver.Path.eq_of_length_zero p' (by simp_all)

Goal state after:
n : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
A : Matrix n n R
inst✝ : Nontrivial n
h_irr : A.IsIrreducible
i : n
this : Quiver n := A.toQuiver
h_row : ¬∃ j, 0 < A i j
no_out : ∀ (j : n), IsEmpty (i ⟶ j)
j : n
hij : ∃ y, j ≠ y
p : Path i j
hp_pos : 0 < p.length
h_le : 1 ≤ p.length
v : n
p₂ : Path v j
p' : Path i i
e : i ⟶ v
_hp_eq : p = (p'.cons e).comp p₂
hp₁_len : (p'.cons e).length = 1
hlen_ne : (p'.cons e).length ≠ 0
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case succ.mpr.nil
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i : n
hp_len : nil.length = m + 1
⊢ 0 < ∑ j, (A ^ m) i j * A j i

Tactic:
simp [Quiver.Path.length] at hp_len

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

Goal state before:
pp: α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
⊢ diagonal A.diag i j = A i j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Goal state after:
case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ diagonal A.diag i i = A i i

case inr
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ diagonal A.diag i j = A i j
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
i : ι
hpqi : p i ≠ q i
⊢ (fun i ↦ Pi.single (p i) (m i)) i (q i) = 0

Tactic:
simp_rw [Pi.single_eq_of_ne' hpqi]

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

Goal state before:
pp: case refine_1
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : SpecialLinearGroup ι F
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : ∀ (w : ι → F), ∃ b ∈ L, g • b = A • w - w
w v : ι → F
hv : v ∈ L
hvw : g • v = A • g • w - g • w
⊢ (g⁻¹ * A * g) • w - w ∈ L

Tactic:
simp_all [eq_comm (a := g • v), sub_eq_iff_eq_add, mul_smul]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case mpr
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
u : LinearMap.GeneralLinearGroup R V
hu : LinearEquiv.det u.toLinearEquiv = 1
⊢ u ∈ Set.range ⇑toGeneralLinearGroup

Tactic:
refine ⟨⟨u.toLinearEquiv, hu⟩, rfl⟩

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

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.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
this :
  ⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h =
    ⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i
⊢ b.cartanMatrixᵀ.det ≠ 0

Tactic:
Matrix.det_transpose,

Goal state after:
ι : 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.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : P.IsRootSystem
this :
  ⇑(Matrix.diagLinearMap (↥b.support ⊕ ι) R R) ∘ h =
    ⇑Sum.elimZeroLeft ∘ fun i ↦ ⇑(algebraMap ℤ R) ∘ fun x ↦ P.pairingIn ℤ x ↑i
⊢ b.cartanMatrix.det ≠ 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ cartanSubalgebra b ≤ lieAlgebra b

Tactic:
by
  rw [cartanSubalgebra, lieAlgebra, ← LieSubalgebra.toSubmodule_le_toSubmodule, Submodule.span_le]
  rintro - ⟨i, rfl⟩
  exact LieSubalgebra.subset_lieSpan <| Or.inl <| Or.inl <| mem_range_self i

Goal state after:
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
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
contra : P.root n = -P.root i
h₃ : 2 • P.root n = P.root m
⊢ False

Tactic:
exact P.nsmul_notMem_range_root ⟨_, h₃.symm⟩

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

Goal state before:
pp: 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
h : TensorAlgebra R M →ₐ[R] A
x✝¹ x✝ : TensorAlgebra R M
h'✝ : (symRingCon R M) x✝¹ x✝
x y : TensorAlgebra R M
h' : SymRel R M x y
⊢ (RingCon.ker h.toRingHom) x y

Tactic:
induction h' with | mul_comm x y
   =>  _ 

Goal state after:
case mul_comm
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
h : TensorAlgebra R M →ₐ[R] A
x✝² x✝¹ : TensorAlgebra R M
h' : (symRingCon R M) x✝² x✝¹
x✝ y✝ : TensorAlgebra R M
x y : M
⊢ (RingCon.ker h.toRingHom) ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)
    ((TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x)
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ IsSymmetricAlgebra (ι R M)

Tactic:
by
  rw [IsSymmetricAlgebra, lift_ι]
  exact Function.Involutive.bijective (congrFun rfl)

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

Goal state before:
pp: 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
⊢ motive a

Tactic:
rw [← h.equiv.right_inv a]
  generalize h.equiv.invFun a = y
  change motive (SymmetricAlgebra.lift f y)
  induction y using SymmetricAlgebra.induction with
  | algebraMap r => simpa using algebraMap r
  | ι y => simpa using ι y
  | mul _ _ hx hy => simpa using mul _ _ hx hy
  | add _ _ hx hy => simpa using add _ _ hx hy

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

Goal state before:
pp: m : ℕ
l : List ℕ
⊢ ∀ i ∈ Finset.univ, coprimes (fun x ↦ l[x]) i ≠ 0

Tactic:
simp [coprimes]

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

Goal state before:
pp: l : List ℕ
i : Fin l.length
⊢ ∀ i ∈ Finset.univ, coprimes (fun x ↦ l[x]) i ≠ 0

Tactic:
simp [coprimes]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hSC : s ∈ C ∧ ↑S ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
obtain ⟨hsC, hSC⟩ := hSC

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inr
ι : 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'
⊢ SecondCountableTopology (WithTop ι)

Tactic:
let x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀

Goal state after:
case inr
ι : 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₀
⊢ SecondCountableTopology (WithTop ι)
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_1
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∀ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, ∃ I t_1, I.Countable ∧ t = I.domRestrict ⁻¹' t_1

Tactic:
rintro - ⟨I, t, -, rfl⟩

Goal state after:
case refine_1
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Finset ι
t : (i : ι) → Set (α i)
⊢ ∃ I_1 t_1, I_1.Countable ∧ (↑I).pi t = I_1.domRestrict ⁻¹' t_1
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: case refine_2
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
⊢ ∀ (t : Set ((a : ι) → α a)),
    MeasurableSet t →
      (∃ I t_1, I.Countable ∧ t = I.domRestrict ⁻¹' t_1) → ∃ I t_1, I.Countable ∧ tᶜ = I.domRestrict ⁻¹' t_1

Tactic:
rintro - - ⟨I, t, hI, rfl⟩

Goal state after:
case refine_2
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : MeasurableSet s
I : Set ι
t : Set ((a : ↑I) → α ↑a)
hI : I.Countable
⊢ ∃ I_1 t_1, I_1.Countable ∧ (I.domRestrict ⁻¹' t)ᶜ = I_1.domRestrict ⁻¹' t_1
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 = ∅
this : Ioi x₁ = ∅
⊢ Ioi ↑x₁ ⊆ Ioi ↑a

Tactic:
simp [WithTop.Ioi_coe, this]

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m s - m t ≤ m (s \ t)

Tactic:
by
  conv_lhs => rw [← inter_union_sdiff s t]
  rw [addContent_union hC (hC.inter_mem hs ht) (hC.sdiff_mem hs ht) disjoint_inf_sdiff, add_comm]
  refine add_tsub_le_assoc.trans_eq ?_
  rw [tsub_eq_zero_of_le
    (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ.restrict E) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε

Tactic:
by
  obtain ⟨δ, hδ_pos, hδε⟩ := hf hε
  refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
  rw [μ.restrict_apply hs, ← measure_toMeasurable] at hμs
  calc
    eLpNorm (indicator s (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E)) := by
      rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
    _ ≤ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) :=
      eLpNorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl
    _ = eLpNorm (indicator (toMeasurable μ (s ∩ E)) (f i)) p μ :=
      (eLpNorm_indicator_eq_eLpNorm_restrict (measurableSet_toMeasurable _ _)).symm
    _ ≤ ENNReal.ofReal ε := hδε i _ (measurableSet_toMeasurable _ _) hμs

Goal state after:
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
s : ℕ → Set α
M : ℝ
hM : 0 < M
p : ℕ → Prop
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝[>] 0)
hr' : Tendsto (fun i ↦ M * r i) atTop (𝓝[>] 0)
⊢ blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p ≤ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p

Tactic:
exact blimsup_cthickening_ae_le_of_eventually_mul_le μ p (inv_pos.mpr hM) hr'
        (Eventually.of_forall fun i => by rw [inv_mul_cancel_left₀ hM.ne' (r i)])

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), v (s n) = v univ - v (s n)ᶜ
J : v (⋂ n, s n) = v univ - v (⋃ n, (s n)ᶜ)
⊢ Tendsto (fun n ↦ v univ - v (s n)ᶜ) atTop (𝓝 (v univ - v (⋃ n, (s n)ᶜ)))

Tactic:
apply tendsto_const_nhds.sub

Goal state after:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), v (s n) = v univ - v (s n)ᶜ
J : v (⋂ n, s n) = v univ - v (⋃ n, (s n)ᶜ)
⊢ Tendsto (fun x ↦ v (s x)ᶜ) atTop (𝓝 (v (⋃ n, (s n)ᶜ)))
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : ¬¬s ≤[i] 0
⊢ s.someExistsOneDivLT i ⊆ i

Tactic:
rw [someExistsOneDivLT, dif_neg hi]
    exact Set.empty_subset _

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Basic

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
x✝ : ℕ
⊢ (if MeasurableSet (f x✝) then v (f x✝ ∩ i) else 0) = v (f x✝ ∩ i)

Tactic:
if_pos (hf₁ _)

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
m mα : MeasurableSpace α
inst✝² : MeasurableSpace β
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v✝ v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
x✝ : ℕ
⊢ v (f x✝ ∩ i) = v (f x✝ ∩ i)