harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_eq_append_iff {l : Vector α (n + m)} {k : Nat} :
    zipIdx l k = l₁ ++ l₂ ↔
      ∃ (l₁' : Vector α n) (l₂' : Vector α m),
        l = l₁' ++ l₂' ∧ l₁ = zipIdx l₁' k ∧ l₂ = zipIdx l₂' (k + n)

Proof state:
α : Type u_1
k : Nat
l₁' l₂' : Array α
h : (l₁' ++ l₂').size = (l₁'.zipIdx k).size + (l₂'.zipIdx (k + l₁'.size)).size
⊢ l₁' ++ l₂' = { toArray := l₁', size_toArray := ⋯ }.toArray ++ { toArray := l₂', size_toArray := ⋯ }.toArray ∧
    l₁'.zipIdx k = { toArray := l₁', size_toArray := ⋯ }.zipIdx k ∧
      l₂'.zipIdx (k + l₁'.size) = { toArray := l₂', size_toArray := ⋯ }.zipIdx (k + (l₁'.zipIdx k).size)

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.mk
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ { toArray := l, size_toArray := h }.zipIdx k =
      { toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ } ↔
    ∃ l₁' l₂',
      { toArray := l, size_toArray := h } = l₁' ++ l₂' ∧
        { toArray := l₁, size_toArray := ⋯ } = l₁'.zipIdx k ∧
          { toArray := l₂, size_toArray := ⋯ } = l₂'.zipIdx (k + l₁.size)

Tactic:
simp only [zipIdx_mk, mk_append_mk, eq_mk, Array.zipIdx_eq_append_iff, mk_eq, toArray_append,
  toArray_zipIdx]

Result:
case mk.mk.mk
α : Type u_1
k : Nat
l : Array α
l₁ l₂ : Array (α × Nat)
h : l.size = l₁.size + l₂.size
⊢ (∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁'.size)) ↔
    ∃ l₁' l₂', l = l₁'.toArray ++ l₂'.toArray ∧ l₁ = l₁'.zipIdx k ∧ l₂ = l₂'.zipIdx (k + l₁.size)
-- Mathlib/RingTheory/FiniteType.lean
theorem of_mem_span_of_iff [Nontrivial R] {m : M} {S : Set M} :
    of R M m ∈ span R (of R M '' S) ↔ m ∈ S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
⊢ (of R M) m ∈ span R (⇑(of R M) '' S) ↔ m ∈ S

Tactic:
refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem (of R M) h⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : (of R M) m ∈ span R (⇑(of R M) '' S)
⊢ m ∈ S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : (of R M) m ∈ span R (⇑(of R M) '' S)
⊢ m ∈ S

Tactic:
erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
  Finsupp.support_single_ne_zero _ (one_ne_zero' R)] at h

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : Monoid M
inst✝ : Nontrivial R
m : M
S : Set M
h : ↑{m} ⊆ S
⊢ m ∈ S

Tactic:
simpa using h

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaEquiv_symm_naturality_right (X : C) {F F' : Sheaf J (Type v)} (f : F ⟶ F')
    (x : F.val.obj ⟨X⟩) : J.yonedaEquiv.symm x ≫ f = J.yonedaEquiv.symm (f.val.app ⟨X⟩ x)

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type v)
f : F ⟶ F'
x : F.val.obj (op X)
⊢ J.yonedaEquiv (J.yonedaEquiv.symm x ≫ f) = J.yonedaEquiv (J.yonedaEquiv.symm (f.val.app (op X) x))

Tactic:
simp [yonedaEquiv_comp]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type v)
f : F ⟶ F'
x : F.val.obj (op X)
⊢ J.yonedaEquiv.symm x ≫ f = J.yonedaEquiv.symm (f.val.app (op X) x)

Tactic:
apply J.yonedaEquiv.injective

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type v)
f : F ⟶ F'
x : F.val.obj (op X)
⊢ J.yonedaEquiv (J.yonedaEquiv.symm x ≫ f) = J.yonedaEquiv (J.yonedaEquiv.symm (f.val.app (op X) x))
-- Mathlib/Probability/Process/Filtration.lean
theorem filtrationOfSet_eq_natural [MulZeroOneClass β] [Nontrivial β] {s : ι → Set Ω}
    (hsm : ∀ i, MeasurableSet[m] (s i)) :
    filtrationOfSet hsm = natural (fun i => (s i).indicator (fun _ => 1 : Ω → β)) fun i =>
      stronglyMeasurable_one.indicator (hsm i)

