harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_push {f : α → β} {as : Array α} {x : α} :
    (as.push x).map f = (as.map f).push (f x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
as : Array α
x : α
⊢ map f (as.push x) = (map f as).push (f x)

Tactic:
ext

Result:
case h₁
α : Type u_1
β : Type u_2
f : α → β
as : Array α
x : α
⊢ (map f (as.push x)).size = ((map f as).push (f x)).size

case h₂
α : Type u_1
β : Type u_2
f : α → β
as : Array α
x : α
i✝ : Nat
hi₁✝ : i✝ < (map f (as.push x)).size
hi₂✝ : i✝ < ((map f as).push (f x)).size
⊢ (map f (as.push x))[i✝] = ((map f as).push (f x))[i✝]

Proof state:
case h₂
α : Type u_1
β : Type u_2
f : α → β
as : Array α
x : α
i✝ : Nat
hi₁✝ : i✝ < (map f (as.push x)).size
hi₂✝ : i✝ < ((map f as).push (f x)).size
⊢ (map f (as.push x))[i✝] = ((map f as).push (f x))[i✝]

Tactic:
simp only [getElem_map, getElem_push, size_map]

Result:
case h₂
α : Type u_1
β : Type u_2
f : α → β
as : Array α
x : α
i✝ : Nat
hi₁✝ : i✝ < (map f (as.push x)).size
hi₂✝ : i✝ < ((map f as).push (f x)).size
⊢ f (if h : i✝ < as.size then as[i✝] else x) = if h : i✝ < as.size then f as[i✝] else f x

Proof state:
case h₂
α : Type u_1
β : Type u_2
f : α → β
as : Array α
x : α
i✝ : Nat
hi₁✝ : i✝ < (map f (as.push x)).size
hi₂✝ : i✝ < ((map f as).push (f x)).size
⊢ f (if h : i✝ < as.size then as[i✝] else x) = if h : i✝ < as.size then f as[i✝] else f x

Tactic:
split <;> rfl

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
f : α → β
as : Array α
x : α
⊢ (map f (as.push x)).size = ((map f as).push (f x)).size

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma restrict_spanning_iff (hSR : S ⊆ R) (hR : R ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Spanning S ↔ R ⊆ M.closure S

Tactic:
rw [spanning_iff, restrict_ground_eq, and_iff_left hSR, restrict_closure_eq _ hSR, inter_eq_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem coe_toReal (θ : Angle) : (θ.toReal : Angle) = θ

Proof state:
θ : Angle
⊢ ↑θ.toReal = θ

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ ↑(↑x✝).toReal = ↑x✝

Proof state:
case h
x✝ : ℝ
⊢ ↑(↑x✝).toReal = ↑x✝

Tactic:
exact coe_toIocMod _ _

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem FiniteDimensional.of_isCompact_closedBall {r : ℝ} (rpos : 0 < r) {c : E}
    (h : IsCompact (Metric.closedBall c r)) : FiniteDimensional 𝕜 E :=
  .of_isCompact_closedBall₀ 𝕜 rpos <| by simpa using h.vadd (-c)

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
c : E
h : IsCompact (closedBall c r)
⊢ IsCompact (closedBall 0 r)

Tactic:
simpa using h.vadd (-c)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_append_1 (s m n : Nat) :
    range' s m ++ range' (s + m) n = range' s (m + n)

Proof state:
s m n : Nat
⊢ range' s m ++ range' (s + m) n = range' s (m + n)

Tactic:
simpa using range'_append s m n 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem zipWith_nil_right {f : α → β → γ} : zipWith f l [] = []

Proof state:
α : Type u
β : Type v
γ : Type w
l : List α
f : α → β → γ
⊢ zipWith f l nil = nil

Tactic:
simp [zipWith]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
    elem a l = l.contains a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : Array α
⊢ elem a l = l.contains a

Tactic:
simp [elem]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofMkLEMk_comp_ofMkLEMk {B A₁ A₂ A₃ : C} (f : A₁ ⟶ B) [Mono f] (g : A₂ ⟶ B) [Mono g]
    (h : A₃ ⟶ B) [Mono h] (h₁ : mk f ≤ mk g) (h₂ : mk g ≤ mk h) :
    ofMkLEMk f g h₁ ≫ ofMkLEMk g h h₂ = ofMkLEMk f h (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst✝² : Mono f
g : A₂ ⟶ B
inst✝¹ : Mono g
h : A₃ ⟶ B
inst✝ : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso h).hom =
    (underlyingIso f).inv ≫ underlying.map ⋯.hom ≫ (underlyingIso h).hom

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst✝² : Mono f
g : A₂ ⟶ B
inst✝¹ : Mono g
h : A₃ ⟶ B
inst✝ : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
⊢ ofMkLEMk f g h₁ ≫ ofMkLEMk g h h₂ = ofMkLEMk f h ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp_assoc underlying, assoc,
  Iso.hom_inv_id_assoc]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
B A₁ A₂ A₃ : C
f : A₁ ⟶ B
inst✝² : Mono f
g : A₂ ⟶ B
inst✝¹ : Mono g
h : A₃ ⟶ B
inst✝ : Mono h
h₁ : mk f ≤ mk g
h₂ : mk g ≤ mk h
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) ≫ (underlyingIso h).hom =
    (underlyingIso f).inv ≫ underlying.map ⋯.hom ≫ (underlyingIso h).hom
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_inf (x : M) : x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
x : M
⊢ x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'

Tactic:
rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
  Submodule.mem_inf]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem algebraMap_leftInverse :
    Function.LeftInverse algebraMapInv (algebraMap R <| ExteriorAlgebra R M) := fun x => by
  simp [algebraMapInv]

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : R
⊢ algebraMapInv ((algebraMap R (ExteriorAlgebra R M)) x) = x

