harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem Integrable.withDensityᵥ_trim_absolutelyContinuous {m m0 : MeasurableSpace α} {μ : Measure α}
    (hm : m ≤ m0) (hfi : Integrable f μ) :
    (μ.withDensityᵥ f).trim hm ≪ᵥ (μ.trim hm).toENNRealVectorMeasure

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑(μ.trim hm).toENNRealVectorMeasure j = 0
⊢ ↑((μ.withDensityᵥ f).trim hm) j = 0

Tactic:
rw [Measure.toENNRealVectorMeasure_apply_measurable hj₁, trim_measurableSet_eq hm hj₁] at hj₂

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ↑((μ.withDensityᵥ f).trim hm) j = 0

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ∫ (x : α) in j, f x ∂μ = 0

Tactic:
simp only [Measure.restrict_eq_zero.mpr hj₂, integral_zero_measure]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ↑((μ.withDensityᵥ f).trim hm) j = 0

Tactic:
rw [VectorMeasure.trim_measurableSet_eq hm hj₁, withDensityᵥ_apply hfi (hm _ hj₁)]

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : μ j = 0
⊢ ∫ (x : α) in j, f x ∂μ = 0

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
⊢ (μ.withDensityᵥ f).trim hm ≪ᵥ (μ.trim hm).toENNRealVectorMeasure

Tactic:
refine VectorMeasure.AbsolutelyContinuous.mk fun j hj₁ hj₂ => ?_

Result:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f μ
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑(μ.trim hm).toENNRealVectorMeasure j = 0
⊢ ↑((μ.withDensityᵥ f).trim hm) j = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_of_mem {a} {l : Vector α n} (h : a ∈ l) : ∃ (i : Nat) (h : i < n), l[i]'h = a

Proof state:
case mk
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ ∃ i h, { toArray := l, size_toArray := ⋯ }[i] = a

Tactic:
simpa using Array.getElem_of_mem (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ a ∈ l

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
h : a ∈ l
⊢ ∃ i h, l[i] = a

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ ∃ i h, { toArray := l, size_toArray := ⋯ }[i] = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_beq_to_not_eq (a b : Bool) : (!(a == b)) = ¬(a = b)

Proof state:
a b : Bool
⊢ ((!a == b) = true) = ¬a = b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_map (f : α → β) (g : β → Option γ) (l : Array α) :
    filterMap g (map f l) = filterMap (g ∘ f) l

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Option γ
l : Array α
⊢ filterMap g (map f l) = filterMap (g ∘ f) l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Option γ
toList✝ : List α
⊢ filterMap g (map f { toList := toList✝ }) = filterMap (g ∘ f) { toList := toList✝ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Option γ
toList✝ : List α
⊢ filterMap g (map f { toList := toList✝ }) = filterMap (g ∘ f) { toList := toList✝ }

Tactic:
simp [List.filterMap_map]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma smallHomMap_comp (f : SmallHom.{w} W₁ X Y) (g : SmallHom.{w} W₁ Y Z) :
    Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)

Proof state:
C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁵ : HasSmallLocalizedHom W₁ X Y
inst✝⁴ : HasSmallLocalizedHom W₁ Y Z
inst✝³ : HasSmallLocalizedHom W₁ X Z
inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Φ.smallHomMap (f.comp g) = (Φ.smallHomMap f).comp (Φ.smallHomMap g)

Tactic:
apply (SmallHom.equiv W₂ W₂.Q).injective

Result:
case a
C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁵ : HasSmallLocalizedHom W₁ X Y
inst✝⁴ : HasSmallLocalizedHom W₁ Y Z
inst✝³ : HasSmallLocalizedHom W₁ X Z
inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ (SmallHom.equiv W₂ W₂.Q) (Φ.smallHomMap (f.comp g)) =
    (SmallHom.equiv W₂ W₂.Q) ((Φ.smallHomMap f).comp (Φ.smallHomMap g))

Proof state:
case a
C₁ : Type u₁
inst✝⁷ : Category.{v₁, u₁} C₁
W₁ : MorphismProperty C₁
C₂ : Type u₂
inst✝⁶ : Category.{v₂, u₂} C₂
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst✝⁵ : HasSmallLocalizedHom W₁ X Y
inst✝⁴ : HasSmallLocalizedHom W₁ Y Z
inst✝³ : HasSmallLocalizedHom W₁ X Z
inst✝² : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)
inst✝¹ : HasSmallLocalizedHom W₂ (Φ.functor.obj Y) (Φ.functor.obj Z)
inst✝ : HasSmallLocalizedHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ (SmallHom.equiv W₂ W₂.Q) (Φ.smallHomMap (f.comp g)) =
    (SmallHom.equiv W₂ W₂.Q) ((Φ.smallHomMap f).comp (Φ.smallHomMap g))

Tactic:
simp [Φ.equiv_smallHomMap W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) (CatCommSq.iso _ _ _ _),
  SmallHom.equiv_comp]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean
lemma mem_ker {x : R} : x ∈ ker f ↔ f x = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
x : R
⊢ x ∈ ker f ↔ f x = 0

Tactic:
rw [mem_iff, ker_ringCon, map_zero]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_inv_intCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMonoid α]
    [Module R α] (c : ℤ) (M : Matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), ((↑c)⁻¹ • M)ᴴ i j = ((↑c)⁻¹ • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_union_eq (s t : Set α) :
    ae (μ.restrict (s ∪ t)) = ae (μ.restrict s) ⊔ ae (μ.restrict t)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ ae (μ.restrict (s ∪ t)) = ae (μ.restrict s) ⊔ ae (μ.restrict t)

Tactic:
simp [union_eq_iUnion, iSup_bool_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ico_add_one_add_one_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) :
    Ico (a + 1) (b + 1) = Ioc a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (a + 1) (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc_of_not_isMax hb a

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem append_take_drop : ∀ (n : ℕ) (s : Stream' α),
    appendStream' (take n s) (drop n s) = s

Proof state:
case zero
α : Type u
⊢ ∀ (s : Stream' α), take 0 s ++ₛ drop 0 s = s

Tactic:
intro s

Result:
case zero
α : Type u
s : Stream' α
⊢ take 0 s ++ₛ drop 0 s = s

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
⊢ ∀ (s : Stream' α), take (n' + 1) s ++ₛ drop (n' + 1) s = s

Tactic:
intro s

Result:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
s : Stream' α
⊢ take (n' + 1) s ++ₛ drop (n' + 1) s = s

Proof state:
α : Type u
⊢ ∀ (n : ℕ) (s : Stream' α), take n s ++ₛ drop n s = s

Tactic:
intro n

Result:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), take n s ++ₛ drop n s = s

Proof state:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), take n s ++ₛ drop n s = s

Tactic:
induction' n with n' ih

Result:
case zero
α : Type u
⊢ ∀ (s : Stream' α), take 0 s ++ₛ drop 0 s = s

case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
⊢ ∀ (s : Stream' α), take (n' + 1) s ++ₛ drop (n' + 1) s = s

Proof state:
case zero
α : Type u
s : Stream' α
⊢ take 0 s ++ₛ drop 0 s = s

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), take n' s ++ₛ drop n' s = s
s : Stream' α
⊢ take (n' + 1) s ++ₛ drop (n' + 1) s = s

Tactic:
rw [take_succ, drop_succ, cons_append_stream, ih (tail s), Stream'.eta]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem mul_add_swap_eq_polar_of_forall_mul_self_eq {A : Type*} [Ring A] [Algebra R A]
    (f : M →ₗ[R] A) (hf : ∀ x, f x * f x = algebraMap _ _ (Q x)) (a b : M) :
    f a * f b + f b * f a = algebraMap R _ (QuadraticMap.polar Q a b) :=
  calc
    f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f a * f a + f b * f a + (f a * f b + f b * f b) - f a * f a - f b * f b

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b) =
    (algebraMap R A) (Q (a + b) - Q a - Q b)

Tactic:
rw [← RingHom.map_sub, ← RingHom.map_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b

Tactic:
rw [f.map_add, mul_add, add_mul, add_mul]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f a * f b + f b * f a = f a * f a + f b * f a + (f a * f b + f b * f b) - f a * f a - f b * f b

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra R A
f : M →ₗ[R] A
hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)
a b : M
⊢ f (a + b) * f (a + b) - f a * f a - f b * f b =
    (algebraMap R A) (Q (a + b)) - (algebraMap R A) (Q a) - (algebraMap R A) (Q b)

Tactic:
rw [hf, hf, hf]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableAt_comp_add_right (a : E) :
    DifferentiableAt 𝕜 (fun x ↦ f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x a : E
⊢ DifferentiableAt 𝕜 (fun x => f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a)

Tactic:
simp [DifferentiableAt, hasFDerivAt_comp_add_right]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem support_esymm [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support =
    (powersetCard n (univ : Finset σ)).image fun t => ∑ i ∈ t, Finsupp.single i 1

Proof state:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (esymm σ R n).support = image (fun t => ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)

Tactic:
rw [support_esymm']

Result:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ ((powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}) =
    image (fun t => ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)

Proof state:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ ((powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}) =
    image (fun t => ∑ i ∈ t, Finsupp.single i 1) (powersetCard n univ)

Tactic:
exact biUnion_singleton

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
private lemma prop_red_T (hS : ∀ B, C B → C (S • B)) (hT : ∀ B, C B → C (T • B)) (B) :
    C (T • B) ↔ C B

Proof state:
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
⊢ C (T • B) ↔ C B

Tactic:
refine ⟨?_, hT _⟩

Result:
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
⊢ C (T • B) → C B

Proof state:
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
⊢ C (T • B) → C B

Tactic:
intro ih

Result:
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 B

Proof state:
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)

Tactic:
solve_by_elim (config := {maxDepth := 10})

Result:
no goals

Proof state:
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)
⊢ B = T⁻¹ • T • B

Tactic:
simp

Result:
no goals

Proof state:
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 B

Tactic:
rw [show B = T⁻¹ • T • B by simp, ← T_S_rel_smul]

Result:
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)
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem mem_cocompact_of_closedBall_compl_subset [ProperSpace α] (c : α)
    (h : ∃ r, (closedBall c r)ᶜ ⊆ s) : s ∈ cocompact α

Proof state:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α

Tactic:
rw [Filter.mem_cocompact]

Result:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Proof state:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ ∃ t, IsCompact t ∧ tᶜ ⊆ s

Tactic:
exact ⟨closedBall c r, isCompact_closedBall c r, h⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
c : α
h : ∃ r, (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α

Tactic:
rcases h with ⟨r, h⟩

Result:
case intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ s ∈ cocompact α
-- Mathlib/Topology/Maps/Basic.lean
theorem IsOpenEmbedding.of_continuous_injective_isOpenMap
    (h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsOpenMap f) : IsOpenEmbedding f

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ IsOpenEmbedding f

Tactic:
simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, isInducing_iff_nhds, *,
  and_true]

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))

Tactic:
exact fun x =>
  le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem boxProd_neighborFinset (x : α × β)
    [Fintype (G.neighborSet x.1)] [Fintype (H.neighborSet x.2)] [Fintype ((G □ H).neighborSet x)] :
    (G □ H).neighborFinset x =
      (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2)
        (Finset.disjoint_product.mpr <| Or.inl <| neighborFinset_disjoint_singleton _ _)

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
this : Fintype ↑((G □ H).neighborSet x) := boxProdFintypeNeighborSet x
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯

Tactic:
convert_to (G □ H).neighborFinset x = _ using 2

Result:
case convert_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
this : Fintype ↑((G □ H).neighborSet x) := boxProdFintypeNeighborSet x
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯

Proof state:
case convert_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
this : Fintype ↑((G □ H).neighborSet x) := boxProdFintypeNeighborSet x
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯

Tactic:
exact Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯

Tactic:
letI : Fintype ((G □ H).neighborSet x) := SimpleGraph.boxProdFintypeNeighborSet _

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
this : Fintype ↑((G □ H).neighborSet x) := boxProdFintypeNeighborSet x
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma Monic.supDegree_mul
    (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2)
    (hbot : (⊥ : B) + ⊥ = ⊥) (hp : p.Monic D) (hq : q.Monic D) :
    (p * q).supDegree D = p.supDegree D + q.supDegree D

Proof state:
case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
exact hq.supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

case inr
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Proof state:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
h✝ : Subsingleton R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem triangle_succ (n : ℕ) : (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

Proof state:
case H
n : ℕ
⊢ 0 < 2

Tactic:
apply zero_lt_succ

Result:
no goals

Proof state:
n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n

Tactic:
rw [← add_mul_div_left, Nat.mul_comm 2 n, ← Nat.mul_add, Nat.add_sub_cancel, Nat.mul_comm]

Result:
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2

Proof state:
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2

case H
n : ℕ
⊢ 0 < 2

Tactic:
cases n <;> rfl

Result:
case H
n : ℕ
⊢ 0 < 2