harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/LiminfLimsup.lean
theorem sup_liminf (a : α) : a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f

Tactic:
simp only [liminf_eq_iSup_iInf]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ a ⊔ ⨆ s ∈ f, ⨅ a ∈ s, u a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1

Tactic:
rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]

Result:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ ⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
a : α
⊢ ⨆ i ∈ f, (⨅ a ∈ i, u a) ⊔ a = ⨆ s ∈ f, ⨅ a_1 ∈ s, a ⊔ u a_1

Tactic:
simp_rw [iInf₂_sup_eq, sup_comm (a := a)]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma opcyclesMap'_add :
    opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ +
      opcyclesMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
have γ' : RightHomologyMapData φ' h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
γ' : RightHomologyMapData φ' h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
γ' : RightHomologyMapData φ' h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
simp only [γ.opcyclesMap'_eq, γ'.opcyclesMap'_eq,
  (γ.add γ').opcyclesMap'_eq, RightHomologyMapData.add_φQ]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem le_rpow_self_of_one_le {x : ℝ≥0∞} {z : ℝ} (hx : 1 ≤ x) (h_one_le : 1 ≤ z) : x ≤ x ^ z

Proof state:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z

Tactic:
exact ENNReal.rpow_le_rpow_of_exponent_le hx h_one_le

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ≤ x ^ z

Tactic:
nth_rw 1 [← ENNReal.rpow_one x]

Result:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
h_one_le : 1 ≤ z
⊢ x ^ 1 ≤ x ^ z
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
@[simp]
lemma scaleRoots_one (p : R[X]) :
    p.scaleRoots 1 = p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.scaleRoots 1 = p

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (p.scaleRoots 1).coeff n✝ = p.coeff n✝

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (p.scaleRoots 1).coeff n✝ = p.coeff n✝

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrable_indicatorConstLp {E} [NormedAddCommGroup E] {p : ℝ≥0∞} {s : Set α}
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : E) :
    Integrable (indicatorConstLp p hs hμs c) μ

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ c = 0 ∨ μ s ≠ ⊤

Tactic:
exact .inr hμs

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ Integrable (↑↑(indicatorConstLp p hs hμs c)) μ

Tactic:
rw [integrable_congr indicatorConstLp_coeFn, integrable_indicator_iff hs, IntegrableOn,
  integrable_const_iff, isFiniteMeasure_restrict]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
⊢ c = 0 ∨ μ s ≠ ⊤
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem dist_partial_sum' (u : ℕ → α) (n : ℕ) :
    dist (∑ k ∈ range n, u k) (∑ k ∈ range (n + 1), u k) = ‖u n‖

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
u : ℕ → α
n : ℕ
⊢ dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖

Tactic:
simp [dist_eq_norm', sum_range_succ]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
lemma adjoin_id_eq_span_one_union (s : Set 𝕜) :
    ((StarAlgebra.adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) : Set C(s, 𝕜)) =
      span 𝕜 ({(1 : C(s, 𝕜))} ∪ (adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}))

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
⊢ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) =
    ↑(span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})))

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ ↑(span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})))

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
x : C(↑s, 𝕜)
⊢ x ∈ ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ↔
    x ∈ ↑(span 𝕜 ({1} ∪ ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})))

Tactic:
rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra,
  ← StarSubalgebra.mem_toSubalgebra, ← Subalgebra.mem_toSubmodule,
  StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/GaloisObjects.lean
@[simp]
lemma evaluationEquivOfIsGalois_symm_fiber (A : C) [IsGalois A] (a b : F.obj A) :
    F.map ((evaluationEquivOfIsGalois F A a).symm b).hom a = b

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsGalois A
a b : (F.obj A).carrier
⊢ F.map ((evaluationEquivOfIsGalois F A a).symm b).hom a = b

Tactic:
change (evaluationEquivOfIsGalois F A a) _ = _

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsGalois A
a b : (F.obj A).carrier
⊢ (evaluationEquivOfIsGalois F A a) ((evaluationEquivOfIsGalois F A a).symm b) = b

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
A : C
inst✝ : IsGalois A
a b : (F.obj A).carrier
⊢ (evaluationEquivOfIsGalois F A a) ((evaluationEquivOfIsGalois F A a).symm b) = b

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem tendsto_nhds_top_mono [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β]
    {l : Filter α} {f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ᶠ[l] g) : Tendsto g l (𝓝 ⊤)

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hf : Tendsto f l (𝓝 ⊤)
hg : f ≤ᶠ[l] g
⊢ Tendsto g l (𝓝 ⊤)

