harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem degree_lt_card_verts [DecidableRel G.Adj] (v : V) : G.degree v < Fintype.card V

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.degree v < Fintype.card V

Tactic:
apply Finset.card_lt_card

Result:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.neighborFinset v ⊂ univ

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.degree v < Fintype.card V

Tactic:
classical
apply Finset.card_lt_card
rw [Finset.ssubset_iff]
exact ⟨v, by simp, Finset.subset_univ _⟩

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ v ∉ G.neighborFinset v

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.neighborFinset v ⊂ univ

Tactic:
rw [Finset.ssubset_iff]

Result:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ ∃ a ∉ G.neighborFinset v, insert a (G.neighborFinset v) ⊆ univ

Proof state:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ ∃ a ∉ G.neighborFinset v, insert a (G.neighborFinset v) ⊆ univ

Tactic:
exact ⟨v, by simp, Finset.subset_univ _⟩

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Canonical.lean
theorem sq_tsub_sq (a b : α) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : AddLeftReflectLE α
a b : α
⊢ a ^ 2 - b ^ 2 = (a + b) * (a - b)

Tactic:
rw [sq, sq, mul_self_tsub_mul_self]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[simp]
lemma RightHomologyData.homologyIso_rightHomologyData [S.HasHomology] :
    S.rightHomologyData.homologyIso = S.rightHomologyIso.symm

Proof state:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyData.homologyIso.hom = S.rightHomologyIso.symm.hom

Tactic:
dsimp [homologyIso, rightHomologyIso]

Result:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyIso.inv ≫ rightHomologyMap' (𝟙 S) S.rightHomologyData S.rightHomologyData = S.rightHomologyIso.inv

Proof state:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyIso.inv ≫ rightHomologyMap' (𝟙 S) S.rightHomologyData S.rightHomologyData = S.rightHomologyIso.inv

Tactic:
erw [rightHomologyMap'_id, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyData.homologyIso = S.rightHomologyIso.symm

Tactic:
ext

Result:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyData.homologyIso.hom = S.rightHomologyIso.symm.hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∉ l₁) :
    (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a)

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₂ : Array α
l₁ : List α
h : ¬a ∈ { toList := l₁ }
⊢ ({ toList := l₁ } ++ l₂).erase a = { toList := l₁ } ++ l₂.erase a

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ { toList := l₁ }
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).erase a = { toList := l₁ } ++ { toList := l₂ }.erase a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ { toList := l₁ }
l₂ : List α
⊢ ¬a ∈ l₁

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ : List α
h : ¬a ∈ { toList := l₁ }
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).erase a = { toList := l₁ } ++ { toList := l₂ }.erase a

Tactic:
simpa using List.erase_append_right l₂ (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : Array α
h : ¬a ∈ l₁
⊢ (l₁ ++ l₂).erase a = l₁ ++ l₂.erase a

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₂ : Array α
l₁ : List α
h : ¬a ∈ { toList := l₁ }
⊢ ({ toList := l₁ } ++ l₂).erase a = { toList := l₁ } ++ l₂.erase a
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_comp_const_add {a b : 𝕜} :
    DifferentiableAt 𝕜 (fun x ↦ f (b + x)) a ↔ DifferentiableAt 𝕜 f (b + a)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b + x)) a
⊢ DifferentiableAt ?m.63302 ?m.62771 (-b + id (b + a))

Tactic:
simpa

Result:
no goals

Proof state:
case h.e'_11
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b + x)) a
⊢ f = (fun x => f (b + x)) ∘ fun y => -b + id y

Tactic:
ext

Result:
case h.e'_11.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b + x)) a
x✝ : 𝕜
⊢ f x✝ = ((fun x => f (b + x)) ∘ fun y => -b + id y) x✝

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 (fun x => f (b + x)) a ↔ DifferentiableAt 𝕜 f (b + a)

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.comp _ (differentiable_id.const_add _).differentiableAt⟩

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b + x)) a
⊢ DifferentiableAt 𝕜 f (b + a)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b + x)) a
⊢ DifferentiableAt 𝕜 f (b + a)

Tactic:
convert DifferentiableAt.comp (b + a) (by simpa)
  (differentiable_id.const_add (-b)).differentiableAt

Result:
case h.e'_11
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b + x)) a
⊢ f = (fun x => f (b + x)) ∘ fun y => -b + id y

Proof state:
case h.e'_11.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b + x)) a
x✝ : 𝕜
⊢ f x✝ = ((fun x => f (b + x)) ∘ fun y => -b + id y) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma ih1 (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) : IH1 x y

Proof state:
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
⊢ IH1 x y

Tactic:
rintro x₁ x₂ y' h₁ h₂ (rfl|hy) <;> apply ih (Args.P24 _ _ _)

Result:
case inl
x x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y') → P124 a
⊢ ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y')

case inr
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
hy : y'.IsOption y
⊢ ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y)

Proof state:
case inr
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
hy : y'.IsOption y
⊢ ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y)

Tactic:
refine TransGen.tail ?_ (cutExpand_pair_right hy)

Result:
case inr
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
hy : y'.IsOption y
⊢ TransGen (CutExpand IsOption) (Args.P24 x₁ x₂ y').toMultiset {x, y'}

Proof state:
case inr
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
hy : y'.IsOption y
⊢ TransGen (CutExpand IsOption) (Args.P24 x₁ x₂ y').toMultiset {x, y'}

Tactic:
exact TransGen.single (cutExpand_double_left h₁ h₂)

Result:
no goals

Proof state:
case inl
x x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y') → P124 a
⊢ ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y')

case inr
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
hy : y'.IsOption y
⊢ ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y)

Tactic:
on_goal 2 => refine TransGen.tail ?_ (cutExpand_pair_right hy)

Result:
case inl
x x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y') → P124 a
⊢ ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y')

case inr
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
hy : y'.IsOption y
⊢ TransGen (CutExpand IsOption) (Args.P24 x₁ x₂ y').toMultiset {x, y'}

Proof state:
case inl
x x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y') → P124 a
⊢ ArgsRel (Args.P24 x₁ x₂ y') (Args.P1 x y')

case inr
x y : PGame
ih : ∀ (a : Args), ArgsRel a (Args.P1 x y) → P124 a
x₁ x₂ y' : PGame
h₁ : x₁.IsOption x
h₂ : x₂.IsOption x
hy : y'.IsOption y
⊢ TransGen (CutExpand IsOption) (Args.P24 x₁ x₂ y').toMultiset {x, y'}

Tactic:
all_goals exact TransGen.single (cutExpand_double_left h₁ h₂)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma zpow_one_sub_natCast₀ (ha : a ≠ 0) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (1 - ↑n) = a / a ^ n

Tactic:
simpa using zpow_sub₀ ha 1 n

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.sin (o.oangle y (y - x)) * ‖y - x‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).sin * ‖y - x‖ = ‖x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_sub_mul_norm_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem linearIndependent_rows_iff_isUnit {A : Matrix m m K} :
    LinearIndependent K (fun i ↦ A i) ↔ IsUnit A

Proof state:
m : Type u
inst✝² : DecidableEq m
K : Type u_3
inst✝¹ : Field K
inst✝ : Fintype m
A : Matrix m m K
⊢ (LinearIndependent K fun i => A i) ↔ IsUnit A

