harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
/--
This lemma establishes a condition under which a subgraph is the same as a connected component.
Note the asymmetry in the hypothesis `h`: `v` is in `H.verts`, but `w` is not required to be.
-/
lemma Connected.exists_verts_eq_connectedComponentSupp {H : Subgraph G}
    (hc : H.Connected) (h : ∀ v ∈ H.verts, ∀ w, G.Adj v w → H.Adj v w) :
    ∃ c : G.ConnectedComponent, H.verts = c.supp

Proof state:
case h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ H.verts = (G.connectedComponentMk v).supp

Tactic:
ext w

Result:
case h.h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ w ∈ (G.connectedComponentMk v).supp

Proof state:
case h.h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ w ∈ (G.connectedComponentMk v).supp

Tactic:
simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]

Result:
case h.h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ G.Reachable w v

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp

Tactic:
obtain ⟨v, hv⟩ := hc.nonempty

Result:
case intro
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ c, H.verts = c.supp

Tactic:
rw [SimpleGraph.ConnectedComponent.exists]

Result:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp

Proof state:
case intro
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ ∃ v, H.verts = (G.connectedComponentMk v).supp

Tactic:
use v

Result:
case h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
⊢ H.verts = (G.connectedComponentMk v).supp

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
⊢ G.Reachable w v

Tactic:
simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom

Result:
no goals

Proof state:
case h.h
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Connected
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
v : V
hv : v ∈ H.verts
w : V
⊢ w ∈ H.verts ↔ G.Reachable w v

Tactic:
exact ⟨fun hw ↦ by simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom,
  fun a ↦ a.symm.mem_subgraphVerts h hv⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getKey!_eq [BEq α] [Inhabited α] {l : AssocList α β} {a : α} :
    l.getKey! a = List.getKey! a l.toList

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getKey! a tail✝ = List.getKey! a tail✝.toList
⊢ getKey! a (cons key✝ value✝ tail✝) = List.getKey! a (cons key✝ value✝ tail✝).toList

Tactic:
simp_all [getKey!, List.getKey!, Bool.apply_cond Option.get!]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
l : AssocList α β
a : α
⊢ getKey! a l = List.getKey! a l.toList

Tactic:
induction l

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
a : α
⊢ getKey! a nil = List.getKey! a nil.toList

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
a key✝ : α
value✝ : β key✝
tail✝ : AssocList α β
tail_ih✝ : getKey! a tail✝ = List.getKey! a tail✝.toList
⊢ getKey! a (cons key✝ value✝ tail✝) = List.getKey! a (cons key✝ value✝ tail✝).toList

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
a : α
⊢ getKey! a nil = List.getKey! a nil.toList

Tactic:
simp [getKey!, List.getKey!]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
@[simp] lemma toCircle_add (θ₁ θ₂ : Angle) : toCircle (θ₁ + θ₂) = toCircle θ₁ * toCircle θ₂

Proof state:
θ₁ θ₂ : Angle
⊢ (θ₁ + θ₂).toCircle = θ₁.toCircle * θ₂.toCircle

Tactic:
induction θ₁ using Real.Angle.induction_on

Result:
case h
θ₂ : Angle
x✝ : ℝ
⊢ (↑x✝ + θ₂).toCircle = (↑x✝).toCircle * θ₂.toCircle

Proof state:
case h
θ₂ : Angle
x✝ : ℝ
⊢ (↑x✝ + θ₂).toCircle = (↑x✝).toCircle * θ₂.toCircle

Tactic:
induction θ₂ using Real.Angle.induction_on

Result:
case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝¹ + ↑x✝).toCircle = (↑x✝¹).toCircle * (↑x✝).toCircle

Proof state:
case h.h
x✝¹ x✝ : ℝ
⊢ (↑x✝¹ + ↑x✝).toCircle = (↑x✝¹).toCircle * (↑x✝).toCircle

Tactic:
exact Circle.exp_add _ _

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_image_left : ⋃ a ∈ s, f a '' t = image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ a ∈ s, f a '' t = image2 f s t

Tactic:
simp only [image2_eq_iUnion, image_eq_iUnion]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.dvd_of_dvd_mul_right (H1 : IsCoprime x z) (H2 : x ∣ y * z) : x ∣ y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
⊢ x ∣ y

Tactic:
let ⟨a, b, H⟩ := H1

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y

