harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem hasMFDerivWithinAt_iff_hasFDerivWithinAt {f'} :
    HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f' ↔ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)
⊢ HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f' ↔ HasFDerivWithinAt f f' s x

Tactic:
simpa only [HasMFDerivWithinAt, and_iff_right_iff_imp, mfld_simps] using
  HasFDerivWithinAt.continuousWithinAt

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_smul_ofReal_left (x y : F) {t : ℝ} : ⟪(t : 𝕜) • x, y⟫ = ⟪x, y⟫ * t

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ ⟪↑t • x, y⟫_𝕜 = ⟪x, y⟫_𝕜 * ↑t

Tactic:
rw [inner_smul_left, conj_ofReal, mul_comm]

Result:
no goals
-- Mathlib/Probability/Kernel/Invariance.lean
theorem const_bind_eq_comp_const (κ : Kernel α β) (μ : Measure α) :
    const α (μ.bind κ) = κ ∘ₖ const α μ

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
a : α
s : Set β
hs : MeasurableSet s
⊢ ((const α (μ.bind ⇑κ)) a) s = ((κ ∘ₖ const α μ) a) s

Tactic:
simp_rw [comp_apply' _ _ _ hs, const_apply, Measure.bind_apply hs (Kernel.measurable _)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
⊢ const α (μ.bind ⇑κ) = κ ∘ₖ const α μ

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
a : α
s : Set β
hs : MeasurableSet s
⊢ ((const α (μ.bind ⇑κ)) a) s = ((κ ∘ₖ const α μ) a) s
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma posPart_algebraMap_nnreal (r : ℝ≥0) : (algebraMap ℝ≥0 A r)⁺ = algebraMap ℝ≥0 A r

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ cfc (fun x => x⁺) ((algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)) = (algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ ((algebraMap ℝ≥0 A) r)⁺ = (algebraMap ℝ≥0 A) r

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc, IsScalarTower.algebraMap_apply ℝ≥0 ℝ A]

Result:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ≥0
⊢ cfc (fun x => x⁺) ((algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)) = (algebraMap ℝ A) ((algebraMap ℝ≥0 ℝ) r)
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_le_one {o} : card o ≤ 1 ↔ o ≤ 1

Proof state:
o : Ordinal.{u_1}
⊢ o.card ≤ 1 ↔ o ≤ 1

Tactic:
simpa using card_le_nat (n := 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1)

Proof state:
case cons.zero
α : Type u_1
hd : α
tl : List α
hl : ∀ (n : Nat), (drop n tl).tail = drop (n + 1) tl
⊢ (drop 0 (hd :: tl)).tail = drop (0 + 1) (hd :: tl)

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
n : Nat
⊢ (drop n []).tail = drop (n + 1) []

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
hd : α
tl : List α
hl : ∀ (n : Nat), (drop n tl).tail = drop (n + 1) tl
n✝ : Nat
⊢ (drop (n✝ + 1) (hd :: tl)).tail = drop (n✝ + 1 + 1) (hd :: tl)

Tactic:
simp [hl]

Result:
no goals

Proof state:
case cons
α : Type u_1
hd : α
tl : List α
hl : ∀ (n : Nat), (drop n tl).tail = drop (n + 1) tl
n : Nat
⊢ (drop n (hd :: tl)).tail = drop (n + 1) (hd :: tl)

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
hd : α
tl : List α
hl : ∀ (n : Nat), (drop n tl).tail = drop (n + 1) tl
⊢ (drop 0 (hd :: tl)).tail = drop (0 + 1) (hd :: tl)

case cons.succ
α : Type u_1
hd : α
tl : List α
hl : ∀ (n : Nat), (drop n tl).tail = drop (n + 1) tl
n✝ : Nat
⊢ (drop (n✝ + 1) (hd :: tl)).tail = drop (n✝ + 1 + 1) (hd :: tl)
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem perm_inv_mapsTo_of_mapsTo (f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) :
    Set.MapsTo (f⁻¹ :) s s

Proof state:
α : Type u
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (⇑f) s s
⊢ Set.MapsTo (⇑f⁻¹) s s

Tactic:
cases nonempty_fintype s

Result:
case intro
α : Type u
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (⇑f) s s
val✝ : Fintype ↑s
⊢ Set.MapsTo (⇑f⁻¹) s s

Proof state:
case intro
α : Type u
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (⇑f) s s
val✝ : Fintype ↑s
⊢ Set.MapsTo (⇑f⁻¹) s s

Tactic:
exact fun x hx =>
  Set.mem_toFinset.mp <|
    perm_inv_on_of_perm_on_finset
      (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
      (Set.mem_toFinset.mpr hx)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma pow_lt_pow_iff_left (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

Proof state:
a b n : ℕ
hn : n ≠ 0
⊢ a ^ n < b ^ n ↔ a < b

Tactic:
simp only [← Nat.not_le, Nat.pow_le_pow_iff_left hn]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem isIso_toSheafify {P : Cᵒᵖ ⥤ D} (hP : Presheaf.IsSheaf J P) : IsIso (J.toSheafify P)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
this : IsIso (J.toPlus P)
⊢ IsIso (J.toPlus P ≫ (J.plusFunctor D).map (J.toPlus P))

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
this : IsIso (J.toPlus P)
⊢ IsIso (J.toPlus P ≫ J.plusMap (J.toPlus P))

Tactic:
change (IsIso (toPlus J P ≫ (J.plusFunctor D).map (toPlus J P)))

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
this : IsIso (J.toPlus P)
⊢ IsIso (J.toPlus P ≫ (J.plusFunctor D).map (J.toPlus P))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (J.toPlus P ≫ J.plusMap (J.toPlus P))

Tactic:
haveI := isIso_toPlus_of_isSheaf J P hP

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
this : IsIso (J.toPlus P)
⊢ IsIso (J.toPlus P ≫ J.plusMap (J.toPlus P))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (J.toSheafify P)

Tactic:
dsimp [toSheafify]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
⊢ IsIso (J.toPlus P ≫ J.plusMap (J.toPlus P))
-- Mathlib/Data/Set/Card.lean
theorem encard_insert_of_not_mem {a : α} (has : a ∉ s) : (insert a s).encard = s.encard + 1

Proof state:
α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ Disjoint s {a}

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a : α
has : a ∉ s
⊢ (insert a s).encard = s.encard + 1

Tactic:
rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem iSup_succ (o : Ordinal) : ⨆ a : Iio o, succ a.1 = o

Proof state:
o : Ordinal.{u_4}
⊢ ⨆ a, succ ↑a = o

Tactic:
apply (le_of_forall_lt _).antisymm'

Result:
o : Ordinal.{u_4}
⊢ ⨆ a, succ ↑a ≤ o

o : Ordinal.{u_4}
⊢ ∀ c < o, c < ⨆ a, succ ↑a

Proof state:
o : Ordinal.{u_4}
⊢ ⨆ a, succ ↑a ≤ o

Tactic:
simp [Ordinal.iSup_le_iff]

Result:
no goals

Proof state:
o : Ordinal.{u_4}
⊢ ∀ c < o, c < ⨆ a, succ ↑a

Tactic:
exact fun a ha ↦ (lt_succ a).trans_le <| Ordinal.le_iSup (fun x : Iio _ ↦ _) ⟨a, ha⟩

Result:
no goals
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma re_complexMGF_ofReal' : (fun x : ℝ ↦ (complexMGF X μ x).re) = mgf X μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ (fun x => (complexMGF X μ ↑x).re) = mgf X μ

Tactic:
ext x

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ (complexMGF X μ ↑x).re = mgf X μ x

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ (complexMGF X μ ↑x).re = mgf X μ x

Tactic:
exact re_complexMGF_ofReal x

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma add_ne_top_iff_of_ne_bot {x y : EReal} (hx : x ≠ ⊥) (hy : y ≠ ⊥) :
    x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Proof state:
case h_real
y : EReal
a✝ : ℝ
hy : ¬y = ⊥
⊢ ¬↑a✝ + y = ⊤ → ¬y = ⊤

Tactic:
induction y <;> simp_all

Result:
no goals

Proof state:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
refine ⟨?_, fun h ↦ add_ne_top h.1 h.2⟩

Result:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤

Proof state:
x y : EReal
hx : x ≠ ⊥
hy : y ≠ ⊥
⊢ x + y ≠ ⊤ → x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
induction x <;> simp_all

Result:
case h_real
y : EReal
a✝ : ℝ
hy : ¬y = ⊥
⊢ ¬↑a✝ + y = ⊤ → ¬y = ⊤
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma ι₀_desc : ι₀ K ≫ desc φ₀ φ₁ h = φ₀

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
φ₀ φ₁ : K ⟶ F
h : Homotopy φ₀ φ₁
⊢ ι₀ K ≫ desc φ₀ φ₁ h = φ₀

Tactic:
simp [ι₀, desc]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem right_nonuniformWitnesses_subset (h : ¬G.IsUniform ε s t) :
    (G.nonuniformWitnesses ε s t).2 ⊆ t

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (G.nonuniformWitnesses ε s t).2 ⊆ t

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (⋯.choose, ⋯.choose).2 ⊆ t

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ (⋯.choose, ⋯.choose).2 ⊆ t

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.1

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem iInf_mul (f : ι → ℝ≥0) (a : ℝ≥0) : iInf f * a = ⨅ i, f i * a

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ iInf f * a = ⨅ i, f i * a

Tactic:
rw [← coe_inj, NNReal.coe_mul, coe_iInf, coe_iInf]

Result:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ i, ↑(f i)) * ↑a = ⨅ i, ↑(f i * a)

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ i, ↑(f i)) * ↑a = ⨅ i, ↑(f i * a)

Tactic:
exact Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.linear_preimage {s : Set F} (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) :
    Convex 𝕜 (f ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s

Tactic:
exact hs hx hy ha hb hab

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s

Tactic:
rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
⊢ Convex 𝕜 (⇑f ⁻¹' s)

Tactic:
intro x hx y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ⇑f ⁻¹' s
y : E
hy : y ∈ ⇑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⇑f ⁻¹' s
-- Mathlib/Logic/Equiv/Basic.lean
theorem eq_of_prodExtendRight_ne {e : Perm β₁} {a a' : α₁} {b : β₁}
    (h : prodExtendRight a e (a', b) ≠ (a', b)) : a' = a

Proof state:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : (prodExtendRight a e) (a', b) ≠ (a', b)
⊢ a' = a

Tactic:
contrapose! h

Result:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : a' ≠ a
⊢ (prodExtendRight a e) (a', b) = (a', b)

Proof state:
α₁ : Type u_9
β₁ : Type u_10
inst✝ : DecidableEq α₁
e : Perm β₁
a a' : α₁
b : β₁
h : a' ≠ a
⊢ (prodExtendRight a e) (a', b) = (a', b)

Tactic:
exact prodExtendRight_apply_ne _ h _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_of_ae_eq_of_ae_restrict {s t} (hst : s =ᵐ[μ] t) {p : α → Prop} :
    (∀ᵐ x ∂μ.restrict s, p x) → ∀ᵐ x ∂μ.restrict t, p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : α → Prop
hst : s =ᶠ[ae μ] t
p : α → Prop
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x

Tactic:
simp [Measure.restrict_congr_set hst]

Result:
no goals
-- Mathlib/ModelTheory/Types.lean
theorem nonempty_iff : Nonempty (T.CompleteType α) ↔ T.IsSatisfiable

Proof state:
L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable

Tactic:
rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne, not_iff_comm,
  ← union_empty ((L.lhomWithConstants α).onTheory T), ← setOf_subset_eq_empty_iff]

Result:
L : Language
T : L.Theory
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅

Proof state:
L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ T.IsSatisfiable

Tactic:
rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]

Result:
L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable

Proof state:
L : Language
T : L.Theory
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mem_span_mul_finite_of_mem_mul {P Q : Submodule R A} {x : A} (hx : x ∈ P * Q) :
    ∃ T T' : Finset A, (T : Set A) ⊆ P ∧ (T' : Set A) ⊆ Q ∧ x ∈ span R (T * T' : Set A) :=
  Submodule.mem_span_mul_finite_of_mem_span_mul
    (by rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P Q : Submodule R A
x : A
hx : x ∈ P * Q
⊢ x ∈ span R (↑P * ↑Q)

Tactic:
rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAtFilter.iterate {f : 𝕜 → 𝕜} {f' : 𝕜}
    (hf : HasDerivAtFilter f f' x L) (hL : Tendsto f L L) (hx : f x = x) (n : ℕ) :
    HasDerivAtFilter f^[n] (f' ^ n) x L

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
this : HasFDerivAtFilter f^[n] (smulRight 1 f' ^ n) x L
⊢ HasDerivAtFilter f^[n] (f' ^ n) x L

Tactic:
rwa [ContinuousLinearMap.smulRight_one_pow] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
⊢ HasDerivAtFilter f^[n] (f' ^ n) x L

Tactic:
have := hf.iterate hL hx n

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivAtFilter f f' x L
hL : Tendsto f L L
hx : f x = x
n : ℕ
this : HasFDerivAtFilter f^[n] (smulRight 1 f' ^ n) x L
⊢ HasDerivAtFilter f^[n] (f' ^ n) x L
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_biUnion_lt_top {s : Set β} {f : β → Set α} (hs : s.Finite)
    (hfin : ∀ i ∈ s, μ (f i) < ∞) : μ (⋃ i ∈ s, f i) < ∞

Proof state:
case h.e'_3.h.e'_6.h.e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ⊤
⊢ (fun i => ⋃ (_ : i ∈ s), f i) = fun i => ⋃ (_ : i ∈ hs.toFinset), f i

Tactic:
ext

Result:
case h.e'_3.h.e'_6.h.e'_3.h.h
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ⊤
x✝¹ : β
x✝ : α
⊢ x✝ ∈ ⋃ (_ : x✝¹ ∈ s), f x✝¹ ↔ x✝ ∈ ⋃ (_ : x✝¹ ∈ hs.toFinset), f x✝¹

Proof state:
case convert_2
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ⊤
⊢ ∑ i ∈ hs.toFinset, μ (f i) < ⊤

Tactic:
simpa only [ENNReal.sum_lt_top, Finite.mem_toFinset]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ⊤
⊢ μ (⋃ i ∈ s, f i) < ⊤

Tactic:
convert (measure_biUnion_finset_le (μ := μ) hs.toFinset f).trans_lt _ using 3

Result:
case h.e'_3.h.e'_6.h.e'_3
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ⊤
⊢ (fun i => ⋃ (_ : i ∈ s), f i) = fun i => ⋃ (_ : i ∈ hs.toFinset), f i

case convert_2
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ⊤
⊢ ∑ i ∈ hs.toFinset, μ (f i) < ⊤

Proof state:
case h.e'_3.h.e'_6.h.e'_3.h.h
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Finite
hfin : ∀ i ∈ s, μ (f i) < ⊤
x✝¹ : β
x✝ : α
⊢ x✝ ∈ ⋃ (_ : x✝¹ ∈ s), f x✝¹ ↔ x✝ ∈ ⋃ (_ : x✝¹ ∈ hs.toFinset), f x✝¹

Tactic:
rw [Finite.mem_toFinset]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc (attr := simp)]
lemma rotateHomotopyEquiv_comm₃ :
    (rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃ = -φ⟦1⟧'

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 rotateHomotopyEquiv.proof_4)
            (-(inl φ).leftShift 1 0 rotateHomotopyEquiv.proof_5) ⋯).f
        p ≫
      (triangle (inr φ)).mor₃.f p =
    -φ.f (p + 1)

Tactic:
simp only [Int.reduceNeg, lift_f _ _ _ _ _ (p + 1) rfl, shiftFunctor_obj_X', Cocycle.coe_neg,
  Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.neg_v,
  (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by omega),
  shiftFunctor_obj_X, mul_one, sub_self, mul_zero, Int.zero_ediv, add_zero, Int.negOnePow_one,
  shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Cochain.ofHom_v, id_comp,
  Units.neg_smul, one_smul, neg_neg, Preadditive.neg_comp, Preadditive.add_comp, assoc,
  inl_v_triangle_mor₃_f, Iso.refl_inv, Preadditive.comp_neg, comp_id, inr_f_triangle_mor₃_f,
  comp_zero, neg_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ

Tactic:
ext p

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ ((rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃).f p =
    (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ).f p

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ ((rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃).f p =
    (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ).f p

Tactic:
dsimp [rotateHomotopyEquiv]

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 rotateHomotopyEquiv.proof_4)
            (-(inl φ).leftShift 1 0 rotateHomotopyEquiv.proof_5) ⋯).f
        p ≫
      (triangle (inr φ)).mor₃.f p =
    -φ.f (p + 1)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ p + 1 + 0 = p + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Category/Compactum.lean
theorem isClosed_cl {X : Compactum} (A : Set X) : IsClosed (cl A)

Proof state:
X : Compactum
A : Set X.A
⊢ ∀ (F : Ultrafilter X.A), Compactum.cl A ∈ F → X.str F ∈ Compactum.cl A

Tactic:
intro F hF

Result:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : Compactum.cl A ∈ F
⊢ X.str F ∈ Compactum.cl A

Proof state:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : Compactum.cl A ∈ F
⊢ X.str F ∈ Compactum.cl A

Tactic:
exact cl_cl _ ⟨F, hF, rfl⟩

Result:
no goals

Proof state:
X : Compactum
A : Set X.A
⊢ IsClosed (Compactum.cl A)

Tactic:
rw [isClosed_iff]

Result:
X : Compactum
A : Set X.A
⊢ ∀ (F : Ultrafilter X.A), Compactum.cl A ∈ F → X.str F ∈ Compactum.cl A
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pullbackSymmetry_inv_comp_snd [HasPullback f g] :
    (pullbackSymmetry f g).inv ≫ pullback.snd f g = pullback.fst g f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).inv ≫ pullback.snd f g = pullback.fst g f

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals