harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_Ioi_eq_Ici {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E)
    (x : ℝ) : derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
simpa using (uniqueDiffOn_Ici x).eq left_mem_Ici A B

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x

Tactic:
rwa [differentiableWithinAt_Ioi_iff_Ici] at H

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
have A := H.hasDerivWithinAt.Ici_of_Ioi

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Proof state:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
rw [derivWithin_zero_of_not_differentiableWithinAt H,
  derivWithin_zero_of_not_differentiableWithinAt]

Result:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : ¬DifferentiableWithinAt ℝ f (Ioi x) x
⊢ ¬DifferentiableWithinAt ℝ f (Ici x) x
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem MonoidHomClass.lipschitz_of_bound [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ)
    (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) : LipschitzWith (Real.toNNReal C) f :=
  LipschitzWith.of_dist_le' fun x y => by simpa only [dist_eq_norm_div, map_div] using h (x / y)

Proof state:
𝓕 : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : SeminormedGroup E
inst✝² : SeminormedGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : MonoidHomClass 𝓕 E F
f : 𝓕
C : ℝ
h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖
x y : E
⊢ dist (f x) (f y) ≤ C * dist x y

Tactic:
simpa only [dist_eq_norm_div, map_div] using h (x / y)

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
@[reassoc (attr := simp)]
lemma whiskerLeft_curry_ihom_ev_app (g : A ⊗ Y ⟶ X) :
    A ◁ curry g ≫ (ihom.ev A).app X = g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
A X Y : C
inst✝ : Closed A
g : A ⊗ Y ⟶ X
⊢ A ◁ curry g ≫ (ihom.ev A).app X = g