Tactic:
simp [algebraMapInv]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma map_hom_inv_id_eval (e : X ≅ Y) (F : C ⥤ D) (j : J) :
    F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{u_5, u_1} C
inst✝ : Category.{u_6, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))

Tactic:
rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id,
  GradedObject.categoryOfGradedObjects_id, Functor.map_id]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
lemma eq_one_or_neg_one_of_mul_eq_one' (h : u * v = 1) : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Proof state:
u v : ℤ
h : u * v = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
have h' : v * u = 1 := mul_comm u v ▸ h

Result:
u v : ℤ
h : u * v = 1
h' : v * u = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Proof state:
u v : ℤ
h : u * v = 1
h' : v * u = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h <;>
    obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h' <;> tauto

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findIdx_toArray {as : List α} {p : α → Bool} :
    as.toArray.findIdx p = as.findIdx p

Proof state:
α : Type u_1
as : List α
p : α → Bool
⊢ Array.findIdx p as.toArray = findIdx p as

Tactic:
rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preOmega_omega0 : preOmega ω = ω

Proof state:
⊢ preOmega ω = ω

Tactic:
simp_rw [← isNormal_preOmega.apply_omega0, preOmega_natCast, iSup_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.true_and (b : Bool) : (true && b) = b

Proof state:
b : Bool
⊢ (true && b) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma eHolderNorm_ne_top : eHolderNorm r f ≠ ∞ ↔ MemHolder r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f ≠ ⊤ ↔ MemHolder r f

Tactic:
rw [← eHolderNorm_lt_top, lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem const_congr {f₁ f₂ g₁ g₂ : R} {U hu} (hf : f₁ = f₂) (hg : g₁ = g₂) :
    const R f₁ g₁ U hu = const R f₂ g₂ U (hg ▸ hu)

Proof state:
R : Type u
inst✝ : CommRing R
f₁ g₁ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
⊢ const R f₁ g₁ U hu = const R f₁ g₁ U ⋯

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
f₁ f₂ g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
hf : f₁ = f₂
hg : g₁ = g₂
⊢ const R f₁ g₁ U hu = const R f₂ g₂ U ⋯

Tactic:
substs hf hg

Result:
R : Type u
inst✝ : CommRing R
f₁ g₁ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl
⊢ const R f₁ g₁ U hu = const R f₁ g₁ U ⋯
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem norm_lineDeriv_le_of_lipschitzOn {f : E → F} {x₀ : E} {s : Set E} (hs : s ∈ 𝓝 x₀)
    {C : ℝ≥0} (hlip : LipschitzOnWith C f s) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖

Tactic:
refine norm_lineDeriv_le_of_lip' 𝕜 C.coe_nonneg ?_

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
v : E
f : E → F
x₀ : E
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ ↑C * ‖x - x₀‖

Tactic:
filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem isPreconnected_iff_preconnectedSpace {s : Set α} : IsPreconnected s ↔ PreconnectedSpace s :=
  ⟨Subtype.preconnectedSpace, fun h => by
    simpa using isPreconnected_univ.image ((↑) : s → α) continuous_subtype_val.continuousOn⟩

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : PreconnectedSpace ↑s
⊢ IsPreconnected s

Tactic:
simpa using isPreconnected_univ.image ((↑) : s → α) continuous_subtype_val.continuousOn

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_stabilizer_of_transitive [IsPretransitive G X] :
    (stabilizer G x).index = Nat.card X

Proof state:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
x : X
inst✝ : IsPretransitive G X
⊢ (stabilizer G x).index = Nat.card X

Tactic:
rw [index_stabilizer, orbit_eq_univ, Set.ncard_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma le_comap_range_rTensor (q : Q) :
    LinearMap.range g ≤ (LinearMap.range (rTensor Q g)).comap
      ((TensorProduct.mk R P Q).flip q)

Proof state:
case intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ g n ∈ Submodule.comap ((TensorProduct.mk R P Q).flip q) (range (rTensor Q g))

Tactic:
exact ⟨n ⊗ₜ[R] q, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
⊢ range g ≤ Submodule.comap ((TensorProduct.mk R P Q).flip q) (range (rTensor Q g))

Tactic:
rintro x ⟨n, rfl⟩

Result:
case intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ g n ∈ Submodule.comap ((TensorProduct.mk R P Q).flip q) (range (rTensor Q g))
-- Mathlib/Algebra/Star/Unitary.lean
/-- Unitary conjugation preserves the spectrum, star on right. -/
@[simp]
lemma spectrum.unitary_conjugate' {a : A} {u : unitary A} :
    spectrum R ((star u : A) * a * u) = spectrum R a

Proof state:
R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : StarMul A
a : A
u : ↥(unitary A)
⊢ spectrum R (star ↑u * a * ↑u) = spectrum R a

Tactic:
simpa using spectrum.unitary_conjugate (u := star u)

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive] lemma sup_div_inf_eq_mabs_div (a b : α) : (a ⊔ b) / (a ⊓ b) = |b / a|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ 1 ≤ mabs (b / a)

Tactic:
exact one_le_mabs _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊔ b) / (a ⊓ b) = mabs (b / a)

Tactic:
simp_rw [sup_div, div_inf, div_self', sup_comm, sup_sup_sup_comm, sup_idem]

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ⊔ b / a ⊔ 1 = mabs (b / a)

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ⊔ b / a ⊔ 1 = mabs (b / a)

Tactic:
rw [← inv_div, sup_comm (b := _ / _), ← mabs, sup_eq_left]

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ 1 ≤ mabs (b / a)
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma isProbabilityMeasure_comap (hf : Injective f) (hf' : ∀ᵐ a ∂μ, a ∈ range f)
    (hf'' : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) :
    IsProbabilityMeasure (μ.comap f) where
  measure_univ

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ f '' univ ∈ ae μ

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ (Measure.comap f μ) univ = 1

Tactic:
rw [comap_apply _ hf hf'' _ MeasurableSet.univ,
  ← mem_ae_iff_prob_eq_one (hf'' _ MeasurableSet.univ)]

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ f '' univ ∈ ae μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem map_fst_zip (l₁ : Vector α n) (l₂ : Vector β n) :
    map Prod.fst (zip l₁ l₂) = l₁

Proof state:
case mk.mk
α : Type u_1
n : Nat
β : Type u_2
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ map Prod.fst
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.zip
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }

Tactic:
simp_all [Array.map_fst_zip]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l₁ : Vector α n
l₂ : Vector β n
⊢ map Prod.fst (l₁.zip l₂) = l₁

Tactic:
cases l₁

Result:
case mk
α : Type u_1
n : Nat
β : Type u_2
l₂ : Vector β n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map Prod.fst ({ toArray := toArray✝, size_toArray := size_toArray✝ }.zip l₂) =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type u_1
n : Nat
β : Type u_2
l₂ : Vector β n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map Prod.fst ({ toArray := toArray✝, size_toArray := size_toArray✝ }.zip l₂) =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
n : Nat
β : Type u_2
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array β
size_toArray✝ : toArray✝.size = n
⊢ map Prod.fst
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.zip
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_mul_ediv_cancel_left (a b : Int) (h : a ≠ 0) : -(a * b) / a = -b

Proof state:
a b : Int
h : a ≠ 0
⊢ -(a * b) / a = -b

Tactic:
rw [neg_ediv_of_dvd (Int.dvd_mul_right a b), mul_ediv_cancel_left _ h]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem IsPathConnected.union {U V : Set X} (hU : IsPathConnected U) (hV : IsPathConnected V)
    (hUV : (U ∩ V).Nonempty) : IsPathConnected (U ∪ V)

Proof state:
case right.inr
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y

Tactic:
exact (hV.joinedIn x xV y yV).mono subset_union_right

Result:
no goals

Proof state:
case right.inl
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

Tactic:
exact (hU.joinedIn x xU y yU).mono subset_union_left

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
hUV : (U ∩ V).Nonempty
⊢ IsPathConnected (U ∪ V)

Tactic:
rcases hUV with ⟨x, xU, xV⟩

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ IsPathConnected (U ∪ V)

Proof state:
case right
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ ∀ {y : X}, y ∈ U ∪ V → JoinedIn (U ∪ V) x y

Tactic:
rintro y (yU | yV)

Result:
case right.inl
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yU : y ∈ U
⊢ JoinedIn (U ∪ V) x y

case right.inr
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
y : X
yV : y ∈ V
⊢ JoinedIn (U ∪ V) x y

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ IsPathConnected (U ∪ V)

Tactic:
use x, Or.inl xU

Result:
case right
X : Type u_1
inst✝ : TopologicalSpace X
U V : Set X
hU : IsPathConnected U
hV : IsPathConnected V
x : X
xU : x ∈ U
xV : x ∈ V
⊢ ∀ {y : X}, y ∈ U ∪ V → JoinedIn (U ∪ V) x y
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Icc_add_one_sub_one_eq_Ioo (a b : α) : Icc (a + 1) (b - 1) = Ioo a b

Proof state:
α : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : One α
inst✝⁴ : Add α
inst✝³ : Sub α
inst✝² : SuccAddOrder α
inst✝¹ : PredSubOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (a + 1) (b - 1) = Ioo a b

Tactic:
simpa [succ_eq_add_one, pred_eq_sub_one] using Icc_succ_pred_eq_Ioo a b

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_three (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 3 = a * a * a

Tactic:
simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_ofNat, NNReal.rpow_ofNat, pow_three]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun x => x * (x * x)) a = a * a * a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun z => id z * (id z * id z)) a = a * a * a

