harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem subsingleton_quotient_iff_eq_top : Subsingleton (M ⧸ p) ↔ p = ⊤

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : Subsingleton (M ⧸ p)
⊢ p = ⊤

Tactic:
refine eq_top_iff.mpr fun x _ => ?_

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
⊢ x ∈ p

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Subsingleton (M ⧸ ⊤)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton (M ⧸ p) → p = ⊤

Tactic:
rintro h

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : Subsingleton (M ⧸ p)
⊢ p = ⊤

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ p = ⊤ → Subsingleton (M ⧸ p)

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Subsingleton (M ⧸ ⊤)

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
this : x - 0 ∈ p
⊢ x ∈ p

Tactic:
rwa [sub_zero] at this

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
⊢ x ∈ p

Tactic:
have : x - 0 ∈ p := (Submodule.Quotient.eq p).mp (Subsingleton.elim _ _)

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : Subsingleton (M ⧸ p)
x : M
x✝ : x ∈ ⊤
this : x - 0 ∈ p
⊢ x ∈ p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton (M ⧸ p) ↔ p = ⊤

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton (M ⧸ p) → p = ⊤

case mpr
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ p = ⊤ → Subsingleton (M ⧸ p)
-- Mathlib/FieldTheory/Separable.lean
theorem AlgEquiv.isSeparable_iff {x : K} : IsSeparable F (e x) ↔ IsSeparable F x

Proof state:
F : Type u_1
K : Type u_3
inst✝⁴ : CommRing F
inst✝³ : Ring K
inst✝² : Algebra F K
E : Type u_4
inst✝¹ : Ring E
inst✝ : Algebra F E
e : K ≃ₐ[F] E
x : K
⊢ IsSeparable F (e x) ↔ IsSeparable F x

Tactic:
simp only [IsSeparable, minpoly.algEquiv_eq e x]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_unique {α β : Type*} [CommMonoid β] [Unique α] [Fintype α] (f : α → β) :
    ∏ x : α, f x = f default

Proof state:
α : Type u_9
β : Type u_10
inst✝² : CommMonoid β
inst✝¹ : Unique α
inst✝ : Fintype α
f : α → β
⊢ ∏ x : α, f x = f default

Tactic:
rw [univ_unique, prod_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem lt_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size)
    (h2 : ∀ j (hji : j ≤ i), ¬p (xs[j]'(Nat.lt_of_le_of_lt hji h))) : i < xs.findIdx p

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : ¬i < findIdx p xs
⊢ False

Tactic:
simp only [Nat.not_lt] at f

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : findIdx p xs ≤ i
⊢ False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
⊢ ¬i < findIdx p xs → False

Tactic:
intro f

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : ¬i < findIdx p xs
⊢ False

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
⊢ i < findIdx p xs

Tactic:
apply Decidable.byContradiction

Result:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
⊢ ¬i < findIdx p xs → False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : Array α
i : Nat
h : i < xs.size
h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true
f : findIdx p xs ≤ i
⊢ False

Tactic:
exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuous_rpow_const {y : ℝ} : Continuous fun a : ℝ≥0∞ => a ^ y

Proof state:
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => 1) x

Tactic:
exact continuousAt_const

Result:
no goals

Proof state:
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ 0 < z

Tactic:
simpa [hz] using hy

Result:
no goals

Proof state:
case inl
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
exact continuousAt_rpow_const_of_pos hy

Result:
no goals

Proof state:
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => (a ^ z)⁻¹) x

Tactic:
exact continuous_inv.continuousAt.comp (continuousAt_rpow_const_of_pos z_pos)

Result:
no goals

Proof state:
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
have z_pos : 0 < z := by simpa [hz] using hy

Result:
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => a ^ y) x

Proof state:
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
simp_rw [hz, rpow_neg]

Result:
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
z_pos : 0 < z
⊢ ContinuousAt (fun a => (a ^ z)⁻¹) x

Proof state:
case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
obtain ⟨z, hz⟩ : ∃ z, y = -z := ⟨-y, (neg_neg _).symm⟩

Result:
case inr.inr.intro
y : ℝ
x : ℝ≥0∞
hy : y < 0
z : ℝ
hz : y = -z
⊢ ContinuousAt (fun a => a ^ y) x

Proof state:
y : ℝ
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)

Result:
case inl
y : ℝ
x : ℝ≥0∞
hy : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x

case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ 0) x

case inr.inr
y : ℝ
x : ℝ≥0∞
hy : y < 0
⊢ ContinuousAt (fun a => a ^ y) x