Tactic:
simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢

Result:
α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
⊢ ∀ i < ⊤, ∀ᶠ (a : α) in l, g a ∈ Ioi i

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x

Tactic:
filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
⊢ ∀ i < ⊤, ∀ᶠ (a : α) in l, g a ∈ Ioi i

Tactic:
intro x hx

Result:
α : Type u
β : Type v
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ i < ⊤, ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma liminf_add_top_of_ne_bot (h : liminf u f = ⊤) (h' : liminf v f ≠ ⊥) :
    liminf (u + v) f = ⊤

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ liminf u f + liminf v f

Tactic:
rw [h, top_add_of_ne_bot h']

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ liminf (u + v) f = ⊤

Tactic:
apply top_le_iff.1 (le_trans _ le_liminf_add)

Result:
α : Type u_3
f : Filter α
u v : α → EReal
h : liminf u f = ⊤
h' : liminf v f ≠ ⊥
⊢ ⊤ ≤ liminf u f + liminf v f
-- Mathlib/Data/Nat/ModEq.lean
theorem add_div_eq_of_add_mod_lt {a b c : ℕ} (hc : a % c + b % c < c) :
    (a + b) / c = a / c + b / c :=
  if hc0 : c = 0 then by simp [hc0]
  else by rw [add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_lt hc), add_zero]

Proof state:
a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
rw [add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_lt hc), add_zero]

Result:
no goals

Proof state:
a b c : ℕ
hc : a % c + b % c < c
hc0 : c = 0
⊢ (a + b) / c = a / c + b / c

Tactic:
simp [hc0]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem dlookup_kinsert {a} {b : β a} (l : List (Sigma β)) :
    dlookup a (kinsert a b l) = some b

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ dlookup a (kinsert a b l) = some b

Tactic:
simp only [kinsert, dlookup_cons_eq]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generatePiSystem_subset_self {S : Set (Set α)} (h_S : IsPiSystem S) :
    generatePiSystem S ⊆ S := fun x h => by
  induction h with
  | base h_s => exact h_s
  | inter _ _ h_nonempty h_s h_u => exact h_S _ h_s _ h_u h_nonempty

Proof state:
case base
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s✝ : Set α
h_s : s✝ ∈ S
⊢ s✝ ∈ S

Tactic:
exact h_s

Result:
no goals

Proof state:
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
⊢ x ∈ S

Tactic:
induction h with
| base h_s => exact h_s
| inter _ _ h_nonempty h_s h_u => exact h_S _ h_s _ h_u h_nonempty

Result:
no goals

Proof state:
case inter
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty : (s✝ ∩ t✝).Nonempty
h_s : s✝ ∈ S
h_u : t✝ ∈ S
⊢ s✝ ∩ t✝ ∈ S

Tactic:
exact h_S _ h_s _ h_u h_nonempty

Result:
no goals
-- Mathlib/Topology/Instances/Int.lean
theorem cobounded_eq : Bornology.cobounded ℤ = atBot ⊔ atTop

Proof state:
⊢ Bornology.cobounded ℤ = atBot ⊔ atTop

Tactic:
simp_rw [← comap_dist_right_atTop (0 : ℤ), dist_eq', sub_zero,
  ← comap_abs_atTop, ← @Int.comap_cast_atTop ℝ, comap_comap]

Result:
⊢ comap (fun x => ↑|x|) atTop = comap (Int.cast ∘ abs) atTop

Proof state:
⊢ comap (fun x => ↑|x|) atTop = comap (Int.cast ∘ abs) atTop

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma isIso_i (hg : S.g = 0) : IsIso h.i :=
  ⟨h.liftK (𝟙 S.X₂) (by rw [hg, id_comp]),
    by simp only [← cancel_mono h.i, id_comp, assoc, liftK_i, comp_id], liftK_i _ _ _⟩

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hg : S.g = 0
⊢ h.i ≫ h.liftK (𝟙 S.X₂) ⋯ = 𝟙 h.K

