harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem linearMap_comp_mul' :
    Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R =
      map (Algebra.linearMap R A) (Algebra.linearMap R B)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R = map (Algebra.linearMap R A) (Algebra.linearMap R B)

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ((AlgebraTensorModule.curry (Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R)) 1) 1 =
    ((AlgebraTensorModule.curry (map (Algebra.linearMap R A) (Algebra.linearMap R B))) 1) 1

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ ((AlgebraTensorModule.curry (Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R)) 1) 1 =
    ((AlgebraTensorModule.curry (map (Algebra.linearMap R A) (Algebra.linearMap R B))) 1) 1

Tactic:
simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars, map_tmul,
  Algebra.linearMap_apply, _root_.map_one, LinearMap.coe_comp, Function.comp_apply,
  LinearMap.mul'_apply, mul_one, Algebra.TensorProduct.one_def]

Result:
no goals
-- Mathlib/Data/List/NatAntidiagonal.lean
theorem antidiagonal_succ {n : ℕ} :
    antidiagonal (n + 1) = (0, n + 1) :: (antidiagonal n).map (Prod.map Nat.succ id)

Proof state:
n : ℕ
⊢ antidiagonal (n + 1) = (0, n + 1) :: map (Prod.map succ id) (antidiagonal n)

Tactic:
simp only [antidiagonal, range_succ_eq_map, map_cons, Nat.add_succ_sub_one,
  Nat.add_zero, id, eq_self_iff_true, Nat.sub_zero, map_map, Prod.map_apply]

Result:
n : ℕ
⊢ (0, n + 1) :: (succ 0, n) :: map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    (0, n + 1) :: (succ 0, n) :: map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)

Proof state:
n : ℕ
⊢ (0, n + 1) :: (succ 0, n) :: map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    (0, n + 1) :: (succ 0, n) :: map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)

Tactic:
apply congr rfl (congr rfl _)

Result:
n : ℕ
⊢ map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)

Proof state:
n : ℕ
⊢ map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n) =
    map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n)

Tactic:
ext

Result:
case h.a
n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ (map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n))[i✝]? ↔
    a✝ ∈ (map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n))[i✝]?

Proof state:
case h.a
n i✝ : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ (map ((fun i => (i, n + 1 - i)) ∘ succ ∘ succ) (range n))[i✝]? ↔
    a✝ ∈ (map (Prod.map succ id ∘ (fun i => (i, n - i)) ∘ succ) (range n))[i✝]?

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_self (n : BitVec w) : n >>> n.toNat = 0#w

Proof state:
w : Nat
n : BitVec w
⊢ n >>> n.toNat = 0#w

Tactic:
simp [BitVec.toNat_eq, Nat.shiftRight_eq_div_pow, Nat.lt_two_pow_self, Nat.div_eq_of_lt]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem cast_heq_iff_heq {α β γ : Sort _} (e : α = β) (a : α) (c : γ) :
    HEq (cast e a) c ↔ HEq a c

Proof state:
α β γ : Sort u_1
e : α = β
a : α
c : γ
⊢ HEq (cast e a) c ↔ HEq a c

Tactic:
subst e

Result:
α γ : Sort u_1
a : α
c : γ
⊢ HEq (cast ⋯ a) c ↔ HEq a c

Proof state:
α γ : Sort u_1
a : α
c : γ
⊢ HEq (cast ⋯ a) c ↔ HEq a c

Tactic:
rfl

Result:
no goals
-- Mathlib/RepresentationTheory/Character.lean
theorem char_orthonormal (V W : FDRep k G) [Simple V] [Simple W] :
    ⅟ (Fintype.card G : k) • ∑ g : G, V.character g * W.character g⁻¹ =
      if Nonempty (V ≅ W) then ↑1 else ↑0

Proof state:
k : Type u
inst✝⁶ : Field k
G : Type u
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Fintype.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k (W ⟶ V)) = if Nonempty (V ≅ W) then 1 else 0

Tactic:
rw_mod_cast [finrank_hom_simple_simple W V, Iso.nonempty_iso_symm]

Result:
no goals

Proof state:
k : Type u
inst✝⁶ : Field k
G : Type u
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Fintype.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k
        ↥(invariants
            ((↑(of (linHom W.ρ V.ρ)).V.obj.endRingEquiv).comp
              ((FGModuleCat.of k (↑W.V →ₗ[k] ↑V.V)).obj.endRingEquiv.symm.toMonoidHom.comp (linHom W.ρ V.ρ))))) =
    if Nonempty (V ≅ W) then 1 else 0

Tactic:
erw [(linHom.invariantsEquivFDRepHom W V).finrank_eq]

Result:
k : Type u
inst✝⁶ : Field k
G : Type u
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Fintype.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k (W ⟶ V)) = if Nonempty (V ≅ W) then 1 else 0

Proof state:
k : Type u
inst✝⁶ : Field k
G : Type u
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Fintype.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ⅟↑(Fintype.card G) • ∑ g : G, V.character g * W.character g⁻¹ = if Nonempty (V ≅ W) then 1 else 0

Tactic:
conv_lhs =>
  enter [2, 2, g]
  rw [mul_comm, ← char_dual, ← Pi.mul_apply, ← char_tensor]
  rw [char_iso (FDRep.dualTensorIsoLinHom W.ρ V)]

Result:
k : Type u
inst✝⁶ : Field k
G : Type u
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Fintype.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ⅟↑(Fintype.card G) • Finset.univ.sum (of (linHom W.ρ V.ρ)).character = if Nonempty (V ≅ W) then 1 else 0

Proof state:
k : Type u
inst✝⁶ : Field k
G : Type u
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Fintype.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ⅟↑(Fintype.card G) • Finset.univ.sum (of (linHom W.ρ V.ρ)).character = if Nonempty (V ≅ W) then 1 else 0

Tactic:
rw [average_char_eq_finrank_invariants, ← FDRep.endRingEquiv_comp_ρ (of _),
    FDRep.of_ρ (linHom W.ρ V.ρ)]

Result:
k : Type u
inst✝⁶ : Field k
G : Type u
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Fintype.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k
        ↥(invariants
            ((↑(of (linHom W.ρ V.ρ)).V.obj.endRingEquiv).comp
              ((FGModuleCat.of k (↑W.V →ₗ[k] ↑V.V)).obj.endRingEquiv.symm.toMonoidHom.comp (linHom W.ρ V.ρ))))) =
    if Nonempty (V ≅ W) then 1 else 0
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_sInter {x y : Class.{u}} (h : x.Nonempty) : y ∈ ⋂₀ x ↔ ∀ z, z ∈ x → y ∈ z

Proof state:
x y : Class.{u}
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
refine ⟨fun hy z => mem_of_mem_sInter hy, fun H => ?_⟩

Result:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋂₀ x

Proof state:
case intro.intro.intro
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right✝ : ↑z y
H : ∀ z ∈ x, ↑y ∈ z
⊢ ∃ x_1, ↑x_1 = ↑y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
refine ⟨y, rfl, fun w hxw => ?_⟩

Result:
case intro.intro.intro
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right✝ : ↑z y
H : ∀ z ∈ x, ↑y ∈ z
w : ZFSet.{u}
hxw : x w
⊢ y ∈ w

Proof state:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋂₀ x

Tactic:
simp_rw [mem_def, sInter_apply]

Result:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Proof state:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
obtain ⟨z, hz⟩ := h

Result:
case intro
x y : Class.{u}
H : ∀ z ∈ x, y ∈ z
z : ZFSet.{u}
hz : z ∈ x
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Proof state:
case intro.intro.intro
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right✝ : ↑z y
H : ∀ z ∈ x, ↑y ∈ z
w : ZFSet.{u}
hxw : x w
⊢ y ∈ w

Tactic:
simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)

Result:
no goals

Proof state:
case intro
x y : Class.{u}
H : ∀ z ∈ x, y ∈ z
z : ZFSet.{u}
hz : z ∈ x
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)

Result:
case intro.intro.intro
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right✝ : ↑z y
H : ∀ z ∈ x, ↑y ∈ z
⊢ ∃ x_1, ↑x_1 = ↑y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
-- Mathlib/Analysis/Subadditive.lean
theorem lim_le_div (hbdd : BddBelow (range fun n => u n / n)) {n : ℕ} (hn : n ≠ 0) :
    h.lim ≤ u n / n

Proof state:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n => u n / ↑n) '' Ici 1) ≤ u n / ↑n

Tactic:
exact csInf_le (hbdd.mono <| image_subset_range _ _) ⟨n, hn.bot_lt, rfl⟩

Result:
no goals

Proof state:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ h.lim ≤ u n / ↑n

Tactic:
rw [Subadditive.lim]

Result:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n => u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n => u n / ↑n) '' Ici 1) ≤ u n / ↑n
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_injective : (toMeasure : PMF α → Measure α).Injective

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
⊢ Function.Injective toMeasure

Tactic:
intro p q h

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
⊢ p = q

Proof state:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
x : α
⊢ p x = q x

Tactic:
rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x,
  ← q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