Proof state:
y : ℝ
⊢ Continuous fun a => a ^ y

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Result:
y : ℝ
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ y) x

Proof state:
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => a ^ 0) x

Tactic:
simp only [rpow_zero]

Result:
case inr.inl
x : ℝ≥0∞
⊢ ContinuousAt (fun a => 1) x
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem aeval_eq_prod_aroots_sub_of_splits [Algebra K L] {p : K[X]}
    (hsplit : Splits (algebraMap K L) p) (v : L) :
    aeval v p = algebraMap K L p.leadingCoeff * ((p.aroots L).map fun a ↦ v - a).prod

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
hsplit : Splits (algebraMap K L) p
v : L
⊢ (aeval v) p = (algebraMap K L) p.leadingCoeff * (Multiset.map (fun a => v - a) (p.aroots L)).prod

Tactic:
rw [← eval_map_algebraMap, eq_prod_roots_of_splits hsplit]

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
hsplit : Splits (algebraMap K L) p
v : L
⊢ eval v (C ((algebraMap K L) p.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (algebraMap K L) p).roots).prod) =
    (algebraMap K L) p.leadingCoeff * (Multiset.map (fun a => v - a) (p.aroots L)).prod

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
hsplit : Splits (algebraMap K L) p
v : L
⊢ eval v (C ((algebraMap K L) p.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (algebraMap K L) p).roots).prod) =
    (algebraMap K L) p.leadingCoeff * (Multiset.map (fun a => v - a) (p.aroots L)).prod

Tactic:
simp [eval_multiset_prod]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem exists₂_comm
    {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
    (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂

Proof state:
ι₁ : Sort u_3
ι₂ : Sort u_4
κ₁ : ι₁ → Sort u_5
κ₂ : ι₂ → Sort u_6
p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop
⊢ (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂

Tactic:
simp only [@exists_comm (κ₁ _), @exists_comm ι₁]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem to_iso [h' : Epi f.base] : IsIso f

Proof state:
case inst
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
t : ↑↑X ≃ₜ ↑↑Y :=
  (Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom f.base) ⋯).trans
    { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso f.base

Tactic:
exact (TopCat.isoOfHomeo t).isIso_hom

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma le_addContent_diff (m : AddContent C) (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) :
    m s - m t ≤ m (s \ t)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s ∩ t ∪ s \ t) - m t ≤ m (s \ t)

Tactic:
rw [addContent_union hC (hC.inter_mem hs ht) (hC.diff_mem hs ht) disjoint_inf_sdiff, add_comm]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s \ t) + m (s ∩ t) - m t ≤ m (s \ t)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s \ t) + m (s ∩ t) - m t ≤ m (s \ t)

Tactic:
refine add_tsub_le_assoc.trans_eq ?_

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s \ t) + (m (s ∩ t) - m t) = m (s \ t)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m s - m t ≤ m (s \ t)

Tactic:
conv_lhs => rw [← inter_union_diff s t]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s ∩ t ∪ s \ t) - m t ≤ m (s \ t)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s \ t) + (m (s ∩ t) - m t) = m (s \ t)