Tactic:
simp only [← cancel_mono h.i, id_comp, assoc, liftK_i, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
rw [hg, id_comp]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
lemma length_takeUntil_lt {u v w : V} {p : G.Walk v w} (h : u ∈ p.support) (huw : u ≠ w) :
    (p.takeUntil u h).length < p.length

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
⊢ (p.takeUntil u h).length < p.length

Tactic:
rw [(p.length_takeUntil_le h).lt_iff_ne]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
⊢ (p.takeUntil u h).length ≠ p.length

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ u = w

Tactic:
simpa using (hl ▸ getVert_takeUntil h (by rfl) :
(p.takeUntil u h).getVert (p.takeUntil u h).length = p.getVert p.length)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
⊢ (p.takeUntil u h).length ≠ p.length

Tactic:
exact fun hl ↦ huw (by simpa using (hl ▸ getVert_takeUntil h (by rfl) :
  (p.takeUntil u h).getVert (p.takeUntil u h).length = p.getVert p.length))

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ (p.takeUntil u h).length

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_succ_zero : testBit (x + 1) 0 = !(testBit x 0)

Proof state:
x : Nat
⊢ decide (1 - x % 2 = 1) = !decide (x % 2 = 1)

Tactic:
cases Nat.mod_two_eq_zero_or_one x with | _ p =>
  simp [p]

Result:
no goals

Proof state:
case inr
x : Nat
p : x % 2 = 1
⊢ decide (1 - x % 2 = 1) = !decide (x % 2 = 1)

Tactic:
simp [p]

Result:
no goals

Proof state:
x : Nat
⊢ (x + 1).testBit 0 = !x.testBit 0

Tactic:
simp [testBit_to_div_mod, succ_mod_two]

Result:
x : Nat
⊢ decide (1 - x % 2 = 1) = !decide (x % 2 = 1)
-- Mathlib/Algebra/Ring/Units.lean
theorem divp_add_divp_same (a b : α) (u : αˣ) : a /ₚ u + b /ₚ u = (a + b) /ₚ u

Proof state:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u + b /ₚ u = (a + b) /ₚ u

Tactic:
simp only [divp, add_mul]

Result:
no goals
-- Mathlib/Data/Vector3.lean
theorem insert_fs (a : α) (b : α) (v : Vector3 α n) (i : Fin2 (n + 1)) :
    insert a (b :: v) (fs i) = b :: insert a v i :=
  funext fun j => by
    refine j.cases' ?_ fun j => ?_ <;> simp [insert, insertPerm]
    refine Fin2.cases' ?_ ?_ (insertPerm i j) <;> simp [insertPerm]

Proof state:
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j : Fin2 (n + 1 + 1)
⊢ insert a (b :: v) i.fs j = (b :: insert a v i) j

Tactic:
refine j.cases' ?_ fun j => ?_ <;> simp [insert, insertPerm]

Result:
case refine_2
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match i.insertPerm j with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) (i.insertPerm j)

Proof state:
case refine_2
α : Type u_1
n : ℕ
a b : α
v : Vector3 α n
i : Fin2 (n + 1)
j✝ : Fin2 (n + 1 + 1)
j : Fin2 (n + 1)
⊢ (a :: b :: v)
      (match i.insertPerm j with
      | fz => fz
      | k.fs => k.fs.fs) =
    (a :: v) (i.insertPerm j)

Tactic:
refine Fin2.cases' ?_ ?_ (insertPerm i j) <;> simp [insertPerm]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma sup_eq_mul_oneLePart_div (a b : α) : a ⊔ b = b * (a / b)⁺ᵐ

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

Tactic:
simp [oneLePart, mul_sup]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem continuous_normSq : Continuous normSq

Proof state:
⊢ Continuous ⇑normSq

Tactic:
simpa [← Complex.normSq_eq_norm_sq] using continuous_norm (E := ℂ).pow 2

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem Basis.addHaar_reindex (b : Basis ι ℝ E) (e : ι ≃ ι') :
    (b.reindex e).addHaar = b.addHaar

Proof state:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
⊢ (b.reindex e).addHaar = b.addHaar

Tactic:
rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma opcyclesMap'_neg :
    opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Tactic:
simp only [γ.opcyclesMap'_eq, γ.neg.opcyclesMap'_eq, RightHomologyMapData.neg_φQ]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂
-- Mathlib/Order/Lattice.lean
theorem sup_sup_distrib_left (a b c : α) : a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)

Tactic:
rw [sup_sup_sup_comm, sup_idem]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_le_half_period {x : AddCircle p} (hp : p ≠ 0) : ‖x‖ ≤ |p| / 2