Tactic:
simp [curry_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
    m.1.isEmpty ↔ ∀ a, m.contains a = false

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
⊢ m.val.isEmpty = true ↔ ∀ (a : α), m.contains a = false

Tactic:
simp_to_model using List.isEmpty_iff_forall_containsKey

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_update_update [DecidableEq ι] {i j : ι} (hij : i ≠ j) (m : M) :
    f (Function.update (Function.update v i m) j m) = 0 :=
  f.map_eq_zero_of_eq _
    (by rw [Function.update_self, Function.update_of_ne hij, Function.update_self]) hij

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
⊢ update (update v i m) j m i = update (update v i m) j m j

Tactic:
rw [Function.update_self, Function.update_of_ne hij, Function.update_self]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_eq_measure_of_between_null_diff {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃)
    (h_nulldiff : μ (s₃ \ s₁) = 0) : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ s₃ = μ (s₃ \ s₁ ∪ s₁)

Tactic:
rw [diff_union_of_subset (h12.trans h23)]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Tactic:
have key : μ s₃ ≤ μ s₁ :=
  calc
    μ s₃ = μ (s₃ \ s₁ ∪ s₁) := by rw [diff_union_of_subset (h12.trans h23)]
    _ ≤ μ (s₃ \ s₁) + μ s₁ := measure_union_le _ _
    _ = μ s₁ := by simp only [h_nulldiff, zero_add]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
key : μ s₃ ≤ μ s₁
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Tactic:
have le12 : μ s₁ ≤ μ s₂ := measure_mono h12

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Tactic:
have le23 : μ s₂ ≤ μ s₃ := measure_mono h23

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
⊢ μ (s₃ \ s₁) + μ s₁ = μ s₁

Tactic:
simp only [h_nulldiff, zero_add]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ (s₃ \ s₁) = 0
le12 : μ s₁ ≤ μ s₂
le23 : μ s₂ ≤ μ s₃
key : μ s₃ ≤ μ s₁
⊢ μ s₁ = μ s₂ ∧ μ s₂ = μ s₃

Tactic:
exact ⟨le12.antisymm (le23.trans key), le23.antisymm (key.trans le12)⟩

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_eq_one : conjneg f = 1 ↔ f = 1

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ conjneg f = 1 ↔ f = 1

Tactic:
rw [← conjneg_inj, conjneg_conjneg, conjneg_one]

Result:
no goals
-- Mathlib/Data/Nat/SuccPred.lean
theorem pred_iterate (a : ℕ) : ∀ n, pred^[n] a = a - n
  | 0 => rfl
  | n + 1 => by
    rw [Function.iterate_succ', sub_succ]
    exact congr_arg _ (Nat.pred_iterate a n)

Proof state:
a n : ℕ
⊢ (pred ∘ pred^[n]) a = (a - n).pred

Tactic:
exact congr_arg _ (Nat.pred_iterate a n)

Result:
no goals

Proof state:
a n : ℕ
⊢ pred^[n + 1] a = a - (n + 1)

Tactic:
rw [Function.iterate_succ', sub_succ]

Result:
a n : ℕ
⊢ (pred ∘ pred^[n]) a = (a - n).pred
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem UniformContinuous.inv [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :
    UniformContinuous fun x => (f x)⁻¹

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
this : UniformContinuous fun x => 1 / f x
⊢ UniformContinuous fun x => (f x)⁻¹

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x => (f x)⁻¹

Tactic:
have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf

Result:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
this : UniformContinuous fun x => 1 / f x
⊢ UniformContinuous fun x => (f x)⁻¹
-- Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean
@[simp] lemma toDirectLimit_tmul_of
    {i : ι} (g : G i) (m : M) :
    (toDirectLimit f M <| (of _ _ G f i g) ⊗ₜ m) = (of _ _ _ _ i (g ⊗ₜ m))

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
g : G i
m : M
⊢ (((mk R (G i) M).compr₂ (of R ι (fun _i => G _i ⊗[R] M) (fun _i _j h => LinearMap.rTensor M (f _i _j h)) i)) g) m =
    (of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
g : G i
m : M
⊢ (toDirectLimit f M) ((of R ι G f i) g ⊗ₜ[R] m) =
    (of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)

Tactic:
rw [toDirectLimit, lift.tmul, lift_of]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
g : G i
m : M
⊢ (((mk R (G i) M).compr₂ (of R ι (fun _i => G _i ⊗[R] M) (fun _i _j h => LinearMap.rTensor M (f _i _j h)) i)) g) m =
    (of R ι (fun x => G x ⊗[R] M) (fun i j h => LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem toSheafify_naturality {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
    η ≫ J.toSheafify _ = J.toSheafify _ ≫ J.sheafifyMap η

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ η ≫ J.toSheafify Q = J.toSheafify P ≫ J.sheafifyMap η

Tactic:
dsimp [sheafifyMap, sheafify, 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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ η ≫ J.toPlus Q ≫ J.plusMap (J.toPlus Q) = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ J.plusMap (J.plusMap η)

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 Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ η ≫ J.toPlus Q ≫ J.plusMap (J.toPlus Q) = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ J.plusMap (J.plusMap η)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparator_prod_of_isCoseparator_left (G H : C) [HasBinaryProduct G H]
    (hG : IsCoseparator G) : IsCoseparator (G ⨯ H) :=
  (isCoseparator_prod _ _).2 <| IsCoseparating.mono hG <| by simp

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hG : IsCoseparator G
⊢ {G} ⊆ {G, H}

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb_or {x : BitVec w} {hi lo : Nat} :
   (x ||| y).extractLsb lo hi = (x.extractLsb lo hi) ||| (y.extractLsb lo hi)

Proof state:
w : Nat
y x : BitVec w
hi lo : Nat
⊢ extractLsb lo hi (x ||| y) = extractLsb lo hi x ||| extractLsb lo hi y

Tactic:
ext k hk

Result:
case pred
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ (extractLsb lo hi (x ||| y)).getLsbD k = (extractLsb lo hi x ||| extractLsb lo hi y).getLsbD k

Proof state:
case pred
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ (extractLsb lo hi (x ||| y)).getLsbD k = (extractLsb lo hi x ||| extractLsb lo hi y).getLsbD k

Tactic:
simp [hk, show k ≤ lo - hi by omega]

Result:
no goals

Proof state:
w : Nat
y x : BitVec w
hi lo k : Nat
hk : k < lo - hi + 1
⊢ k ≤ lo - hi

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Finset/Finsupp.lean
theorem card_pi (f : ι →₀ Finset α) : #f.pi = f.prod fun i ↦ #(f i)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι →₀ Finset α
⊢ #f.pi = f.prod fun i => ↑(#(f i))

Tactic:
rw [pi, card_finsupp]

Result:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι →₀ Finset α
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i => ↑(#(f i))

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι →₀ Finset α
⊢ ∏ i ∈ f.support, #(f i) = f.prod fun i => ↑(#(f i))

Tactic:
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
f : ι →₀ Finset α
i : ι
x✝ : i ∈ f.support
⊢ #(f i) = (fun i => ↑(#(f i))) i (f i)

Tactic:
simp only [Pi.natCast_apply, Nat.cast_id]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
lemma length_lt_card (s : LTSeries α) : s.length < Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ Fintype.card α < Fintype.card (Fin (s.length + 1))

Tactic:
rw [Fintype.card_fin]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ Fintype.card α < s.length + 1

Proof state:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
this : ∀ (i j : Fin (s.length + 1)), i ≠ j → s.toFun i = s.toFun j → i < j → False
hl : ¬i < j
⊢ False

Tactic:
exact this j i hn.symm he.symm (by omega)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
this : ∀ (i j : Fin (s.length + 1)), i ≠ j → s.toFun i = s.toFun j → i < j → False
hl : ¬i < j
⊢ j < i

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ False

Tactic:
obtain ⟨i, j, hn, he⟩ := Fintype.exists_ne_map_eq_of_card_lt s (by rw [Fintype.card_fin]; omega)

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
hl : i < j
⊢ False

Tactic:
exact absurd he (s.strictMono hl).ne

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
⊢ False

Tactic:
wlog hl : i < j generalizing i j

Result:
case intro.intro.intro.inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
this : ∀ (i j : Fin (s.length + 1)), i ≠ j → s.toFun i = s.toFun j → i < j → False
hl : ¬i < j
⊢ False

α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
i j : Fin (s.length + 1)
hn : i ≠ j
he : s.toFun i = s.toFun j
hl : i < j
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ Fintype.card α < s.length + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
⊢ s.length < Fintype.card α

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Fintype α
s : LTSeries α
h : Fintype.card α ≤ s.length
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.getD_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {a : α}
    {fallback : β} : Raw.Const.getD m a fallback =
      Raw₀.Const.getD ⟨m, h.size_buckets_pos⟩ a fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
h : m.WF
a : α
fallback : β
⊢ Raw.Const.getD m a fallback = Raw₀.Const.getD ⟨m, ⋯⟩ a fallback

Tactic:
simp [Raw.Const.getD, h.size_buckets_pos]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.MeasurableEmbedding.aestronglyMeasurable_map_iff {γ : Type*}
    {mγ : MeasurableSpace γ} {mα : MeasurableSpace α} {f : γ → α} {μ : Measure γ}
    (hf : MeasurableEmbedding f) {g : α → β} :
    AEStronglyMeasurable g (Measure.map f μ) ↔ AEStronglyMeasurable (g ∘ f) μ

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
g₁ : γ → β
hgm₁ : StronglyMeasurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEStronglyMeasurable g (Measure.map f μ)

Tactic:
rcases hf.exists_stronglyMeasurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g g₂ : α → β
hgm₂ : StronglyMeasurable g₂
hgm₁ : StronglyMeasurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEStronglyMeasurable g (Measure.map f μ)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable g (Measure.map f μ) ↔ AEStronglyMeasurable (g ∘ f) μ

Tactic:
refine ⟨fun H => H.comp_measurable hf.measurable, ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable g (Measure.map f μ)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g g₂ : α → β
hgm₂ : StronglyMeasurable g₂
hgm₁ : StronglyMeasurable (g₂ ∘ f)
heq : g ∘ f =ᶠ[ae μ] g₂ ∘ f
⊢ AEStronglyMeasurable g (Measure.map f μ)

Tactic:
exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
⊢ AEStronglyMeasurable (g ∘ f) μ → AEStronglyMeasurable g (Measure.map f μ)

Tactic:
rintro ⟨g₁, hgm₁, heq⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
g₁ : γ → β
hgm₁ : StronglyMeasurable g₁
heq : g ∘ f =ᶠ[ae μ] g₁
⊢ AEStronglyMeasurable g (Measure.map f μ)
-- Mathlib/CategoryTheory/Closed/Functor.lean
theorem expComparison_iso_of_frobeniusMorphism_iso (h : L ⊣ F) (A : C)
    [i : IsIso (frobeniusMorphism F h A)] : IsIso (expComparison F A).natTrans

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso
    ((conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (frobeniusMorphism F h A).natTrans)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso (expComparison F A).natTrans

Tactic:
rw [← frobeniusMorphism_mate F h]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (frobeniusMorphism F h A)
⊢ IsIso
    ((conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (frobeniusMorphism F h A).natTrans)