Tactic:
rw [tsub_eq_zero_of_le
  (addContent_mono hC.isSetSemiring (hC.inter_mem hs ht) ht inter_subset_right), add_zero]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_nhdsWithin {y : M} (hy : y ∈ f.source) :
    map (f.extend I) (𝓝[s] y) = 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I)) (𝓝[s] y) = 𝓝[↑(f.extend I).symm ⁻¹' s ∩ range ↑I] ↑(f.extend I) y

Tactic:
rw [map_extend_nhdsWithin_eq_image f hy, nhdsWithin_inter, ←
  nhdsWithin_extend_target_eq _ hy, ← nhdsWithin_inter, (f.extend I).image_source_inter_eq',
  inter_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem zero_lt_pow (n : Nat) : 0 < 2^n

Proof state:
⊢ 0 < 2 ^ 0

Tactic:
simp [eq_0_of_lt]

Result:
no goals

Proof state:
case succ
n✝ : Nat
a✝ : 0 < 2 ^ n✝
⊢ 0 < 2 ^ (n✝ + 1)

Tactic:
case succ n hyp => simpa [Nat.pow_succ]

Result:
no goals

Proof state:
n : Nat
⊢ 0 < 2 ^ n

Tactic:
induction n

Result:
case zero

⊢ 0 < 2 ^ 0

case succ
n✝ : Nat
a✝ : 0 < 2 ^ n✝
⊢ 0 < 2 ^ (n✝ + 1)

Proof state:
n : Nat
hyp : 0 < 2 ^ n
⊢ 0 < 2 ^ (n + 1)

Tactic:
simpa [Nat.pow_succ]

Result:
no goals

Proof state:
case zero

⊢ 0 < 2 ^ 0

case succ
n✝ : Nat
a✝ : 0 < 2 ^ n✝
⊢ 0 < 2 ^ (n✝ + 1)

Tactic:
case zero => simp [eq_0_of_lt]

Result:
case succ
n✝ : Nat
a✝ : 0 < 2 ^ n✝
⊢ 0 < 2 ^ (n✝ + 1)
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma log_coverMincard_nonneg (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) (n : ℕ) :
    0 ≤ log (coverMincard T F U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ coverMincard T F U n

Tactic:
exact (one_le_coverMincard_iff T F U n).2 h

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 0 ≤ (↑(coverMincard T F U n)).log

Tactic:
apply zero_le_log_iff.2

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ ↑(coverMincard T F U n)

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ ↑(coverMincard T F U n)

Tactic:
rw [← ENat.toENNReal_one, ENat.toENNReal_le]

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
n : ℕ
⊢ 1 ≤ coverMincard T F U n
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_lowerClosure (s : Set α) : ↑(lowerClosure s) = ⋃ a ∈ s, Iic a

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ↑(lowerClosure s) = ⋃ a ∈ s, Iic a

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(lowerClosure s) ↔ x✝ ∈ ⋃ a ∈ s, Iic a

Proof state:
case h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(lowerClosure s) ↔ x✝ ∈ ⋃ a ∈ s, Iic a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem eq_cons {n m : ℕ} (h : n < m) : Ico n m = n :: Ico (n + 1) m

Proof state:
n m : ℕ
h : n < m
⊢ Ico n m = n :: Ico (n + 1) m

Tactic:
rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]

Result:
n m : ℕ
h : n < m
⊢ [n] ++ Ico n.succ m = n :: Ico (n + 1) m

Proof state:
n m : ℕ
h : n < m
⊢ [n] ++ Ico n.succ m = n :: Ico (n + 1) m

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem fastGrowing_one : fastGrowing 1 = fun n => 2 * n

Proof state:
⊢ fastGrowing 1 = fun n => 2 * n

Tactic:
rw [@fastGrowing_succ 1 0 rfl]

Result:
⊢ (fun i => (fastGrowing 0)^[i] i) = fun n => 2 * n

Proof state:
⊢ (fun i => (fastGrowing 0)^[i] i) = fun n => 2 * n

Tactic:
funext i

Result:
case h
i : ℕ
⊢ (fastGrowing 0)^[i] i = 2 * i

Proof state:
case h
i a b : ℕ
⊢ Nat.succ^[a] b = b + a

Tactic:
induction a <;> simp [*, Function.iterate_succ', Nat.add_assoc, -Function.iterate_succ]

Result:
no goals

Proof state:
case h
i : ℕ
⊢ Nat.succ^[i] i = i + i

Tactic:
suffices ∀ a b, Nat.succ^[a] b = b + a from this _ _

Result:
case h
i : ℕ
⊢ ∀ (a b : ℕ), Nat.succ^[a] b = b + a

Proof state:
case h
i : ℕ
⊢ (fastGrowing 0)^[i] i = 2 * i

Tactic:
rw [two_mul, fastGrowing_zero]

Result:
case h
i : ℕ
⊢ Nat.succ^[i] i = i + i

Proof state:
case h
i : ℕ
⊢ ∀ (a b : ℕ), Nat.succ^[a] b = b + a

Tactic:
intro a b

Result:
case h
i a b : ℕ
⊢ Nat.succ^[a] b = b + a
-- Mathlib/Data/Finsupp/Interval.lean
theorem card_Ico : #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.associator_natural {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) :
    biprod.map (biprod.map f g) h ≫ (biprod.associator _ _ _).hom
      = (biprod.associator _ _ _).hom ≫ biprod.map f (biprod.map g h)

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
U V W X Y Z : C
f : U ⟶ X
g : V ⟶ Y
h : W ⟶ Z
⊢ map (map f g) h ≫ (associator X Y Z).hom = (associator U V W).hom ≫ map f (map g h)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_pos {x : X} (hx : x ∈ s) : ∃ i, 0 < f i x

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∑ᶠ (i : ι), (f i) x = 1
⊢ ∃ i, 0 < (f i) x

Tactic:
contrapose! H

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (i : ι), (f i) x ≤ 0
⊢ ∑ᶠ (i : ι), (f i) x ≠ 1

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ ∃ i, 0 < (f i) x

Tactic:
have H := f.sum_eq_one hx

Result:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∑ᶠ (i : ι), (f i) x = 1
⊢ ∃ i, 0 < (f i) x

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (i : ι), (f i) x ≤ 0
⊢ ∑ᶠ (i : ι), (f i) x ≠ 1

Tactic:
simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem biproduct_ι_comp_rightDistributor_hom {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
    (biproduct.ι _ j ▷ X) ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ biproduct.ι f j ▷ X ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j

Tactic:
classical
simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_whiskerRight_assoc, biproduct.ι_π,
  dite_whiskerRight, dite_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ biproduct.ι f j ▷ X ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j

Tactic:
simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_whiskerRight_assoc, biproduct.ι_π,
  dite_whiskerRight, dite_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem aemeasurable_const' (h : ∀ᵐ (x) (y) ∂μ, f x = f y) : AEMeasurable f μ

Proof state:
case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable f 0

Tactic:
exact aemeasurable_zero_measure

Result:
no goals

Proof state:
case inr.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : (ae μ).NeBot
x : α
hx : ∀ᵐ (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ

Tactic:
exact ⟨const α (f x), measurable_const, EventuallyEq.symm hx⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ

Tactic:
rcases eq_or_ne μ 0 with (rfl | hμ)

Result:
case inl
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
h : ∀ᵐ (x : α) (y : α) ∂0, f x = f y
⊢ AEMeasurable f 0

case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ AEMeasurable f μ

Proof state:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
⊢ AEMeasurable f μ

Tactic:
haveI := ae_neBot.2 hμ

Result:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : (ae μ).NeBot
⊢ AEMeasurable f μ

Proof state:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : (ae μ).NeBot
⊢ AEMeasurable f μ

Tactic:
rcases h.exists with ⟨x, hx⟩

Result:
case inr.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
h : ∀ᵐ (x : α) (y : α) ∂μ, f x = f y
hμ : μ ≠ 0
this : (ae μ).NeBot
x : α
hx : ∀ᵐ (y : α) ∂μ, f x = f y
⊢ AEMeasurable f μ
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem numeric_toPGame (o : Ordinal) : o.toPGame.Numeric

Proof state:
case h.H
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.Numeric
⊢ ∀ (i : o.toPGame.LeftMoves), (o.toPGame.moveLeft i).Numeric

Tactic:
simpa using fun i => IH _ (Ordinal.toLeftMovesToPGame_symm_lt i)

Result:
no goals

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.Numeric
⊢ o.toPGame.Numeric

Tactic:
apply numeric_of_isEmpty_rightMoves

Result:
case h.H
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.Numeric
⊢ ∀ (i : o.toPGame.LeftMoves), (o.toPGame.moveLeft i).Numeric

Proof state:
o : Ordinal.{u_1}
⊢ o.toPGame.Numeric

Tactic:
induction' o using Ordinal.induction with o IH

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, k.toPGame.Numeric
⊢ o.toPGame.Numeric
-- Mathlib/Data/List/Map2.lean
theorem map₂Right'_nil_left : map₂Right' f [] bs = (bs.map (f none), [])

Proof state:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right' f [] bs = (map (f none) bs, [])

Tactic:
cases bs <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLinAlgEquiv_mul (A B : Matrix n n R) :
    Matrix.toLinAlgEquiv v₁ (A * B) =
      (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
A B : Matrix n n R
⊢ (toLinAlgEquiv v₁) (A * B) = (toLinAlgEquiv v₁) A ∘ₗ (toLinAlgEquiv v₁) B

Tactic:
convert Matrix.toLin_mul v₁ v₁ v₁ A B

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem neg_mul_neg (a b : α) : -a * -b = a * b

Proof state:
α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * -b = a * b

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem prod_trans {η : Type*} {ε : Type*} (e : PartialEquiv α β) (f : PartialEquiv β γ)
    (e' : PartialEquiv δ η) (f' : PartialEquiv η ε) :
    (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
⊢ (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

Tactic:
ext ⟨x, y⟩ <;> simp [Set.ext_iff]

Result:
case hs.h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source

Proof state:
case hs.h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
η : Type u_5
ε : Type u_6
e : PartialEquiv α β
f : PartialEquiv β γ
e' : PartialEquiv δ η
f' : PartialEquiv η ε
x : α
y : δ
⊢ (x ∈ e.source ∧ y ∈ e'.source) ∧ ↑e x ∈ f.source ∧ ↑e' y ∈ f'.source ↔
    (x ∈ e.source ∧ ↑e x ∈ f.source) ∧ y ∈ e'.source ∧ ↑e' y ∈ f'.source

Tactic:
tauto

Result:
no goals