⊢ p = q

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p q : PMF α
h : p.toMeasure = q.toMeasure
x : α
⊢ p x = q x
-- Mathlib/Data/Set/Lattice.lean
theorem subset_iInter₂_iff {s : Set α} {t : ∀ i, κ i → Set α} :
    (s ⊆ ⋂ (i) (j), t i j) ↔ ∀ i j, s ⊆ t i j

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ⊆ ⋂ i, ⋂ j, t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j

Tactic:
simp_rw [subset_iInter_iff]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem pbind_map (f : α → β) (x : Option α) (g : ∀ b : β, b ∈ x.map f → Option γ) :
    pbind (Option.map f x) g = x.pbind fun a h ↦ g (f a) (mem_map_of_mem _ h)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
x : Option α
g : (b : β) → b ∈ Option.map f x → Option γ
⊢ (Option.map f x).pbind g = x.pbind fun a h => g (f a) ⋯

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_eq_zero_iff' : orderOf x = 0 ↔ ∀ n : ℕ, 0 < n → x ^ n ≠ 1

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

Tactic:
simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem get_rotate (l : List α) (n : ℕ) (k : Fin (l.rotate n).length) :
    (l.rotate n).get k = l.get ⟨(k + n) % l.length, mod_lt _ (length_rotate l n ▸ k.pos)⟩

Proof state:
α : Type u
l : List α
n : ℕ
k : Fin (l.rotate n).length
⊢ (l.rotate n).get k = l.get ⟨(↑k + n) % l.length, ⋯⟩

Tactic:
simp [getElem_rotate]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_symmDiff_right :
    a ∆ (b ∆ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c :=
  calc
    a ∆ (b ∆ c) = a \ b ∆ c ⊔ b ∆ c \ a := symmDiff_def _ _
    _ = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))

Tactic:
rw [sdiff_symmDiff', sup_comm (a ⊓ b ⊓ c), symmDiff_sdiff]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Ring.lean
theorem Tendsto.atBot_mul_atBot₀ (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
have : Tendsto (fun x => -f x * -g x) l atTop :=
  (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ (tendsto_neg_atBot_atTop.comp hg)

Result:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x => -f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x => -f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
simpa only [neg_mul_neg] using this

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.left_eq_right_iff (h : s.IsDiameter p₁ p₂) : p₁ = p₂ ↔ s.radius = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ 2 * s.radius = 0 ↔ s.radius = 0

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ p₁ = p₂ ↔ s.radius = 0

Tactic:
rw [← dist_eq_zero, h.dist_left_right]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ 2 * s.radius = 0 ↔ s.radius = 0
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDerivWithin_of_isOpen (n : ℕ) (hs : IsOpen s) :
    EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s

Proof state:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (n + 1) f s x = iteratedFDeriv 𝕜 (n + 1) f x

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]

Result:
case succ
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
n : ℕ
IH : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
x : E
hx : x ∈ s
⊢ (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) x =
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)) x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
hs : IsOpen s
⊢ EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s

Tactic:
induction n with
| zero =>
  intro x _
  ext1
  simp only [iteratedFDerivWithin_zero_apply, iteratedFDeriv_zero_apply]
| succ n IH =>
  intro x hx
  rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]
  dsimp
  congr 1
  rw [fderivWithin_of_isOpen hs hx]
  apply Filter.EventuallyEq.fderiv_eq
  filter_upwards [hs.mem_nhds hx]
  exact IH

Result:
no goals
-- Mathlib/Topology/Algebra/UniformMulAction.lean
@[to_additive]
lemma IsUniformInducing.uniformContinuousConstSMul [SMul M Y] [UniformContinuousConstSMul M Y]
    {f : X → Y} (hf : IsUniformInducing f) (hsmul : ∀ (c : M) x, f (c • x) = c • f x) :
    UniformContinuousConstSMul M X where
  uniformContinuous_const_smul c

Proof state:
M : Type v
X : Type x
Y : Type y
inst✝⁴ : UniformSpace X
inst✝³ : UniformSpace Y
inst✝² : SMul M X
inst✝¹ : SMul M Y
inst✝ : UniformContinuousConstSMul M Y
f : X → Y
hf : IsUniformInducing f
hsmul : ∀ (c : M) (x : X), f (c • x) = c • f x
c : M
⊢ UniformContinuous fun x => c • x