Proof state:
case h.refine_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSet t

Tactic:
suffices MeasurableSpace.generateFrom {t | n ≤ i ∧
  MeasurableSet[MeasurableSpace.comap ((s n).indicator (fun _ => 1 : Ω → β)) mβ] t} ≤
    MeasurableSpace.generateFrom {t | ∃ (j : ι), j ≤ i ∧ s j = t} by
  exact this _ ht

Result:
case h.refine_2.intro
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : Preorder ι
inst✝¹ : MulZeroOneClass β
inst✝ : Nontrivial β
s : ι → Set Ω
hsm : ∀ (i : ι), MeasurableSet (s i)
i : ι
t : Set Ω
n : ι
ht : MeasurableSet t
⊢ MeasurableSpace.generateFrom {t | n ≤ i ∧ MeasurableSet t} ≤ MeasurableSpace.generateFrom {t | ∃ j ≤ i, s j = t}
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
@[simp]
lemma measure_const (c : ℝ) : (StieltjesFunction.const c).measure = 0 :=
  Measure.ext_of_Ioc _ _ (by simp)

Proof state:
c : ℝ
⊢ ∀ ⦃a b : ℝ⦄, a < b → (StieltjesFunction.const c).measure (Ioc a b) = 0 (Ioc a b)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem Derivation.tensorProductTo_mul (D : Derivation R S M) (x y : S ⊗[R] S) :
    D.tensorProductTo (x * y) =
      TensorProduct.lmul' (S := S) R x • D.tensorProductTo y +
        TensorProduct.lmul' (S := S) R y • D.tensorProductTo x

Proof state:
case refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y +
      (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
refine TensorProduct.induction_on y ?_ ?_ ?_

Result:
case refine_2.refine_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * 0) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo 0 +
      (TensorProduct.lmul' R) 0 • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

case refine_2.refine_2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x ⊗ₜ[R] y) =
      (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x ⊗ₜ[R] y) +
        (TensorProduct.lmul' R) (x ⊗ₜ[R] y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

case refine_2.refine_3
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ ∀ (x y : S ⊗[R] S),
    D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * x) =
        (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo x +
          (TensorProduct.lmul' R) x • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
      D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * y) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ ⊗ₜ[R] x₂) →
        D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * (x + y)) =
          (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo (x + y) +
            (TensorProduct.lmul' R) (x + y) • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Proof state:
case refine_2.refine_1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
x y : S ⊗[R] S
x₁ x₂ : S
⊢ D.tensorProductTo (x₁ ⊗ₜ[R] x₂ * 0) =
    (TensorProduct.lmul' R) (x₁ ⊗ₜ[R] x₂) • D.tensorProductTo 0 +
      (TensorProduct.lmul' R) 0 • D.tensorProductTo (x₁ ⊗ₜ[R] x₂)

Tactic:
rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/Additive.lean
theorem singleMapHomologicalComplex_inv_app_self (j : ι) (X : W₁) :
    ((singleMapHomologicalComplex F c j).inv.app X).f j =
      (singleObjXSelf c j (F.obj X)).hom ≫ F.map (singleObjXSelf c j X).inv

Proof state:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_5, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
j : ι
X : W₁
⊢ ((singleMapHomologicalComplex F c j).inv.app X).f j =
    (singleObjXSelf c j (F.obj X)).hom ≫ F.map (singleObjXSelf c j X).inv

Tactic:
simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem add_factorial_succ_le_factorial_add_succ (i : ℕ) (n : ℕ) :
    i + (n + 1)! ≤ (i + (n + 1))!

Proof state:
case inr
i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
match i with
| 0 => simp
| 1 =>
  rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
    Nat.add_le_add_iff_right]
  exact Nat.mul_pos n.succ_pos n.succ.factorial_pos
| succ (succ n) => contradiction

Result:
no goals

Proof state:
case inl.a.hi
i n : ℕ
h✝ : 2 ≤ i
⊢ 2 ≤ i

Tactic:
assumption

Result:
no goals

Proof state:
case inl.a
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Tactic:
apply add_factorial_succ_lt_factorial_add_succ

Result:
case inl.a.hi
i n : ℕ
h✝ : 2 ≤ i
⊢ 2 ≤ i

Proof state:
i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + (n + 1))!

Tactic:
rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
  Nat.add_le_add_iff_right]

Result:
i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1) * (n + 1)!

