mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case pos
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
⊢ ∀ (a : Kˣ), ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'

Tactic:
intro a

Goal state after:
case pos
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : D ≠ D'
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
⊢ ∃ h, LinearEquiv.det h = a ∧ h • D = D ∧ h • D' = D'
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ 0 < (weightedSumSquares 𝕜 w) ↑⟨v, hv⟩

Tactic:
weightedSumSquares_apply

Goal state after:
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
hv' : ⟨v, hv⟩ ≠ 0
⊢ 0 < ∑ i, w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case zero
ι : 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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ 0 j (Sum.inl i) = 0

Tactic:
| zero =>

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✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ cartanSubalgebra b = LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)

Tactic:
refine le_antisymm LieSubalgebra.submodule_span_le_lieSpan ?_

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✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h) ≤ cartanSubalgebra b
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case zero
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
⊢ (e i ^ 0).col (Sum.inr j) = 0 ∨
    ∃ k x, P.root k = P.root j + 0 • P.root ↑i ∧ (e i ^ 0).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1

Tactic:
| zero =>

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

Goal state before:
pp: case mem
ι : 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
b : P.Base
inst✝ : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
i : ↥b.support
⊢ u i (Sum.inr j) = 0

Tactic:
simp [u]

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

Goal state before:
pp: case zero
ι : 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
b : P.Base
inst✝ : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
⊢ 0 (Sum.inr j) = 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
ι : 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 ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ (ωConj b) 0 ∈ lieAlgebra b

Tactic:
| zero =>

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✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
⊢ ωConjLieSubmodule N = ⊤ ↔ N = ⊤

Tactic:
rw [← LieSubmodule.toSubmodule_eq_top]

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✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
⊢ ↑(ωConjLieSubmodule N) = ⊤ ↔ N = ⊤
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝² : Module.IsReflexive R M
this✝¹ : IsAddTorsionFree M
this✝ : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
this : P.root k ≠ 2 • P.root ↑i
⊢ ∀ x ∈ Finset.univ, ¬(x = ↑i ∧ P.root k = P.root ↑i + P.root x)

Tactic:
by simpa [two_smul]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
k : ι
x : ℕ
hk₁ : P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i ∈ range ⇑P.root
⊢ P.root ↑i ≠ -P.root j

Tactic:
contrapose hij

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j k : ι
x : ℕ
hk₁ : P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i ∈ range ⇑P.root
hij : P.root ↑i = -P.root j
⊢ j = -↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case zero
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
⊢ ω b * f i ^ 0 = e i ^ 0 * ω b

Tactic:
| zero =>

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case zero
ι : 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
inst✝ : P.IsIrreducible
i : ι
hi : P.root i ∉ allRoots P
this✝ : Fintype ι
B : P.InvariantForm
h₂ : (B.form (P.root i)) (P.root (long P)) = 0
h₁ : (B.form (P.root i)) (P.root (short P)) = 0
this : Module.IsReflexive R M
x : M
⊢ (B.form (P.root i)) 0 = 0

Tactic:
| zero =>

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
hki : P.pairingIn ℤ k i = 0
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✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
key₃ : P.pairingIn ℤ j k = 2
key₄ : P.pairingIn ℤ l j = 1
⊢ (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)

Tactic:
replace key₄ : P.pairingIn ℤ j l ≠ 0 := by rw [ne_eq, P.pairingIn_eq_zero_iff]; lia

Goal state after:
ι : 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
hki : P.pairingIn ℤ k i = 0
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✝¹ : P.IsNotG2
this✝ : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn : P.root n = P.root k + P.root i - P.root j
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ P.root k ≠ -P.root j
hnk_notMem : P.root n - P.root k ∉ range ⇑P.root
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
key₃ : P.pairingIn ℤ j k = 2
key₄ : P.pairingIn ℤ j l ≠ 0
⊢ (chainBotCoeff i m + 1) * (chainBotCoeff j (-k) + 1) = (chainBotCoeff j (-l) + 1) * (chainBotCoeff i k + 1)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ h₀ i ∈ ↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))

Tactic:
rw [hef]

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ ⁅e₀ i, f₀ i⁆ ∈ ↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD J]
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ x ^ p ≡ y ^ p [SMOD J * I]

Tactic:
SModEq.sub_mem

Goal state after:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ x ^ p - y ^ p ∈ J * I
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
I : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD I]
⊢ x ^ p ^ 0 ≡ y ^ p ^ 0 [SMOD I ^ (0 + 1)]

Tactic:
| zero =>

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
A' : Type u_4
inst✝¹ : CommSemiring A'
inst✝ : Algebra R A'
h : IsSymmetricAlgebra f
F G : A →ₐ[R] A'
hFG : ↑F ∘ₗ f = ↑G ∘ₗ f
this : F.comp ↑h.equiv = G.comp ↑h.equiv
⊢ F = G

Tactic:
rw [DFunLike.ext'_iff] at this ⊢
    exact h.equiv.surjective.injective_comp_right this

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

Goal state before:
pp: n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this✝ : p ∣ (m - n) * a
this : p ∣ a
⊢ False

Tactic:
apply pp.ne_one

Goal state after:
n m a : ℕ
ha : m - n ∣ a
p : ℕ
pp : Prime p
hn : p ∣ n * a + 1
hm : p ∣ m * a + 1
this✝ : p ∣ (m - n) * a
this : p ∣ a
⊢ p = 1
Module: Mathlib.Logic.Hydra

Goal state before:
pp: case inl.refine_2
α : Type u_1
r : α → α → Prop
s₁ s₂ t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
he : (s₁ + s₂ + t).erase a + {a} = s₁ + s₂ + t
h : a ∈ s₁
⊢ (s₁.erase a + t, s₂).1 + (s₁.erase a + t, s₂).2 = (s₁ + s₂ + t).erase a

Tactic:
rw [add_assoc s₁, erase_add_left_pos _ h, add_right_comm, add_assoc]

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

Goal state before:
pp: case zero
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
h : finrank K (V ⧸ (↑e).fixedSubmodule) = 0
⊢ e ∈ transvections K V ^ (0 - 1) * dilatransvections K V

Tactic:
| zero =>

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

Goal state before:
pp: case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s}) ≤ MeasurableSpace.pi