Proof state:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖Quot.mk (⇑(QuotientAddGroup.leftRel (zmultiples p))) x‖ ≤ |p| / 2

Tactic:
change ‖(x : AddCircle p)‖ ≤ |p| / 2

Result:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖↑x‖ ≤ |p| / 2

Proof state:
p : ℝ
x : AddCircle p
hp : p ≠ 0
⊢ ‖x‖ ≤ |p| / 2

Tactic:
obtain ⟨x⟩ := x

Result:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖Quot.mk (⇑(QuotientAddGroup.leftRel (zmultiples p))) x‖ ≤ |p| / 2

Proof state:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x))| ≤ 1 / 2

Tactic:
exact abs_sub_round (p⁻¹ * x)

Result:
no goals

Proof state:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖↑x‖ ≤ |p| / 2

Tactic:
rw [norm_eq, ← mul_le_mul_left (abs_pos.mpr (inv_ne_zero hp)), ← abs_mul, mul_sub, mul_left_comm,
  ← mul_div_assoc, ← abs_mul, inv_mul_cancel₀ hp, mul_one, abs_one]

Result:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |p⁻¹ * x - ↑(round (p⁻¹ * x))| ≤ 1 / 2
-- Mathlib/Data/List/Map2.lean
theorem zipLeft_eq_zipLeft' (as : List α) (bs : List β) : zipLeft as bs = (zipLeft' as bs).fst

Proof state:
case cons
α : Type u
β : Type v
bs : List β
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) bs = (zipWithLeft' Prod.mk (head✝ :: atl) bs).fst

Tactic:
cases bs with
| nil => rfl
| cons _ btl =>
  rw [zipWithLeft, zipWithLeft', cons_inj_right]
  exact @zipLeft_eq_zipLeft' atl btl

Result:
no goals

Proof state:
case cons.nil
α : Type u
β : Type v
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) [] = (zipWithLeft' Prod.mk (head✝ :: atl) []).fst

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
bs : List β
⊢ zipWithLeft Prod.mk [] bs = (zipWithLeft' Prod.mk [] bs).fst

Tactic:
rfl

Result:
no goals

Proof state:
case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk (head✝¹ :: atl) (head✝ :: btl) = (zipWithLeft' Prod.mk (head✝¹ :: atl) (head✝ :: btl)).fst

Tactic:
rw [zipWithLeft, zipWithLeft', cons_inj_right]

Result:
case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst

Proof state:
α : Type u
β : Type v
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst

Tactic:
cases as with
| nil => rfl
| cons _ atl =>
  cases bs with
  | nil => rfl
  | cons _ btl =>
    rw [zipWithLeft, zipWithLeft', cons_inj_right]
    exact @zipLeft_eq_zipLeft' atl btl

Result:
no goals

Proof state:
case cons.cons
α : Type u
β : Type v
head✝¹ : α
atl : List α
head✝ : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst

Tactic:
exact @zipLeft_eq_zipLeft' atl btl

Result:
no goals

Proof state:
α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipLeft bs = (as.zipLeft' bs).fst

Tactic:
rw [zipLeft, zipLeft']

Result:
α : Type u
β : Type v
as : List α
bs : List β
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem sum_add_index {S : Type*} [AddCommMonoid S] (p q : R[X]) (f : ℕ → R → S)
    (hf : ∀ i, f i 0 = 0) (h_add : ∀ a b₁ b₂, f a (b₁ + b₂) = f a b₁ + f a b₂) :
    (p + q).sum f = p.sum f + q.sum f

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from add_def p q]

Result:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ { toFinsupp := p.toFinsupp + q.toFinsupp }.sum f = p.sum f + q.sum f

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ { toFinsupp := p.toFinsupp + q.toFinsupp }.sum f = p.sum f + q.sum f

Tactic:
exact Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)

Result:
no goals
-- Mathlib/Algebra/Algebra/Prod.lean
theorem fst_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : (fst R B C).comp (prod f g) = f

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
ext

Result:
case H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Proof state:
case H
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Star/Module.lean
theorem IsSelfAdjoint.skewAdjointPart_apply {x : A} (hx : IsSelfAdjoint x) :
    skewAdjointPart R x = 0 := Subtype.eq <| by
  rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ↑((skewAdjointPart R) x) = ↑0

Tactic:
rw [skewAdjointPart_apply_coe, hx.star_eq, sub_self, smul_zero, ZeroMemClass.coe_zero]

Result:
no goals