Proof state:
i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1) * (n + 1)!

Tactic:
exact Nat.mul_pos n.succ_pos n.succ.factorial_pos

Result:
no goals

Proof state:
i n✝ n : ℕ
h✝ : n.succ.succ < 2
⊢ n.succ.succ + (n✝ + 1)! ≤ (n.succ.succ + (n✝ + 1))!

Tactic:
contradiction

Result:
no goals

Proof state:
i n : ℕ
h✝ : 0 < 2
⊢ 0 + (n + 1)! ≤ (0 + (n + 1))!

Tactic:
simp

Result:
no goals

Proof state:
i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
cases (le_or_lt (2 : ℕ) i)

Result:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!

case inr
i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Proof state:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!

Tactic:
apply Nat.le_of_lt

Result:
case inl.a
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!

Proof state:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
rw [← Nat.add_assoc]

Result:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
-- Mathlib/Algebra/Module/SpanRank.lean
lemma spanRank_span_le_card (s : Set M) : (Submodule.span R s).spanRank ≤ #s

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s' : { s1 // span R s1 = span R s } := ⟨s, ⋯⟩
⊢ ⨅ s_1, #↑↑s_1 ≤ #↑s

Tactic:
exact ciInf_le' _ s'

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ (span R s).spanRank ≤ #↑s

Tactic:
rw [spanRank]

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ⨅ s_1, #↑↑s_1 ≤ #↑s

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ⨅ s_1, #↑↑s_1 ≤ #↑s

Tactic:
let s' : {s1 : Set M // span R s1 = span R s} := ⟨s, rfl⟩

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
s' : { s1 // span R s1 = span R s } := ⟨s, ⋯⟩
⊢ ⨅ s_1, #↑↑s_1 ≤ #↑s
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem rel_cons_right {as b bs} :
    Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ (∃ b_1 bs', flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
refine exists₂_congr fun a as' => ?_

Result:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
a : α
as' : Multiset α
⊢ flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
rw [← rel_flip, rel_cons_left]

Result:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ (∃ b_1 bs', flip r b b_1 ∧ Rel (flip r) bs bs' ∧ as = b_1 ::ₘ bs') ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
a : α
as' : Multiset α
⊢ flip r b a ∧ Rel (flip r) bs as' ∧ as = a ::ₘ as' ↔ r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
rw [rel_flip, flip]

Result:
no goals
-- Mathlib/Tactic/Linarith/Preprocessing.lean
theorem without_one_mul {M : Type*} [MulOneClass M] {a b : M} (h : 1 * a = b) : a = b

Proof state:
M : Type u_1
inst✝ : MulOneClass M
a b : M
h : 1 * a = b
⊢ a = b

Tactic:
rwa [one_mul] at h

Result:
no goals
-- Mathlib/MeasureTheory/Covering/DensityTheorem.lean
theorem ae_tendsto_average_norm_sub {f : α → E} (hf : LocallyIntegrable f μ) (K : ℝ) : ∀ᵐ x ∂μ,
    ∀ {ι : Type*} {l : Filter ι} (w : ι → α) (δ : ι → ℝ) (_ : Tendsto δ l (𝓝[>] 0))
      (_ : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)),
      Tendsto (fun j => ⨍ y in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)

Proof state:
α : Type u_1
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : IsUnifLocDoublingMeasure μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
E : Type u_2
inst✝ : NormedAddCommGroup E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
⊢ ∀ᵐ (x : α) ∂μ,
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j => ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)

Tactic:
filter_upwards [(vitaliFamily μ K).ae_tendsto_average_norm_sub hf] with x hx ι l w δ δlim
  xmem using hx.comp (tendsto_closedBall_filterAt μ _ _ δlim xmem)

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem OrderIso.isMin_apply {α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x : α} :
    IsMin (f x) ↔ IsMin x

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMin (f.symm (f x)) → IsMin (f x)

Tactic:
exact f.symm.strictMono.isMin_of_apply

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMin x → IsMin (f x)

Tactic:
conv_lhs => rw [← f.symm_apply_apply x]

Result:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMin (f.symm (f x)) → IsMin (f x)

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMin (f x) ↔ IsMin x