Tactic:
simpa only [hf.uniformContinuous_iff, Function.comp_def, hsmul]
  using hf.uniformContinuous.const_smul c

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k}
    {v' : β k'} (h : (k' == k) = false) :
    Perm (insertEntry k v (⟨k', v'⟩ :: l)) (⟨k', v'⟩ :: insertEntry k v l)

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
h✝ : containsKey k l = true
⊢ (replaceEntry k v (⟨k', v'⟩ :: l)).Perm (⟨k', v'⟩ :: replaceEntry k v l)

Tactic:
rw [replaceEntry_cons_of_false h]

Result:
no goals

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
h✝ : ¬containsKey k l = true
⊢ (⟨k, v⟩ :: ⟨k', v'⟩ :: l).Perm (⟨k', v'⟩ :: ⟨k, v⟩ :: l)

Tactic:
apply Perm.swap

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
⊢ (insertEntry k v (⟨k', v'⟩ :: l)).Perm (⟨k', v'⟩ :: insertEntry k v l)

Tactic:
simp only [insertEntry, containsKey_cons, h, Bool.false_or, cond_eq_if]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
⊢ (if containsKey k l = true then replaceEntry k v (⟨k', v'⟩ :: l) else ⟨k, v⟩ :: ⟨k', v'⟩ :: l).Perm
    (⟨k', v'⟩ :: if containsKey k l = true then replaceEntry k v l else ⟨k, v⟩ :: l)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
⊢ (if containsKey k l = true then replaceEntry k v (⟨k', v'⟩ :: l) else ⟨k, v⟩ :: ⟨k', v'⟩ :: l).Perm
    (⟨k', v'⟩ :: if containsKey k l = true then replaceEntry k v l else ⟨k, v⟩ :: l)

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
h✝ : containsKey k l = true
⊢ (replaceEntry k v (⟨k', v'⟩ :: l)).Perm (⟨k', v'⟩ :: replaceEntry k v l)

case isFalse
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v : β k
v' : β k'
h : (k' == k) = false
h✝ : ¬containsKey k l = true
⊢ (⟨k, v⟩ :: ⟨k', v'⟩ :: l).Perm (⟨k', v'⟩ :: ⟨k, v⟩ :: l)
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
lemma subset_verticalStrip_of_isCompact {K : Set ℍ} (hK : IsCompact K) :
    ∃ A B : ℝ, 0 < B ∧ K ⊆ verticalStrip A B

Proof state:
case inr.intro.intro.intro.intro
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left✝¹ : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
v : ℍ
left✝ : v ∈ K
hv : IsMinOn im K v
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
exact ⟨|re u|, im v, v.im_pos, fun k hk ↦ ⟨isMaxOn_iff.mp hu _ hk, isMinOn_iff.mp hv _ hk⟩⟩

Result:
no goals

Proof state:
K : Set ℍ
hK : IsCompact K
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
rcases K.eq_empty_or_nonempty with rfl | hne

Result:
case inl
hK : IsCompact ∅
⊢ ∃ A B, 0 < B ∧ ∅ ⊆ verticalStrip A B

case inr
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Proof state:
case inr
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
obtain ⟨u, _, hu⟩ := hK.exists_isMaxOn hne (_root_.continuous_abs.comp continuous_re).continuousOn

Result:
case inr.intro.intro
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left✝ : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Proof state:
case inr.intro.intro
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left✝ : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
obtain ⟨v, _, hv⟩ := hK.exists_isMinOn hne continuous_im.continuousOn

Result:
case inr.intro.intro.intro.intro
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left✝¹ : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
v : ℍ
left✝ : v ∈ K
hv : IsMinOn im K v
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Proof state:
case inl
hK : IsCompact ∅
⊢ ∃ A B, 0 < B ∧ ∅ ⊆ verticalStrip A B

Tactic:
exact ⟨1, 1, Real.zero_lt_one, empty_subset _⟩

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_def (a b : Nimber) :
    a + b = sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

Proof state:
a b : Nimber
⊢ a + b = sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

Tactic:
change Nimber.add a b = _

Result:
a b : Nimber
⊢ a.add b = sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

Proof state:
a b : Nimber
⊢ sInf {x | (∃ a' < a, a'.add b = x) ∨ ∃ b' < b, a.add b' = x}ᶜ =
    sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

Tactic:
rfl

Result:
no goals

Proof state:
a b : Nimber
⊢ a.add b = sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

Tactic:
rw [Nimber.add]

Result:
a b : Nimber
⊢ sInf {x | (∃ a', ∃ (_ : a' < a), a'.add b = x) ∨ ∃ b', ∃ (_ : b' < b), a.add b' = x}ᶜ =
    sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

Proof state:
a b : Nimber
⊢ sInf {x | (∃ a', ∃ (_ : a' < a), a'.add b = x) ∨ ∃ b', ∃ (_ : b' < b), a.add b' = x}ᶜ =
    sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ

Tactic:
simp_rw [exists_prop]

Result:
a b : Nimber
⊢ sInf {x | (∃ a' < a, a'.add b = x) ∨ ∃ b' < b, a.add b' = x}ᶜ =
    sInf {x | (∃ a' < a, a' + b = x) ∨ ∃ b' < b, a + b' = x}ᶜ