Tactic:
rw [← transpose_transpose A, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,
  transpose_transpose, ← vecMul_injective_iff_isUnit, coe_vecMulLinear]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem lift_word_prod_nontrivial_of_head_card {i j} (w : NeWord H i j)
    (hcard : 3 ≤ #(H i)) (hheadtail : i ≠ j) : lift f w.prod ≠ 1

Proof state:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
hw' : (lift f) w'.prod ≠ 1
⊢ (lift f) w.prod ≠ 1

Tactic:
intro heq1

Result:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
hw' : (lift f) w'.prod ≠ 1
heq1 : (lift f) w.prod = 1
⊢ False

Proof state:
case intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
hnot1 : h * w.head ≠ 1
w' : NeWord H i i := (w.mulHead h hnot1).append ⋯ (NeWord.singleton h⁻¹ ⋯)
hw' : (lift f) w'.prod ≠ 1
heq1 : (lift f) w.prod = 1
⊢ (lift f) w'.prod = 1

Tactic:
simp [w', heq1]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem w_support {D : ℝ} (Dpos : 0 < D) : support (w D : E → ℝ) = ball 0 D

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
B : D • ball 0 1 = ball 0 D
⊢ ¬D ^ finrank ℝ E = 0

Tactic:
exact pow_ne_zero _ Dpos.ne'

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
B : D • ball 0 1 = ball 0 D
⊢ support (w D) = ball 0 D

Tactic:
have C : D ^ finrank ℝ E ≠ 0 := by
  norm_cast
  exact pow_ne_zero _ Dpos.ne'

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
B : D • ball 0 1 = ball 0 D
C : D ^ finrank ℝ E ≠ 0
⊢ support (w D) = ball 0 D

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
B : D • ball 0 1 = ball 0 D
C : D ^ finrank ℝ E ≠ 0
⊢ support (w D) = ball 0 D

Tactic:
simp only [w_def, Algebra.id.smul_eq_mul, support_mul, support_inv, univ_inter,
  support_comp_inv_smul₀ Dpos.ne', u_support, B, support_const (u_int_pos E).ne', support_const C,
  abs_of_nonneg Dpos.le]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
B : D • ball 0 1 = ball 0 D
⊢ D ^ finrank ℝ E ≠ 0

Tactic:
norm_cast

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
B : D • ball 0 1 = ball 0 D
⊢ ¬D ^ finrank ℝ E = 0

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ support (w D) = ball 0 D

Tactic:
have B : D • ball (0 : E) 1 = ball 0 D := by
  rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
B : D • ball 0 1 = ball 0 D
⊢ support (w D) = ball 0 D

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ D • ball 0 1 = ball 0 D

Tactic:
rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/EpiWithInjectiveKernel.lean
lemma epiWithInjectiveKernel_of_iso {X Y : C} (f : X ⟶ Y) [IsIso f] :
    epiWithInjectiveKernel f

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ epiWithInjectiveKernel f

Tactic:
rw [epiWithInjectiveKernel_iff]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ ∃ I, ∃ (_ : Injective I), ∃ f_1, ∃ (w : f_1 ≫ f = 0), Nonempty (ShortComplex.mk f_1 f w).Splitting

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso (ShortComplex.mk 0 f ⋯).g

Tactic:
dsimp

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso f

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ ∃ I, ∃ (_ : Injective I), ∃ f_1, ∃ (w : f_1 ≫ f = 0), Nonempty (ShortComplex.mk f_1 f w).Splitting

Tactic:
exact ⟨0, inferInstance, 0, by simp,
  ⟨ShortComplex.Splitting.ofIsZeroOfIsIso _ (isZero_zero C) (by dsimp; infer_instance)⟩⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ 0 ≫ f = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso f

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma isSquare_prod {s : Finset ι} [CommMonoid α] (f : ι → α)
    (h : ∀ c ∈ s, IsSquare (f c)) : IsSquare (∏ i ∈ s, f i)

Proof state:
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ IsSquare (∏ i ∈ s, f i)

Tactic:
rw [isSquare_iff_exists_sq]

Result:
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∃ r, ∏ i ∈ s, f i = r ^ 2

Proof state:
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∃ r, ∏ i ∈ s, f i = r ^ 2

Tactic:
use (∏ (x : s), ((isSquare_iff_exists_sq _).mp (h _ x.2)).choose)

Result:
case h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = (∏ x : { x // x ∈ s }, ⋯.choose) ^ 2

Proof state:
case h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i ∈ s, f i = (∏ x : { x // x ∈ s }, ⋯.choose) ^ 2

Tactic:
rw [@sq, ← Finset.prod_mul_distrib, ← Finset.prod_coe_sort]

Result:
case h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i : { x // x ∈ s }, f ↑i = ∏ x : { x // x ∈ s }, ⋯.choose * ⋯.choose

Proof state:
case h.e_f.h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
i : { x // x ∈ s }
⊢ f ↑i = ⋯.choose ^ 2

Tactic:
exact ((isSquare_iff_exists_sq _).mp (h _ i.2)).choose_spec

Result:
no goals

Proof state:
case h.e_f.h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
i : { x // x ∈ s }
⊢ f ↑i = ⋯.choose * ⋯.choose

Tactic:
rw [← @sq]

Result:
case h.e_f.h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
i : { x // x ∈ s }
⊢ f ↑i = ⋯.choose ^ 2

Proof state:
case h.e_f
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ (fun i => f ↑i) = fun x => ⋯.choose * ⋯.choose

Tactic:
ext i

Result:
case h.e_f.h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
i : { x // x ∈ s }
⊢ f ↑i = ⋯.choose * ⋯.choose

Proof state:
case h
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ ∏ i : { x // x ∈ s }, f ↑i = ∏ x : { x // x ∈ s }, ⋯.choose * ⋯.choose

Tactic:
congr

Result:
case h.e_f
ι : Type u_1
α : Type u_3
s : Finset ι
inst✝ : CommMonoid α
f : ι → α
h : ∀ c ∈ s, IsSquare (f c)
⊢ (fun i => f ↑i) = fun x => ⋯.choose * ⋯.choose
-- Mathlib/Probability/Kernel/Composition/Comp.lean
@[simp] lemma zero_comp (κ : Kernel α β) : (0 : Kernel β γ) ∘ₖ κ = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
⊢ 0 ∘ₖ κ = 0

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((0 ∘ₖ κ) a✝¹) s✝ = (0 a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
a✝¹ : α
s✝ : Set γ
a✝ : MeasurableSet s✝
⊢ ((0 ∘ₖ κ) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
simp [comp_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_left_Ioc (a b c : α) : (Ioc a b).image (c + ·) = Ioc (c + a) (c + b)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)

Tactic:
rw [← map_add_left_Ioc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem edges_subset_edgeSet {u v : V} :
    ∀ (p : G.Walk u v) ⦃e : Sym2 V⦄, e ∈ p.edges → e ∈ G.edgeSet
  | cons h' p', e, h => by
    cases h
    · exact h'
    next h' => exact edges_subset_edgeSet p' h'

Proof state:
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
e : Sym2 V
h : e ∈ (cons h' p').edges
⊢ e ∈ G.edgeSet

Tactic:
cases h

Result:
case head
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { toProd := (u, v✝), adj := h' }.edge ∈ G.edgeSet

case tail
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
e : Sym2 V
a✝ : List.Mem e (List.map Dart.edge p'.darts)
⊢ e ∈ G.edgeSet

Proof state:
case head
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
⊢ { toProd := (u, v✝), adj := h' }.edge ∈ G.edgeSet

Tactic:
exact h'

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v v✝ : V
h'✝ : G.Adj u v✝
p' : G.Walk v✝ v
e : Sym2 V
h' : List.Mem e (List.map Dart.edge p'.darts)
⊢ e ∈ G.edgeSet

Tactic:
exact edges_subset_edgeSet p' h'

Result:
no goals

Proof state:
case tail
V : Type u
G : SimpleGraph V
u v v✝ : V
h' : G.Adj u v✝
p' : G.Walk v✝ v
e : Sym2 V
a✝ : List.Mem e (List.map Dart.edge p'.darts)
⊢ e ∈ G.edgeSet

Tactic:
next h' => exact edges_subset_edgeSet p' h'

Result:
no goals