pp: case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi ≤ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s})

Tactic:
· rw [MeasurableSpace.generateFrom_le_iff]
    rintro S ⟨s, t, h, rfl⟩
    simp only [mem_univ_pi, mem_ofPred_eq] at h
    exact MeasurableSet.pi (Finset.countable_toSet _) (fun i _ ↦ h i)

Goal state after:
case a
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ MeasurableSpace.pi ≤ generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s})
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case zero
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
⊢ ⋃ i, ⋃ (_ : i ≤ 0), s i ∈ C

Tactic:
| zero =>

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case zero
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
⊢ ⋂ i, ⋂ (_ : i ≤ 0), s i ∈ C

Tactic:
| zero =>

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case zero
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (i : ℕ), s i ∈ C
⊢ accumulate s 0 ∈ C

Tactic:
| zero =>

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
⊢ (↑{Set.Ioc u u', Set.Ioc v' v}).PairwiseDisjoint id

Tactic:
intro a

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Nonempty α
u v : α
huv : u ≤ v
u' v' : α
hu'v' : u' ≤ v'
hu : u < u'
hv : v' < v
a : Set α
⊢ a ∈ ↑{Set.Ioc u u', Set.Ioc v' v} →
    ∀ ⦃y : Set α⦄, y ∈ ↑{Set.Ioc u u', Set.Ioc v' v} → a ≠ y → Function.onFun Disjoint id a y
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.coe.refine_2
ι : 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 b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z)

Tactic:
apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind

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

Goal state before:
pp: case zero
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
he : ∀ (a : K), ∃ x, e.fixedReduce x ≠ a • x
h : finrank K (V ⧸ (↑e).fixedSubmodule) = 0
⊢ e ∈ transvections K V ^ (0 - 1) * dilatransvections K V

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
C : Set (Set α)
s t : Set α
I✝ : Finset (Set α)
G✝ : Type u_2
inst✝² : AddCommMonoid G✝
m m' : AddContent G✝ C
inst✝¹ : LinearOrder α
G : Type u_3
inst✝ : AddCommGroup G
f : α → G
I : Finset (Set α)
hI : ↑I ⊆ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
h'I : (↑I).PairwiseDisjoint id
h''I : ⋃₀ ↑I ∈ {s | ∃ u v, u ≤ v ∧ s = Set.Ioc u v}
hn : #I = 0
⊢ onIocAux f (⋃₀ ↑I) = ∑ u ∈ I, onIocAux f u

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
C : Set (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetRing C
s : ℕ → Set α
hs_disj : Pairwise (Disjoint on s)
hsC : ∀ (i : ℕ), s i ∈ C
⊢ m (accumulate s 0) = ∑ i ∈ Finset.range (0 + 1), m (s i)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
C : Set (Set α)
hC : IsSetRing C
m : AddContent ℝ≥0∞ C
hm_ne_top : ∀ s ∈ C, m s ≠ ∞
hm_tendsto : ∀ ⦃s : ℕ → Set α⦄, (∀ (n : ℕ), s n ∈ C) → Antitone s → ⋂ n, s n = ∅ → Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hUf : ⋃ i, f i ∈ C
h_disj : Pairwise (Disjoint on f)
s : ℕ → Set α := fun n ↦ (⋃ i, f i) \ accumulate f n
hCs : ∀ (n : ℕ), s n ∈ C
h_tendsto : Tendsto (fun n ↦ m (s n)) atTop (𝓝 0)
n : ℕ
⊢ m (s n) = m (⋃ i, f i) - ∑ i ∈ Finset.range (n + 1), m (f i)

Tactic:
rw [addContent_sdiff_of_ne_top m hC hm_ne_top hUf (hC.accumulate_mem hf n)
      (Set.accumulate_subset_iUnion _), addContent_accumulate m hC h_disj hf n]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), MeasurableSet i → v i = w i

Tactic:
constructor
  · rintro rfl _ _
    rfl
  · rw [DFunLike.ext_iff]
    intro h i
    by_cases hi : MeasurableSet i
    · exact h i hi
    · simp_rw [not_measurable _ hi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ HasSum (fun i ↦ v (f i)) (v (⋃ i, f i))

Tactic:
by
  rcases Countable.exists_injective_nat β with ⟨e, he⟩
  rw [← hasSum_extend_zero he]
  convert! m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _
  · simp only [Pi.zero_def, Function.apply_extend v, Function.comp_def, empty]
  · exact (iSup_extend_bot he _).symm
  · simp [Function.apply_extend MeasurableSet, Function.comp_def, hm]
  · exact hd.disjoint_extend_bot (he.factorsThrough _)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
this :
  ∀ (p : ℕ → Prop) {r : ℕ → ℝ},
    Tendsto r atTop (𝓝[>] 0) →
      blimsup (fun i ↦ cthickening (M * r i) (s i)) atTop p =ᵐ[μ] blimsup (fun i ↦ cthickening (r i) (s i)) atTop p
r' : ℕ → ℝ := fun i ↦ if 0 < r i then r i else 1 / (↑i + 1)
i : ℕ
hi : ¬0 < r i
⊢ r' i ∈ Ioi 0

Tactic:
simp only [r', hi, one_div, mem_Ioi, if_false, inv_pos]; positivity

Goal state after: