harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Bases.lean
theorem inf_neBot_iff_frequently_right {f g : Filter α} :
    NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in g, p x) → ∃ᶠ x in f, p x

Proof state:
α : Type u_1
f g : Filter α
⊢ (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Tactic:
rw [inf_comm]

Result:
α : Type u_1
f g : Filter α
⊢ (g ⊓ f).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Proof state:
α : Type u_1
f g : Filter α
⊢ (g ⊓ f).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

Tactic:
exact inf_neBot_iff_frequently_left

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem head_some_of_head_tail_some {s : WSeq α} {a} (h : some a ∈ head (tail s)) :
    ∃ a', some a' ∈ head s

Proof state:
α : Type u
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) s.tail.destruct
⊢ ∃ a', some a' ∈ s.head

Tactic:
rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩

Result:
case intro.intro
α : Type u
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) s.tail.destruct
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head

Proof state:
α : Type u
s : WSeq α
a : α
h : some a ∈ s.tail.head
⊢ ∃ a', some a' ∈ s.head

Tactic:
unfold head at h

Result:
α : Type u
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) s.tail.destruct
⊢ ∃ a', some a' ∈ s.head

Proof state:
case intro.intro
α : Type u
s : WSeq α
a : α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) s.tail.destruct
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head

Tactic:
clear h

Result:
case intro.intro
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head

Proof state:
case intro.intro.some
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
h' : o.fst = a
⊢ ∃ a', some a' ∈ s.head

Tactic:
clear h'

Result:
case intro.intro.some
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
⊢ ∃ a', some a' ∈ s.head

Proof state:
case intro.intro.some
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
⊢ ∃ a', some a' ∈ s.head

Tactic:
obtain ⟨a, am⟩ := destruct_some_of_destruct_tail_some md

Result:
case intro.intro.some.intro
α : Type u
s : WSeq α
a✝ : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
a : α × WSeq α
am : some a ∈ s.destruct
⊢ ∃ a', some a' ∈ s.head

Proof state:
case intro.intro
α : Type u
s : WSeq α
a : α
o : Option (α × WSeq α)
md : o ∈ s.tail.destruct
e : Prod.fst <$> o = some a
⊢ ∃ a', some a' ∈ s.head

Tactic:
rcases o with - | o <;> [injection e; injection e with h']

Result:
case intro.intro.some
α : Type u
s : WSeq α
a : α
o : α × WSeq α
md : some o ∈ s.tail.destruct
h' : o.fst = a
⊢ ∃ a', some a' ∈ s.head
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem Nat.sub_mul_eq_mod_of_lt_of_le (hlo : w * n ≤ i) (hhi : i < w * (n + 1)) :
    i - w * n = i % w

Proof state:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i < (n + 1) * w

Tactic:
rw [Nat.mul_comm]

Result:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i < w * (n + 1)

Proof state:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ n * w ≤ i

Tactic:
rw [Nat.mul_comm]

Result:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ w * n ≤ i

Proof state:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ w * n ≤ i

Tactic:
omega

Result:
no goals

Proof state:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i - w * n = i - w * (i / w)

Tactic:
congr

Result:
case e_a.e_a
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ n = i / w

Proof state:
case e_a.e_a
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i / w = n

Tactic:
apply Nat.div_eq_of_lt_le
  (by rw [Nat.mul_comm]; omega)
  (by rw [Nat.mul_comm]; omega)

Result:
no goals

Proof state:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i < w * (n + 1)

Tactic:
omega

Result:
no goals

Proof state:
case e_a.e_a
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ n = i / w

Tactic:
symm

Result:
case e_a.e_a
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i / w = n

Proof state:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i - w * n = i % w

Tactic:
rw [Nat.mod_def]

Result:
w n i : Nat
hlo : w * n ≤ i
hhi : i < w * (n + 1)
⊢ i - w * n = i - w * (i / w)
-- Mathlib/Data/List/Lex.lean
theorem cons_iff {r : α → α → Prop} [IsIrrefl α r] {a l₁ l₂} :
    Lex r (a :: l₁) (a :: l₂) ↔ Lex r l₁ l₂ :=
  ⟨fun h => by obtain - | h | h := h; exacts [h, (irrefl_of r a h).elim], Lex.cons⟩

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂

Tactic:
obtain - | h | h := h

Result:
case cons
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂

case rel
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂

case rel
α : Type u
r : α → α → Prop
inst✝ : IsIrrefl α r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

Tactic:
exacts [h, (irrefl_of r a h).elim]

Result:
no goals
-- Mathlib/Algebra/GradedMonoid.lean
theorem GradedMonoid.mk_list_dProd (l : List α) (fι : α → ι) (fA : ∀ a, A (fι a)) :
    GradedMonoid.mk _ (l.dProd fι fA) = (l.map fun a => GradedMonoid.mk (fι a) (fA a)).prod

Proof state:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk (l.dProdIndex fι) (l.dProd fι fA) = (List.map (fun a => mk (fι a) (fA a)) l).prod

Tactic:
match l with
| [] => simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]; rfl
| head::tail =>
  simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk ([].dProdIndex fι) ([].dProd fι fA) = (List.map (fun a => mk (fι a) (fA a)) []).prod

