harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem locallyRingedSpace_toLocallyRingedSpace {X Y : LocallyRingedSpace} (f : X ⟶ Y)
    [LocallyRingedSpace.IsOpenImmersion f] : toLocallyRingedSpace Y f.1 = X

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
inst✝ : LocallyRingedSpace.IsOpenImmersion f
⊢ toLocallyRingedSpace Y f.toHom = X

Tactic:
cases X

Result:
case mk
Y : LocallyRingedSpace
toSheafedSpace✝ : SheafedSpace CommRingCat
isLocalRing✝ : ∀ (x : ↑↑toSheafedSpace✝.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace✝.presheaf.stalk x)
f : { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ } ⟶ Y
inst✝ : LocallyRingedSpace.IsOpenImmersion f
⊢ toLocallyRingedSpace Y f.toHom = { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ }

Proof state:
case mk
Y : LocallyRingedSpace
toSheafedSpace✝ : SheafedSpace CommRingCat
isLocalRing✝ : ∀ (x : ↑↑toSheafedSpace✝.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace✝.presheaf.stalk x)
f : { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ } ⟶ Y
inst✝ : LocallyRingedSpace.IsOpenImmersion f
⊢ { toSheafedSpace := toSheafedSpace Y.toSheafedSpace f.toHom, isLocalRing := ⋯ } =
    { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ }

Tactic:
simp

Result:
no goals

Proof state:
case mk
Y : LocallyRingedSpace
toSheafedSpace✝ : SheafedSpace CommRingCat
isLocalRing✝ : ∀ (x : ↑↑toSheafedSpace✝.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace✝.presheaf.stalk x)
f : { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ } ⟶ Y
inst✝ : LocallyRingedSpace.IsOpenImmersion f
⊢ toLocallyRingedSpace Y f.toHom = { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ }

Tactic:
delta toLocallyRingedSpace

Result:
case mk
Y : LocallyRingedSpace
toSheafedSpace✝ : SheafedSpace CommRingCat
isLocalRing✝ : ∀ (x : ↑↑toSheafedSpace✝.toPresheafedSpace), IsLocalRing ↑(toSheafedSpace✝.presheaf.stalk x)
f : { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ } ⟶ Y
inst✝ : LocallyRingedSpace.IsOpenImmersion f
⊢ { toSheafedSpace := toSheafedSpace Y.toSheafedSpace f.toHom, isLocalRing := ⋯ } =
    { toSheafedSpace := toSheafedSpace✝, isLocalRing := isLocalRing✝ }
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioc_sub_one_right_eq_Ioo (a b : α) : Ioc a (b - 1) = Ioo a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
⊢ Ioc a (b - 1) = Ioo a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_right_eq_Ioo a b

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
    Disjoint (single i b).support (single j b').support ↔ i ≠ j

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
b b' : M
hb : b ≠ 0
hb' : b' ≠ 0
i j : α
⊢ Disjoint (single i b).support (single j b').support ↔ i ≠ j

Tactic:
rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem mem_ball_self (hr : 0 < r) : x ∈ ball p x r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ x ∈ p.ball x r

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem sumCongr_refl : sumCongr (.refl X) (.refl Y) = .refl (X ⊕ Y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (Homeomorph.refl X).sumCongr (Homeomorph.refl Y) = Homeomorph.refl (X ⊕ Y)

Tactic:
ext i

Result:
case H
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : X ⊕ Y
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) i = (Homeomorph.refl (X ⊕ Y)) i

Proof state:
case H
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : X ⊕ Y
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) i = (Homeomorph.refl (X ⊕ Y)) i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem suffixLevenshtein_nil_nil : (suffixLevenshtein C [] []).1 = [0]

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
⊢ (suffixLevenshtein C [] []).val = [0]

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem lt_csSup_iff' (hb : BddAbove s) : a < sSup s ↔ ∃ b ∈ s, a < b

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
a : α
hb : BddAbove s
⊢ a < sSup s ↔ ∃ b ∈ s, a < b

Tactic:
simpa only [not_le, not_forall₂, exists_prop] using (csSup_le_iff' hb).not

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Set.Finite.closure_sUnion {S : Set (Set X)} (hS : S.Finite) :
    closure (⋃₀ S) = ⋃ s ∈ S, closure s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ closure (⋃₀ S) = ⋃ s ∈ S, closure s

Tactic:
rw [sUnion_eq_biUnion, hS.closure_biUnion]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sOppSide_iff_exists_right {s : AffineSubspace R P} {x y p₂ : P} (h : p₂ ∈ s) :
    s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rw [SOppSide, and_comm, wOppSide_iff_exists_right h, and_assoc, and_congr_right_iff,
  and_congr_right_iff]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ x ∉ s → y ∉ s → ((y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
a✝ : x ∉ s
hy : y ∉ s
⊢ (y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)

Tactic:
rw [or_iff_right hy]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
⊢ x ∉ s → y ∉ s → ((y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))

Tactic:
rintro _ hy

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₂ : P
h : p₂ ∈ s
a✝ : x ∉ s
hy : y ∉ s
⊢ (y ∈ s ∨ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)) ↔ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) {hc : k' ∈ m.alter k f} :
    (m.alter k f).get k' hc =
      if heq : k == k' then
        haveI h' : (f (m.get? k)).isSome := mem_alter_of_beq h heq |>.mp hc
        cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get <| h'
      else
        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
        m.get k' h'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc✝ : k' ∈ m.alter k f
hc : (m.alter k f).contains k' = true
⊢ (m.alter k f).get k' hc✝ = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯

Tactic:
revert hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k' ∈ m.alter k f
⊢ (m.alter k f).contains k' = true →
    (m.alter k f).get k' hc = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k' ∈ m.alter k f
⊢ (m.alter k f).get k' hc = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc✝ : k' ∈ m.alter k f
hc : (m.alter k f).contains k' = true
⊢ (m.alter k f).get k' hc✝ = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k' ∈ m.alter k f
⊢ (m.alter k f).contains k' = true →
    (m.alter k f).get k' hc = if heq : (k == k') = true then cast ⋯ ((f (m.get? k)).get ⋯) else m.get k' ⋯

Tactic:
simp_to_raw using Raw₀.get_alter

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli_zero : bernoulli 0 = 1

Proof state:
⊢ bernoulli 0 = 1

Tactic:
simp [bernoulli]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp] lemma uIoc_of_le (h : a ≤ b) : Ι a b = Ioc a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ Ι a b = Ioc a b

Tactic:
simp [uIoc, h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma removeNth_last {α : Type*} (f : Fin (n + 1) → α) : removeNth (last n) f = init f

Proof state:
case h
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
x✝ : Fin n
⊢ (last n).removeNth f x✝ = init f x✝

Tactic:
simp [init, removeNth]

Result:
no goals

Proof state:
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
⊢ (last n).removeNth f = init f

Tactic:
ext

Result:
case h
n : ℕ
α : Type u_3
f : Fin (n + 1) → α
x✝ : Fin n
⊢ (last n).removeNth f x✝ = init f x✝
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
lemma map_injective_iff (F : C ⥤ D) [Faithful F] {X Y : C} (f g : X ⟶ Y) :
    F.map f = F.map g ↔ f = g :=
  ⟨fun h => F.map_injective h, fun h => by rw [h]⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
rw [h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableAtFilter.sup_iff {l l' : Filter α} :
    IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

Tactic:
constructor

Result:
case mp
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ → IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

case mpr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ

Proof state:
case mpr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ

Tactic:
exact fun ⟨⟨s, hsl, hs⟩, ⟨t, htl, ht⟩⟩ ↦ ⟨s ∪ t, union_mem_sup hsl htl, hs.union ht⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ → IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ

Tactic:
exact fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_sub_const [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b]
    (f : F) (x : G) : f (x - a) = f x - b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f (x - a) = f x - b

Tactic:
simpa using map_sub_nsmul f x 1

Result:
no goals
-- Mathlib/Order/Chain.lean
lemma IsChain.le_of_not_lt [Preorder α] (hs : IsChain (· ≤ ·) s)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬ x < y) : y ≤ x

Proof state:
case inr
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 => x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : y ≤ x
⊢ y ≤ x

Tactic:
exact h'

Result:
no goals

Proof state:
case inl
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 => x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
h' : x ≤ y
⊢ y ≤ x

Tactic:
simpa [lt_iff_le_not_le, h'] using h

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 => x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
⊢ y ≤ x

Tactic:
cases hs.total hx hy with
| inr h' => exact h'
| inl h' => simpa [lt_iff_le_not_le, h'] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem lt_of_mul_lt_mul_right {a b c : Int} (w : b * a < c * a) (h : 0 ≤ a) : b < c

Proof state:
a b c : Int
w : a * b < a * c
h : 0 ≤ a
⊢ b < c

Tactic:
exact lt_of_mul_lt_mul_left w h

Result:
no goals

Proof state:
a b c : Int
w : b * a < c * a
h : 0 ≤ a
⊢ b < c

Tactic:
rw [Int.mul_comm b, Int.mul_comm c] at w

Result:
a b c : Int
w : a * b < a * c
h : 0 ≤ a
⊢ b < c
-- Mathlib/Data/Nat/Pairing.lean
theorem iUnion_unpair_prod {α β} {s : ℕ → Set α} {t : ℕ → Set β} :
    ⋃ n : ℕ, s n.unpair.fst ×ˢ t n.unpair.snd = (⋃ n, s n) ×ˢ ⋃ n, t n

Proof state:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = ⋃ x, s x.1 ×ˢ t x.2

Tactic:
exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = (⋃ n, s n) ×ˢ ⋃ n, t n

Tactic:
rw [← Set.iUnion_prod]

Result:
α : Type u_1
β : Type u_2
s : ℕ → Set α
t : ℕ → Set β
⊢ ⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = ⋃ x, s x.1 ×ˢ t x.2
-- Mathlib/Data/Fintype/Order.lean
lemma Set.Finite.exists_minimal_le {s : Set α} (hs : s.Finite) (h : a ∈ s) :
    ∃ b, b ≤ a ∧ Minimal (· ∈ s) b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
hs : s.Finite
h : a ∈ s
⊢ ∃ b ≤ a, Minimal (fun x => x ∈ s) b

Tactic:
obtain ⟨b, lb, minb⟩ := hs.toFinset.exists_minimal_le (hs.mem_toFinset.mpr h)

Result:
case intro.intro
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
hs : s.Finite
h : a ∈ s
b : α
lb : b ≤ a
minb : Minimal (fun x => x ∈ hs.toFinset) b
⊢ ∃ b ≤ a, Minimal (fun x => x ∈ s) b

Proof state:
case right
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
hs : s.Finite
h : a ∈ s
b : α
lb : b ≤ a
minb : Minimal (fun x => x ∈ hs.toFinset) b
⊢ Minimal (fun x => x ∈ s) b

Tactic:
simpa using minb

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
hs : s.Finite
h : a ∈ s
b : α
lb : b ≤ a
minb : Minimal (fun x => x ∈ hs.toFinset) b
⊢ ∃ b ≤ a, Minimal (fun x => x ∈ s) b

Tactic:
use b, lb

Result:
case right
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
hs : s.Finite
h : a ∈ s
b : α
lb : b ≤ a
minb : Minimal (fun x => x ∈ hs.toFinset) b
⊢ Minimal (fun x => x ∈ s) b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_right_comm : ∀ (x y z : Bool), ((x || y) || z) = ((x || z) || y)

Proof state:
⊢ ∀ (x y z : Bool), (x || y || z) = (x || z || y)

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.repr_ker : LinearMap.ker hv.repr = ⊥

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
⊢ LinearMap.ker hv.repr = ⊥

Tactic:
rw [LinearIndependent.repr, LinearEquiv.ker]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem isOption_neg_neg {x y : PGame} : IsOption (-x) (-y) ↔ IsOption x y

Proof state:
x y : PGame
⊢ (-x).IsOption (-y) ↔ x.IsOption y

Tactic:
rw [isOption_neg, neg_neg]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.exists_isBasis_inter_eq_of_superset (hI : M.IsBasis I X) (hXY : X ⊆ Y)
    (hY : Y ⊆ M.E

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J ∩ X ⊆ I

Tactic:
exact fun e he ↦ hI.mem_of_insert_indep he.2 (hJ.indep.subset (insert_subset he.1 hIJ))

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ J, M.IsBasis J Y ∧ J ∩ X = I

Tactic:
refine ⟨J, hJ, subset_antisymm ?_ (subset_inter hIJ hI.subset)⟩

Result:
case intro.intro
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ J ∩ X ⊆ I

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ ∃ J, M.IsBasis J Y ∧ J ∩ X = I

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans hXY)

Result:
case intro.intro
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
hY : autoParam (Y ⊆ M.E) _auto✝
J : Set α
hJ : M.IsBasis J Y
hIJ : I ⊆ J
⊢ ∃ J, M.IsBasis J Y ∧ J ∩ X = I
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_empty (f : α →ₛ β) : restrict f ∅ = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
⊢ f.restrict ∅ = 0

Tactic:
simp [restrict]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_pow_atTop_iff :
    Tendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
h : Tendsto (fun x => c * x ^ 0) atTop atTop
⊢ False

Tactic:
simp only [pow_zero, not_tendsto_const_atTop] at h

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
k : α
hck : 0 < c * k ^ n
hk : 0 ≤ k
⊢ 0 < c

Tactic:
exact pos_of_mul_pos_left hck (pow_nonneg hk _)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ 0 < c

Tactic:
rcases ((h.eventually_gt_atTop 0).and (eventually_ge_atTop 0)).exists with ⟨k, hck, hk⟩

Result:
case refine_2.intro.intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
k : α
hck : 0 < c * k ^ n
hk : 0 ≤ k
⊢ 0 < c

Proof state:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
h : Tendsto (fun x => c * x ^ 0) atTop atTop
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
n : ℕ
⊢ Tendsto (fun x => c * x ^ n) atTop atTop ↔ n ≠ 0 ∧ 0 < c

Tactic:
refine ⟨fun h => ⟨?_, ?_⟩, fun h => tendsto_const_mul_pow_atTop h.1 h.2⟩

Result:
case refine_1
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ n ≠ 0

case refine_2
α : Type u_1
inst✝ : LinearOrderedSemifield α
c : α
n : ℕ
h : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ 0 < c
-- Mathlib/CategoryTheory/CommSq.lean
theorem iff : HasLift sq ↔ Nonempty sq.LiftStruct

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ Nonempty sq.LiftStruct

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift → Nonempty sq.LiftStruct

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct → sq.HasLift

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift → Nonempty sq.LiftStruct

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct → sq.HasLift

Tactic:
exacts [fun h => h.exists_lift, fun h => mk h]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem mem_iff_iSup_of_isClosed (hs : IsClosed s) :
    a ∈ s ↔ ∃ (ι : Type u) (_hι : Nonempty ι) (f : ι → Ordinal),
      (∀ i, f i ∈ s) ∧ ⨆ i, f i = a

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
hs : IsClosed s
⊢ a ∈ s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
rw [← mem_closure_iff_iSup, hs.closure_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem inductionOn₂
    {motive : Quotient s₁ → Quotient s₂ → Prop}
    (q₁ : Quotient s₁)
    (q₂ : Quotient s₂)
    (h : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))
    : motive q₁ q₂

Proof state:
case a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
q₂ : Quotient s₂
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂

Tactic:
induction q₂ using Quotient.ind

Result:
case a.a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝)

Proof state:
case a.a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
a✝¹ : α
a✝ : β
⊢ motive (Quotient.mk s₁ a✝¹) (Quotient.mk s₂ a✝)

Tactic:
apply h

Result:
no goals

Proof state:
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
q₁ : Quotient s₁
q₂ : Quotient s₂
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
⊢ motive q₁ q₂

Tactic:
induction q₁ using Quotient.ind

Result:
case a
α : Sort uA
β : Sort uB
s₁ : Setoid α
s₂ : Setoid β
motive : Quotient s₁ → Quotient s₂ → Prop
q₂ : Quotient s₂
h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)
a✝ : α
⊢ motive (Quotient.mk s₁ a✝) q₂
-- Mathlib/Algebra/DirectSum/Module.lean
theorem linearEquivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : M i) :
    (linearEquivFunOnFintype R ι M).symm (Pi.single i m) = lof R ι M i m

Proof state:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ DFinsupp.equivFunOnFintype.symm (Pi.single i m) = (lof R ι M i) m

Tactic:
rw [DFinsupp.equivFunOnFintype_symm_single i m]

Result:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ DFinsupp.single i m = (lof R ι M i) m

Proof state:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ DFinsupp.single i m = (lof R ι M i) m

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ (linearEquivFunOnFintype R ι M).symm (Pi.single i m) = (lof R ι M i) m

Tactic:
change (DFinsupp.equivFunOnFintype.symm (Pi.single i m)) = _

Result:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ DFinsupp.equivFunOnFintype.symm (Pi.single i m) = (lof R ι M i) m