Tactic:
rw [cfcₙ_mul id _ a, cfcₙ_mul id _ a, ← mul_assoc, cfcₙ_id ℝ≥0 a]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun x => x * (x * x)) a = a * a * a

Tactic:
change cfcₙ (fun z : ℝ≥0 => id z * (id z * id z)) a = a * a * a

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun z => id z * (id z * id z)) a = a * a * a
-- Mathlib/Computability/TuringMachine.lean
theorem trNormal_run {k : K} (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ) :
    trNormal (stRun s q) = goto fun _ _ ↦ go k s q

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trNormal (stRun s q) = goto fun x x => go k s q

Tactic:
cases s <;> rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
/-- All triangles are isosceles in an ultrametric normed group. -/
@[to_additive "All triangles are isosceles in an ultrametric normed additive group."]
lemma norm_mul_eq_max_of_norm_ne_norm
    {x y : S} (h : ‖x‖ ≠ ‖y‖) : ‖x * y‖ = max ‖x‖ ‖y‖

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ ‖x * y‖ = ‖x‖ ⊔ ‖y‖

Tactic:
rw [← div_inv_eq_mul, ← dist_eq_norm_div, dist_eq_max_of_dist_ne_dist _ 1 _ (by simp [h])]

Result:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ dist x 1 ⊔ dist 1 y⁻¹ = ‖x‖ ⊔ ‖y‖

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ dist x 1 ⊔ dist 1 y⁻¹ = ‖x‖ ⊔ ‖y‖

Tactic:
simp only [dist_one_right, dist_one_left, norm_inv']

Result:
no goals

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ dist x 1 ≠ dist 1 y⁻¹

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
theorem subsingleton_coe (s : Set α) : Subsingleton s ↔ s.Subsingleton

Proof state:
case mpr
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton ↑s

Tactic:
exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)

Result:
no goals

Proof state:
case mp
α : Type u
s : Set α
⊢ Subsingleton ↑s → s.Subsingleton

Tactic:
refine fun h => fun a ha b hb => ?_

Result:
case mp
α : Type u
s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b

Proof state:
α : Type u
s : Set α
⊢ Subsingleton ↑s ↔ s.Subsingleton

Tactic:
constructor

Result:
case mp
α : Type u
s : Set α
⊢ Subsingleton ↑s → s.Subsingleton

case mpr
α : Type u
s : Set α
⊢ s.Subsingleton → Subsingleton ↑s

Proof state:
case mp
α : Type u
s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b

Tactic:
exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)

Result:
no goals