Tactic:
rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y * a * x + b * (y * z)

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y * a * x + b * (y * z)

Tactic:
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma compare_iff (a b : α) {o : Ordering} : compare a b = o ↔ o.Compares a b

Proof state:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
exact compare_eq_iff_eq

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
o : Ordering
⊢ compare a b = o ↔ o.Compares a b

Tactic:
cases o <;> simp only [Ordering.Compares]

Result:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Proof state:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
exact compare_lt_iff_lt

Result:
no goals

Proof state:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
exact compare_gt_iff_gt

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_add_val_of_le {n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) :
    a.val + b.val = (a + b).val + n

Proof state:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ n ≤ a.val % n + b.val % n

Tactic:
rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ a.val + b.val = (a + b).val + n

Tactic:
rw [val_add, Nat.add_mod_add_of_le_add_mod, Nat.mod_eq_of_lt (val_lt _),
  Nat.mod_eq_of_lt (val_lt _)]

Result:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : n ≤ a.val + b.val
⊢ n ≤ a.val % n + b.val % n
-- Mathlib/Condensed/TopCatAdjunction.lean
lemma continuous_coinducingCoprod {S : CompHaus.{u}} (x : X.val.obj ⟨S⟩) :
    Continuous fun a ↦ (X.coinducingCoprod ⟨⟨S, x⟩, a⟩)

Proof state:
X : CondensedSet
S : CompHaus
x : X.val.obj (Opposite.op S)
⊢ Continuous (CondensedSet.coinducingCoprod X)

Tactic:
apply continuous_coinduced_rng

Result:
no goals

Proof state:
X : CondensedSet
S : CompHaus
x : X.val.obj (Opposite.op S)
⊢ ∀ (i : (T : CompHaus) × X.val.obj (Opposite.op T)), Continuous fun a => CondensedSet.coinducingCoprod X ⟨i, a⟩

Tactic:
rw [← continuous_sigma_iff]

Result:
X : CondensedSet
S : CompHaus
x : X.val.obj (Opposite.op S)
⊢ Continuous (CondensedSet.coinducingCoprod X)

Proof state:
X : CondensedSet
S : CompHaus
x : X.val.obj (Opposite.op S)
⊢ Continuous fun a => CondensedSet.coinducingCoprod X ⟨⟨S, x⟩, a⟩

Tactic:
suffices ∀ (i : (T : CompHaus.{u}) × X.val.obj ⟨T⟩),
    Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩

Result:
X : CondensedSet
S : CompHaus
x : X.val.obj (Opposite.op S)
⊢ ∀ (i : (T : CompHaus) × X.val.obj (Opposite.op T)), Continuous fun a => CondensedSet.coinducingCoprod X ⟨i, a⟩
-- Mathlib/Algebra/Homology/Additive.lean
theorem NatTrans.mapHomologicalComplex_naturality {c : ComplexShape ι} {F G : W₁ ⥤ W₂}
    [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms]
    (α : F ⟶ G) {C D : HomologicalComplex W₁ c} (f : C ⟶ D) :
    (F.mapHomologicalComplex c).map f ≫ (NatTrans.mapHomologicalComplex α c).app D =
      (NatTrans.mapHomologicalComplex α c).app C ≫ (G.mapHomologicalComplex c).map f

Proof state:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁵ : Category.{u_5, u_3} W₁
inst✝⁴ : Category.{u_6, u_4} W₂
inst✝³ : HasZeroMorphisms W₁
inst✝² : HasZeroMorphisms W₂
c : ComplexShape ι
F G : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : G.PreservesZeroMorphisms
α : F ⟶ G
C D : HomologicalComplex W₁ c
f : C ⟶ D
⊢ (F.mapHomologicalComplex c).map f ≫ (mapHomologicalComplex α c).app D =
    (mapHomologicalComplex α c).app C ≫ (G.mapHomologicalComplex c).map f

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem leftUnitor_whiskerRight (X Y : C) :
    (λ_ X).hom ▷ Y = (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ X).hom ▷ Y = (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom

Tactic:
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ←
    cancel_epi ((α_ _ _ _).hom ▷ _), pentagon_assoc, triangle, ← associator_naturality_middle, ←
    comp_whiskerRight_assoc, triangle, associator_naturality_left]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_mul₀ {μ : Measure α} {f g : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    μ.withDensity (f * g) = (μ.withDensity f).withDensity g

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f * g)) s = ((μ.withDensity f).withDensity g) s