Tactic:
refine ⟨f.strictMono.isMin_of_apply, ?_⟩

Result:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMin x → IsMin (f x)
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem ite_le_natDegree_coeff (p : R[X]) (n : ℕ) (I : Decidable (n < 1 + natDegree p)) :
    @ite _ (n < 1 + natDegree p) I (coeff p n) 0 = coeff p n

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : n < 1 + p.natDegree
⊢ p.coeff n = p.coeff n

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
⊢ (if n < 1 + p.natDegree then p.coeff n else 0) = p.coeff n

Tactic:
split_ifs with h

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : n < 1 + p.natDegree
⊢ p.coeff n = p.coeff n

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
I : Decidable (n < 1 + p.natDegree)
h : ¬n < 1 + p.natDegree
⊢ 0 = p.coeff n

Tactic:
exact (coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem trace_eq_trace_adjoin [FiniteDimensional K L] (x : L) :
    trace K L x = finrank K⟮x⟯ L • trace K K⟮x⟯ (AdjoinSimple.gen K x)

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K ↥K⟮x⟯) ((Algebra.trace (↥K⟮x⟯) L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x))) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Tactic:
rw [trace_algebraMap, LinearMap.map_smul_of_tower]

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K ↥K⟮x⟯) ((Algebra.trace (↥K⟮x⟯) L) x) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Tactic:
conv in x => rw [← AdjoinSimple.algebraMap_gen K x]

Result:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K ↥K⟮x⟯) ((Algebra.trace (↥K⟮x⟯) L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x))) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K L) x = finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)

Tactic:
rw [← trace_trace (S := K⟮x⟯)]

Result:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K ↥K⟮x⟯) ((Algebra.trace (↥K⟮x⟯) L) x) =
    finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)
-- Mathlib/GroupTheory/OrderOfElement.lean
lemma smul_eq_of_le_smul
    {G : Type*} [Group G] [Finite G] {α : Type*} [PartialOrder α] {g : G} {a : α}
    [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : a ≤ g • a) : g • a = a

Proof state:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ g • g ^ (Nat.card G - 1) • a
⊢ g • a = a

Tactic:
rw [smul_smul, ← _root_.pow_succ',
  Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key

Result:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ a
⊢ g • a = a

Proof state:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ a
⊢ g • a = a

Tactic:
exact le_antisymm key h

Result:
no goals

Proof state:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ g • a = a

Tactic:
have key := smul_mono_right g (le_pow_smul h (Nat.card G - 1))

Result:
G : Type u_6
inst✝⁴ : Group G
inst✝³ : Finite G
α : Type u_7
inst✝² : PartialOrder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
key : g • a ≤ g • g ^ (Nat.card G - 1) • a
⊢ g • a = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem zip_nil_right : zip (l : List α) ([] : List β)  = []

Proof state:
α : Type u
β : Type v
l : List α
⊢ l.zip nil = nil

Tactic:
simp [zip, zipWith]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_add_nim_equiv (x y : Ordinal) :
    nim x + nim y ≈ nim (toOrdinal (∗x + ∗y))

Proof state:
x y : Ordinal.{u_1}
⊢ nim x + nim y ≈ nim (toOrdinal (toNimber x + toNimber y))

Tactic:
rw [← grundyValue_eq_iff_equiv_nim, grundyValue_nim_add_nim]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem lift_unique {A : Type*} [Semiring A] [Algebra R A] (f : M →ₗ[R] A)
    (g : TensorAlgebra R M →ₐ[R] A) : g.toLinearMap.comp (ι R) = f ↔ g = lift R f

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ g = (lift R) f

Tactic:
rw [← (lift R).symm_apply_eq]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ (lift R).symm g = f

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
g : TensorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔ (lift R).symm g = f

Tactic:
simp only [lift, Equiv.coe_fn_symm_mk]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma iInf_rat_gt_defaultRatCDF (t : ℚ) :
    ⨅ r : Ioi t, defaultRatCDF r = defaultRatCDF t

Proof state:
case intro
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
⊢ 0 ≤ (fun r => if ↑r < 0 then 0 else 1) y

Tactic:
dsimp only

Result:
case intro
t : ℚ
y : ↑(Ioi t)
hx : (fun r => if ↑r < 0 then 0 else 1) y ∈ range fun r => if ↑r < 0 then 0 else 1
⊢ 0 ≤ if ↑y < 0 then 0 else 1