Tactic:
simp only [List.dProdIndex_nil, List.dProd_nil, List.map_nil, List.prod_nil]

Result:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1

Proof state:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
⊢ mk ((head :: tail).dProdIndex fι) ((head :: tail).dProd fι fA) =
    (List.map (fun a => mk (fι a) (fA a)) (head :: tail)).prod

Tactic:
simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
/-- The formula `ψ(P₁ + P₂) = (ψ(P₂)(x(P₁) - x(P₃)) - ψ(P₁)(x(P₂) - x(P₃))) / (x(P₂) - x(P₁))`,
where `ψ(x,y) = 2y + a₁x + a₃`. -/
lemma addY_sub_negY_addY {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
    let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)
    let y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)
    y₃ - W.negY x₃ y₃ =
      ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁)

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
  let y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂);
  y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁)

Tactic:
simp_rw [addY, negY, eq_div_iff (sub_ne_zero.mpr hx.symm)]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
        (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
            W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
          W.a₃)) *
      (x₂ - x₁) =
    (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
        (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
            W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
          W.a₃)) *
      (x₂ - x₁) =
    (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))

Tactic:
linear_combination (norm := ring1) 2 * cyclic_sum_Y_mul_X_sub_X y₁ y₂ hx

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem injective_comp (h : N ≃[L] P) :
    Function.Injective (h.comp : (M ≃[L] N) →  (M ≃[L] P))

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x

Tactic:
exact h.injective (congr_fun (congr_arg DFunLike.coe hfg) x)

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
⊢ f = g

Tactic:
ext x

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
x : M
⊢ f x = g x

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
⊢ Function.Injective h.comp

Tactic:
intro f g hfg

Result:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
hfg : h.comp f = h.comp g
⊢ f = g
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem sepDegree_bot : sepDegree F (⊥ : IntermediateField F E) = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
⊢ sepDegree F ↥⊥ = 1

Tactic:
rwa [sepDegree_self, Cardinal.lift_one, ← Cardinal.lift_one.{v, u}, Cardinal.lift_inj] at this

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ sepDegree F ↥⊥ = 1

Tactic:
have := lift_sepDegree_eq_of_equiv _ _ _ (botEquiv F E)

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
this : Cardinal.lift.{u, v} (sepDegree F ↥⊥) = Cardinal.lift.{v, u} (sepDegree F F)
⊢ sepDegree F ↥⊥ = 1
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_C {x : R} (hx : x ≠ 0) : integralNormalization (C x) = 1

Proof state:
R : Type u
inst✝ : Semiring R
x : R
hx : x ≠ 0
⊢ (C x).integralNormalization = 1

Tactic:
simp [integralNormalization, sum_def, support_C hx, degree_C hx]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem fst_eq_coprod : fst R M M₂ = coprod LinearMap.id 0

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ fst R M M₂ = id.coprod 0

Tactic:
ext

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (fst R M M₂) x✝ = (id.coprod 0) x✝

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (fst R M M₂) x✝ = (id.coprod 0) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} :
    (m.insert k v).contains a = ((k == a) || m.contains a)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β k
⊢ (m.insert k v).contains a = (k == a || m.contains a)

Tactic:
simp_to_model [insert] using List.containsKey_insertEntry

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma parallelComp_comp_parallelComp {η : Kernel β γ} [IsSFiniteKernel η]
    {κ' : Kernel α' β'} [IsSFiniteKernel κ'] {η' : Kernel β' γ'} [IsSFiniteKernel η'] :
    (η ∥ₖ η') ∘ₖ (κ ∥ₖ κ') = (η ∘ₖ κ) ∥ₖ (η' ∘ₖ κ')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
α' : Type u_5
β' : Type u_6
γ' : Type u_7
mα' : MeasurableSpace α'
mβ' : MeasurableSpace β'
mγ' : MeasurableSpace γ'
inst✝³ : IsSFiniteKernel κ
η : Kernel β γ
inst✝² : IsSFiniteKernel η
κ' : Kernel α' β'
inst✝¹ : IsSFiniteKernel κ'
η' : Kernel β' γ'
inst✝ : IsSFiniteKernel η'
⊢ η ∥ₖ η' ∘ₖ (κ ∥ₖ κ') = η ∘ₖ κ ∥ₖ (η' ∘ₖ κ')

Tactic:
rw [← parallelComp_id_left_comp_parallelComp, ← parallelComp_id_right_comp_parallelComp,
  ← comp_assoc, parallelComp_id_left_comp_parallelComp, comp_id]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem restrict_withDensity' [SFinite μ] (s : Set α) (f : α → ℝ≥0∞) :
    (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
⊢ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f

Tactic:
ext1 t ht

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ ((μ.withDensity f).restrict s) t = ((μ.restrict s).withDensity f) t

Tactic:
rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s),
  restrict_restrict ht]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P3_of_le_left {y₁ y₂} (i) (h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂) (hl : x₁ ≤ x₂.moveLeft i) :
    P3 x₁ x₂ y₁ y₂

Proof state:
case inl
x₁ x₂ y₁ y₂ : PGame
i : x₂.LeftMoves
h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hl✝ : x₁ ≤ x₂.moveLeft i
hl : x₁ < x₂.moveLeft i
⊢ P3 x₁ x₂ y₁ y₂

Tactic:
exact (h.2.2.2 hl).trans h.2.2.1

Result:
no goals

Proof state:
case inr
x₁ x₂ y₁ y₂ : PGame
i : x₂.LeftMoves
h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hl : x₁ ≤ x₂.moveLeft i
he : x₁ ≈ x₂.moveLeft i
⊢ P3 x₁ x₂ y₁ y₂

Tactic:
rw [P3, h.1 he, h.2.1 he]

Result:
case inr
x₁ x₂ y₁ y₂ : PGame
i : x₂.LeftMoves
h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hl : x₁ ≤ x₂.moveLeft i
he : x₁ ≈ x₂.moveLeft i
⊢ ⟦x₂.moveLeft i * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₂.moveLeft i * y₁⟧ + ⟦x₂ * y₂⟧

Proof state:
case inr
x₁ x₂ y₁ y₂ : PGame
i : x₂.LeftMoves
h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hl : x₁ ≤ x₂.moveLeft i
he : x₁ ≈ x₂.moveLeft i
⊢ ⟦x₂.moveLeft i * y₂⟧ + ⟦x₂ * y₁⟧ < ⟦x₂.moveLeft i * y₁⟧ + ⟦x₂ * y₂⟧

Tactic:
exact h.2.2.1

Result:
no goals

Proof state:
x₁ x₂ y₁ y₂ : PGame
i : x₂.LeftMoves
h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hl : x₁ ≤ x₂.moveLeft i
⊢ P3 x₁ x₂ y₁ y₂

Tactic:
obtain (hl|he) := lt_or_equiv_of_le hl

Result:
case inl
x₁ x₂ y₁ y₂ : PGame
i : x₂.LeftMoves
h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hl✝ : x₁ ≤ x₂.moveLeft i
hl : x₁ < x₂.moveLeft i
⊢ P3 x₁ x₂ y₁ y₂

case inr
x₁ x₂ y₁ y₂ : PGame
i : x₂.LeftMoves
h : IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂
hl : x₁ ≤ x₂.moveLeft i
he : x₁ ≈ x₂.moveLeft i
⊢ P3 x₁ x₂ y₁ y₂
-- Mathlib/Probability/Moments/Basic.lean
/-- The moment generating function is monotone in the random variable for `t ≥ 0`. -/
lemma mgf_mono_of_nonneg {Y : Ω → ℝ} (hXY : X ≤ᵐ[μ] Y) (ht : 0 ≤ t)
    (htY : Integrable (fun ω ↦ exp (t * Y ω)) μ) :
    mgf X μ t ≤ mgf Y μ t

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
rw [mgf_undef htX]

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ 0 ≤ mgf Y μ t

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ 0 ≤ mgf Y μ t

Tactic:
exact mgf_nonneg

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (fun ω => rexp (t * X ω)) ≤ᶠ[ae μ] fun ω => rexp (t * Y ω)

Tactic:
filter_upwards [hXY] with ω hω using by gcongr

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : Integrable (fun ω => rexp (t * X ω)) μ
ω : Ω
hω : X ω ≤ Y ω
⊢ rexp (t * X ω) ≤ rexp (t * Y ω)

Tactic:
gcongr

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
by_cases htX : Integrable (fun ω ↦ exp (t * X ω)) μ

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : ¬Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : Integrable (fun ω => rexp (t * X ω)) μ
⊢ mgf X μ t ≤ mgf Y μ t