Tactic:
rw [withDensity_apply _ hs, withDensity_apply _ hs, restrict_withDensity hs,
  lintegral_withDensity_eq_lintegral_mul₀ hf.restrict hg.restrict]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ μ.withDensity (f * g) = (μ.withDensity f).withDensity g

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f * g)) s = ((μ.withDensity f).withDensity g) s
-- Mathlib/GroupTheory/Complement.lean
theorem finite_right_iff (h : IsComplement H T) : Finite T ↔ H.FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex

Tactic:
exact ⟨fun _ ↦ finiteIndex_of_finite_quotient H, fun _ ↦ finite_quotient_of_finiteIndex H⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite ↑T ↔ H.FiniteIndex

Tactic:
rw [← h.rightQuotientEquiv.finite_iff,
  (QuotientGroup.quotientRightRelEquivQuotientLeftRel H).finite_iff]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
h : IsComplement (↑H) T
⊢ Finite (G ⧸ H) ↔ H.FiniteIndex
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_modify_self [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
fallback : β k
f : β k → β k
h : m.WF
⊢ (m.modify k f).getD k fallback = (Option.map f (m.get? k)).getD fallback

Tactic:
simp_to_raw using Raw₀.getD_modify_self

Result:
no goals
-- Mathlib/Data/Countable/Small.lean
theorem Uncountable.of_not_small {α : Type v} (h : ¬ Small.{w} α) : Uncountable α

Proof state:
α : Type v
h : ¬Small.{w, v} α
⊢ Uncountable α

Tactic:
rw [uncountable_iff_not_countable]

Result:
α : Type v
h : ¬Small.{w, v} α
⊢ ¬Countable α

Proof state:
α : Type v
h : ¬Small.{w, v} α
⊢ ¬Countable α

Tactic:
exact mt (@Countable.toSmall α) h

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem isIso_of_subset {X Y : PresheafedSpace C} (f : X ⟶ Y)
    [H : PresheafedSpace.IsOpenImmersion f] (U : Opens Y.carrier)
    (hU : (U : Set Y.carrier) ⊆ Set.range f.base) : IsIso (f.c.app <| op U)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (f.c.app (op U))

Tactic:
have : U = H.base_open.isOpenMap.functor.obj ((Opens.map f.base).obj U) := by
  ext1
  exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : U = ⋯.functor.obj ((Opens.map f.base).obj U)
⊢ IsIso (f.c.app (op U))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ U = ⋯.functor.obj ((Opens.map f.base).obj U)

Tactic:
ext1

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ ↑U = ↑(⋯.functor.obj ((Opens.map f.base).obj U))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this : U = ⋯.functor.obj ((Opens.map f.base).obj U)
⊢ IsIso (f.c.app (op U))

Tactic:
convert H.c_iso ((Opens.map f.base).obj U)

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ ↑U = ↑(⋯.functor.obj ((Opens.map f.base).obj U))

Tactic:
exact (Set.inter_eq_left.mpr hU).symm.trans Set.image_preimage_eq_inter_range.symm

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem map_id : ∀ s : Seq α, map id s = s
  | ⟨s, al⟩ => by
    apply Subtype.eq; dsimp [map]
    rw [Option.map_id, Stream'.map_id]

Proof state:
case a
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map id) s = s

Tactic:
rw [Option.map_id, Stream'.map_id]

Result:
no goals

Proof state:
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ map id ⟨s, al⟩ = ⟨s, al⟩

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map id ⟨s, al⟩) = ↑⟨s, al⟩

Proof state:
case a
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map id ⟨s, al⟩) = ↑⟨s, al⟩

Tactic:
dsimp [map]

Result:
case a
α : Type u
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map id) s = s
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldr_cons (t : RBNode.Stream α) (l) : t.foldr (·::·) l = t.toList ++ l

Proof state:
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t l = foldr (fun x1 x2 => x1 :: x2) t [] ++ l

Tactic:
apply Eq.symm

Result:
case h
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t [] ++ l = foldr (fun x1 x2 => x1 :: x2) t l

Proof state:
case h
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t [] ++ l = foldr (fun x1 x2 => x1 :: x2) t l

Tactic:
induction t <;> simp [*, foldr, RBNode.foldr_cons]

Result:
no goals

Proof state:
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t l = t.toList ++ l

Tactic:
unfold toList

Result:
α : Type u_1
t : RBNode.Stream α
l : List α
⊢ foldr (fun x1 x2 => x1 :: x2) t l = foldr (fun x1 x2 => x1 :: x2) t [] ++ l
-- Mathlib/RingTheory/Localization/Module.lean
@[simp]
lemma LocalizedModule.map_mk (f : M →ₗ[R] N) (x y) :
    map S f (.mk x y) = LocalizedModule.mk (f x) y

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ ((map S) f) (IsLocalizedModule.mk' (mkLinearMap S M) x y) = IsLocalizedModule.mk' (mkLinearMap S N) (f x) y

Tactic:
exact IsLocalizedModule.map_mk' _ _ _ _ _ _

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ ((map S) f) (mk x y) = mk (f x) y

Tactic:
rw [IsLocalizedModule.mk_eq_mk', IsLocalizedModule.mk_eq_mk']

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ ((map S) f) (IsLocalizedModule.mk' (mkLinearMap S M) x y) = IsLocalizedModule.mk' (mkLinearMap S N) (f x) y
-- Mathlib/Order/SupClosed.lean
@[simp] lemma latticeClosure_univ : latticeClosure (Set.univ : Set α) = Set.univ

Proof state:
α : Type u_3
inst✝ : Lattice α
⊢ latticeClosure Set.univ = Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem ite_none_left_eq_some {p : Prop} [Decidable p] {b : Option β} :
    (if p then none else b) = some a ↔ ¬ p ∧ b = some a

Proof state:
β : Type u_1
a : β
p : Prop
inst✝ : Decidable p
b : Option β
⊢ (if p then none else b) = some a ↔ ¬p ∧ b = some a

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem mem_support_append_iff {t u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support

Proof state:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Tactic:
obtain rfl | h := eq_or_ne t v <;> obtain rfl | h' := eq_or_ne t u <;>
  (try have := h'.symm) <;> simp [*]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support

Tactic:
simp only [mem_support_iff, mem_tail_support_append_iff]

Result:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Proof state:
case inr.inr
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Tactic:
have := h'.symm

Result:
case inr.inr
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
this : u ≠ t
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Proof state:
case inr.inr
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail

Tactic:
try have := h'.symm

Result:
case inr.inr
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
h : t ≠ v
h' : t ≠ u
this : u ≠ t
⊢ t = u ∨ t ∈ p.support.tail ∨ t ∈ p'.support.tail ↔ (t = u ∨ t ∈ p.support.tail) ∨ t = v ∨ t ∈ p'.support.tail
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_lt_lowerCrossingTime (hab : a < b)
    (hn : lowerCrossingTime a b f N (n + 1) ω ≠ N) :
    upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
⊢ upperCrossingTime a b f N (n + 1) ω < lowerCrossingTime a b f N (n + 1) ω

Tactic:
refine lt_of_le_of_ne upperCrossingTime_le_lowerCrossingTime fun h =>
  not_le.2 hab <| le_trans ?_ (stoppedValue_lowerCrossingTime hn)

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ stoppedValue f (lowerCrossingTime a b f N (n + 1)) ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ stoppedValue f (lowerCrossingTime a b f N (n + 1)) ω

Tactic:
simp only [stoppedValue]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (lowerCrossingTime a b f N (n + 1) ω) ω

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (upperCrossingTime a b f N (n + 1) ω) ω

Tactic:
exact stoppedValue_upperCrossingTime (h.symm ▸ hn)

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (lowerCrossingTime a b f N (n + 1) ω) ω

Tactic:
rw [← h]

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (upperCrossingTime a b f N (n + 1) ω) ω
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma μ_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) :
    F.obj X' ◁ F.map f ≫ μ F X' Y = μ F X' X ≫ F.map (X' ◁ f)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y X' : C
f : X ⟶ Y
⊢ F.obj X' ◁ F.map f ≫ μ F X' Y = μ F X' X ≫ F.map (X' ◁ f)

Tactic:
apply μ'_natural_right

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Prod.lean
theorem sup_inf_sup (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
    s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2

Proof state:
α : Type u_2
ι : Type u_5
κ : Type u_6
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
⊢ s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2

Tactic:
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]

Result:
no goals