Tactic:
refine integral_mono_ae htX htY ?_

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : 0 ≤ t
htY : Integrable (fun ω => rexp (t * Y ω)) μ
htX : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (fun ω => rexp (t * X ω)) ≤ᶠ[ae μ] fun ω => rexp (t * Y ω)
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap_comap_eq_relrank_of_le
    {L : Type v} [Field L] (f : L →+* E) (h : B ≤ f.fieldRange) :
    relrank (A.comap f) (B.comap f) = relrank A B

Proof state:
E : Type v
inst✝¹ : Field E
A B : Subfield E
L : Type v
inst✝ : Field L
f : L →+* E
h : B ≤ f.fieldRange
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h

Result:
no goals
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem _root_.Algebra.lmul_injective : Function.Injective (Algebra.lmul R A) :=
  fun a₁ a₂ h ↦ by simpa using DFunLike.congr_fun h 1

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
h : (Algebra.lmul R A) a₁ = (Algebra.lmul R A) a₂
⊢ a₁ = a₂

Tactic:
simpa using DFunLike.congr_fun h 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Instances.lean
theorem some_inj {a b : α} : some a = some b ↔ a = b

Proof state:
α : Type u_1
a b : α
⊢ some a = some b ↔ a = b

Tactic:
simp

Result:
α : Type u_1
a b : α
⊢ a = b ↔ a = b

Proof state:
α : Type u_1
a b : α
⊢ a = b ↔ a = b

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_modify [LawfulBEq α] {k k': α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).contains k' = m.contains k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).contains k' = m.contains k'

Tactic:
simp_to_raw using Raw₀.contains_modify

Result:
no goals
-- Mathlib/Algebra/Group/Ext.lean
theorem DivInvMonoid.ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄
    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))
    (h_inv : (letI := m₁; Inv.inv : M → M) = (letI := m₂; Inv.inv : M → M)) : m₁ = m₂

Proof state:
case mk.mk.mk.mk.mk.mk
M : Type u_1
toMonoid✝¹ : Monoid M
zpow✝¹ : ℤ → M → M
zpow_zero'✝¹ : ∀ (a : M), zpow✝¹ 0 a = 1
zpow_succ'✝¹ : ∀ (n : ℕ) (a : M), zpow✝¹ (↑n.succ) a = zpow✝¹ (↑n) a * a
inv✝¹ : M → M
zpow_neg'✝¹ : ∀ (n : ℕ) (a : M), zpow✝¹ (Int.negSucc n) a = (zpow✝¹ (↑n.succ) a)⁻¹
div✝¹ : M → M → M
div_eq_mul_inv✝¹ : ∀ (a b : M), a / b = a * b⁻¹
toMonoid✝ : Monoid M
zpow✝ : ℤ → M → M
zpow_zero'✝ : ∀ (a : M), zpow✝ 0 a = 1
zpow_succ'✝ : ∀ (n : ℕ) (a : M), zpow✝ (↑n.succ) a = zpow✝ (↑n) a * a
inv✝ : M → M
zpow_neg'✝ : ∀ (n : ℕ) (a : M), zpow✝ (Int.negSucc n) a = (zpow✝ (↑n.succ) a)⁻¹
div✝ : M → M → M
div_eq_mul_inv✝ : ∀ (a b : M), a / b = a * b⁻¹
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : toMonoid = toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this✝¹ : Monoid.npow = Monoid.npow
this✝ : DivInvMonoid.zpow = DivInvMonoid.zpow
this : Div.div = Div.div
⊢ mk div_eq_mul_inv✝¹ zpow✝¹ zpow_zero'✝¹ zpow_succ'✝¹ zpow_neg'✝¹ =
    mk div_eq_mul_inv✝ zpow✝ zpow_zero'✝ zpow_succ'✝ zpow_neg'✝

Tactic:
congr

Result:
no goals

Proof state:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : toMonoid = toMonoid
h₁ : One.one = One.one
⊢ m₁ = m₂

Tactic:
let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=
  @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
    (fun x y => congr_fun (congr_fun h_mul x) y)

Result:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : toMonoid = toMonoid
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
⊢ m₁ = m₂
-- Mathlib/Topology/Algebra/MulAction.lean
theorem continuousSMul_inf {t₁ t₂ : TopologicalSpace X} [@ContinuousSMul M X _ _ t₁]
    [@ContinuousSMul M X _ _ t₂] : @ContinuousSMul M X _ _ (t₁ ⊓ t₂)

Proof state:
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
refine continuousSMul_iInf fun b => ?_

Result:
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
b : Bool
⊢ ContinuousSMul M X

Proof state:
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
b : Bool
⊢ ContinuousSMul M X

Tactic:
cases b <;> assumption

Result:
no goals