harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.mul (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
    HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x

Proof state:
case h.e'_12.h.e'_6
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ d x • c' = c'.smulRight (d x)

Tactic:
ext z

Result:
case h.e'_12.h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
z : E
⊢ (d x • c') z = (c'.smulRight (d x)) z

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x

Tactic:
convert hc.mul' hd

Result:
case h.e'_12.h.e'_6
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ d x • c' = c'.smulRight (d x)

Proof state:
case h.e'_12.h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
z : E
⊢ (d x • c') z = (c'.smulRight (d x)) z

Tactic:
apply mul_comm

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma primitiveCharacter_one (hn : n ≠ 0) :
    (1 : DirichletCharacter R n).primitiveCharacter = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
hn : n ≠ 0
⊢ primitiveCharacter 1 = 1

Tactic:
rw [eq_one_iff_conductor_eq_one <| (@conductor_one R _ _ hn) ▸ Nat.one_ne_zero,
    (isPrimitive_def _).1 (1 : DirichletCharacter R n).primitiveCharacter_isPrimitive,
    conductor_one hn]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_inter_union_subset {f : α → α → β} {s t : Finset α} (hf : ∀ a b, f a b = f b a) :
    image₂ f (s ∩ t) (s ∪ t) ⊆ image₂ f s t :=
  coe_subset.1 <| by
    push_cast
    exact image2_inter_union_subset hf

Proof state:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (↑s ∩ ↑t) (↑s ∪ ↑t) ⊆ image2 f ↑s ↑t

Tactic:
exact image2_inter_union_subset hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ ↑(image₂ f (s ∩ t) (s ∪ t)) ⊆ ↑(image₂ f s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → α → β
s t : Finset α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (↑s ∩ ↑t) (↑s ∪ ↑t) ⊆ image2 f ↑s ↑t
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem isUniformInducing_iff [PseudoMetricSpace β] {f : α → β} :
    IsUniformInducing f ↔ UniformContinuous f ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ :=
  isUniformInducing_iff'.trans <| Iff.rfl.and <|
    ((uniformity_basis_dist.comap _).le_basis_iff uniformity_basis_dist).trans <| by
      simp only [subset_def, Prod.forall, gt_iff_lt, preimage_setOf_eq, Prod.map_apply, mem_setOf]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ), 0 < i' → ∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | dist p.1 p.2 < i} ⊆ {p | dist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
simp only [subset_def, Prod.forall, gt_iff_lt, preimage_setOf_eq, Prod.map_apply, mem_setOf]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem pred_eq_iff_not_succ {o} : pred o = o ↔ ¬∃ a, o = succ a :=
  ⟨fun e ⟨a, e'⟩ => by rw [e', pred_succ] at e; exact (lt_succ a).ne e, fun h => dif_neg h⟩

Proof state:
o : Ordinal.{u_4}
e : o.pred = o
x✝ : ∃ a, o = succ a
a : Ordinal.{u_4}
e' : o = succ a
⊢ False

Tactic:
rw [e', pred_succ] at e

Result:
o : Ordinal.{u_4}
x✝ : ∃ a, o = succ a
a : Ordinal.{u_4}
e : a = succ a
e' : o = succ a
⊢ False

Proof state:
o : Ordinal.{u_4}
x✝ : ∃ a, o = succ a
a : Ordinal.{u_4}
e : a = succ a
e' : o = succ a
⊢ False

Tactic:
exact (lt_succ a).ne e

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem inv_mul_cancel_right (a : α) (b : αˣ) : a * ↑b⁻¹ * b = a

Proof state:
α : Type u
inst✝ : Monoid α
a : α
b : αˣ
⊢ a * ↑b⁻¹ * ↑b = a

Tactic:
rw [mul_assoc, inv_mul, mul_one]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Basic.lean
theorem basicOpen_le {U : Opens X} (f : X.presheaf.obj (op U)) : X.basicOpen f ≤ U

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ X.basicOpen f ≤ U

Tactic:
rintro x ⟨h, _⟩

Result:
case intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
h : x ∈ U
h✝ : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x h)) f)
⊢ x ∈ ↑U

Proof state:
case intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
h : x ∈ U
h✝ : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x h)) f)
⊢ x ∈ ↑U

Tactic:
exact h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Lean/Except.lean
theorem pmap_id {ε : Type u} {α : Type v} (x : Except ε α) :
    x.pmap (fun a _ => a) = x

Proof state:
ε : Type u
α : Type v
x : Except ε α
⊢ (x.pmap fun a x => a) = x

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_le' (n : ℕ) : sqrt n ^ 2 ≤ n

Proof state:
n : ℕ
⊢ n.sqrt ^ 2 ≤ n

Tactic:
simpa [Nat.pow_two] using sqrt_le n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_congr [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α}
    {fallback : β} (hab : a == b) : getValueD a l fallback = getValueD b l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
a b : α
fallback : β
hab : (a == b) = true
⊢ getValueD a l fallback = getValueD b l fallback

Tactic:
simp only [getValueD_eq_getValue?, getValue?_congr hab]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then `f` is an antitone
function. -/
lemma antitone_of_hasDerivAt_nonpos {f f' : ℝ → ℝ} (hf : ∀ x, HasDerivAt f (f' x) x)
    (hf' : f' ≤ 0) : Antitone f :=
  antitone_of_deriv_nonpos (fun _ ↦ (hf _).differentiableAt) fun x ↦ by
    rw [(hf _).deriv]; exact hf' _

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0

Tactic:
exact hf' _

Result:
no goals

Proof state:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ deriv f x ≤ 0

Tactic:
rw [(hf _).deriv]

Result:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem map_comp (C : G.ConnectedComponent) (φ : G →g G') (ψ : G' →g G'') :
    (C.map φ).map ψ = C.map (ψ.comp φ)

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : G.ConnectedComponent
φ : G →g G'
ψ : G' →g G''
⊢ ∀ (v : V), map ψ (map φ (G.connectedComponentMk v)) = map (ψ.comp φ) (G.connectedComponentMk v)

Tactic:
exact fun _ => rfl

Result:
no goals

Proof state:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : G.ConnectedComponent
φ : G →g G'
ψ : G' →g G''
⊢ map ψ (map φ C) = map (ψ.comp φ) C

Tactic:
refine C.ind ?_

Result:
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : G.ConnectedComponent
φ : G →g G'
ψ : G' →g G''
⊢ ∀ (v : V), map ψ (map φ (G.connectedComponentMk v)) = map (ψ.comp φ) (G.connectedComponentMk v)
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem LinearMap.lift_rank_le_of_surjective (f : M →ₗ[R] M') (h : Surjective f) :
    lift.{v} (Module.rank R M') ≤ lift.{v'} (Module.rank R M)

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R ↥(range f)) ≤ lift.{v', v} (Module.rank R M)

Tactic:
apply lift_rank_range_le

Result:
no goals

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
rw [← rank_range_of_surjective f h]

Result:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
h : Surjective ⇑f
⊢ lift.{v, v'} (Module.rank R ↥(range f)) ≤ lift.{v', v} (Module.rank R M)
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/CrossProduct.lean
theorem norm_withLpEquiv_symm_crossProduct (a b : Fin 3 → ℝ) :
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm (a ×₃ b)‖ =
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm a‖ * ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm b‖ *
      sin (angle ((WithLp.equiv 2 (Fin 3 → ℝ)).symm a) ((WithLp.equiv 2 (Fin 3 → ℝ)).symm b))

Proof state:
a b : Fin 3 → ℝ
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct a) b)‖ =
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm a‖ * ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm b‖ *
      sin (angle ((WithLp.equiv 2 (Fin 3 → ℝ)).symm a) ((WithLp.equiv 2 (Fin 3 → ℝ)).symm b))

Tactic:
rw [← norm_withLpEquiv_crossProduct ((WithLp.equiv _ _).symm a) ((WithLp.equiv _ _).symm b)]

Result:
a b : Fin 3 → ℝ
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct a) b)‖ =
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) ((WithLp.equiv 2 ((i : Fin 3) → (fun x => ℝ) i)).symm a)))
          ((WithLp.equiv 2 (Fin 3 → ℝ)) ((WithLp.equiv 2 ((i : Fin 3) → (fun x => ℝ) i)).symm b)))‖

Proof state:
a b : Fin 3 → ℝ
⊢ ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct a) b)‖ =
    ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm
        ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) ((WithLp.equiv 2 ((i : Fin 3) → (fun x => ℝ) i)).symm a)))
          ((WithLp.equiv 2 (Fin 3 → ℝ)) ((WithLp.equiv 2 ((i : Fin 3) → (fun x => ℝ) i)).symm b)))‖

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem le_refl : ∀ (x : Bool), x ≤ x

Proof state:
⊢ ∀ (x : Bool), x ≤ x

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem MeasurePreserving.setLIntegral_comp_emb {mb : MeasurableSpace β} {ν : Measure β}
    {g : α → β} (hg : MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ℝ≥0∞)
    (s : Set α) : ∫⁻ a in s, f (g a) ∂μ = ∫⁻ b in g '' s, f b ∂ν

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set α
⊢ ∫⁻ (a : α) in s, f (g a) ∂μ = ∫⁻ (b : β) in g '' s, f b ∂ν

Tactic:
rw [← hg.setLIntegral_comp_preimage_emb hge, preimage_image_eq _ hge.injective]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem foldl_one (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) : foldl Q f hf n 1 = n

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
⊢ ((foldl Q f hf) n) 1 = n

Tactic:
rw [← foldr_reverse, reverse.map_one, foldr_one]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_cyclicPermutations_iff {l l' : List α} :
    l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'

Proof state:
α : Type u
l l' : List α
⊢ l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'

Tactic:
simp only [IsRotated, ← cyclicPermutations_rotate, cyclicPermutations_inj]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
@[simp]
lemma dualBasis_dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) (hB' : B.IsSymm) {ι}
    [Finite ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) :
    B.dualBasis hB (B.dualBasis hB b) = b

Proof state:
case h.e'_2.h.e'_9
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
ι : Type u_10
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : FiniteDimensional K V
b : Basis ι K V
⊢ B = B.flip

Tactic:
rwa [eq_comm, ← isSymm_iff_flip]

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
ι : Type u_10
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : FiniteDimensional K V
b : Basis ι K V
⊢ B.dualBasis hB (B.dualBasis hB b) = b

Tactic:
convert dualBasis_dualBasis_flip _ hB.flip b

Result:
case h.e'_2.h.e'_9
V : Type u_5
K : Type u_6
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B : BilinForm K V
hB : B.Nondegenerate
hB' : B.IsSymm
ι : Type u_10
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : FiniteDimensional K V
b : Basis ι K V
⊢ B = B.flip
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_map {f : α → β} {g : β → Option γ} {x : Option α} :
    (x.map f).bind g = x.bind (g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → Option γ
x : Option α
⊢ (Option.map f x).bind g = x.bind (g ∘ f)

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem δ_naturality {m n : M} {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal]:
    (δ F m n).app X ≫ (F.obj n).map ((F.obj m).map f) =
      (F.obj _).map f ≫ (δ F m n).app Y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n : M
X Y : C
f : X ⟶ Y
inst✝ : F.OplaxMonoidal
⊢ (δ F m n).app X ≫ (F.obj n).map ((F.obj m).map f) = (F.obj (m ⊗ n)).map f ≫ (δ F m n).app Y

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem id_tensor_associator_inv_naturality {X Y Z X' : C} (f : X ⟶ X') :
    (f ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z X' : C
f : X ⟶ X'
⊢ (f ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z)

Tactic:
rw [← tensor_id, associator_inv_naturality]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean
theorem GradedAlgebra.ι_sq_scalar (m : M) :
    GradedAlgebra.ι Q m * GradedAlgebra.ι Q m = algebraMap R _ (Q m)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (GradedAlgebra.ι Q) m * (GradedAlgebra.ι Q) m = (algebraMap R (⨁ (i : ZMod 2), ↥(evenOdd Q i))) (Q m)

Tactic:
rw [GradedAlgebra.ι_apply Q, DirectSum.of_mul_of, DirectSum.algebraMap_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) (1 + 1)) (GradedMonoid.GMul.mul ⟨(ι Q) m, ⋯⟩ ⟨(ι Q) m, ⋯⟩) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) 0) (DirectSum.GAlgebra.toFun (Q m))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (DirectSum.of (fun i => ↥(evenOdd Q i)) (1 + 1)) (GradedMonoid.GMul.mul ⟨(ι Q) m, ⋯⟩ ⟨(ι Q) m, ⋯⟩) =
    (DirectSum.of (fun i => ↥(evenOdd Q i)) 0) (DirectSum.GAlgebra.toFun (Q m))

Tactic:
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext rfl <| ι_sq_scalar _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] :
    ¬a ∈ m → m.get! a = default

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
a : α
inst✝ : Inhabited (β a)
⊢ ¬a ∈ m → m.get! a = default

Tactic:
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_cons_of_true [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} (h : k == a) :
    getValueCast? a (⟨k, v⟩ :: l) = some (cast (congrArg β (eq_of_beq h)) v)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ getValueCast? a (⟨k, v⟩ :: l) = some (cast ⋯ v)

Tactic:
simp [getValueCast?, h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrable_mul_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) :
    Integrable fun x : ℝ => x * exp (-b * x ^ 2)

Proof state:
b : ℝ
hb : 0 < b
⊢ Integrable (fun x => x * rexp (-b * x ^ 2)) volume

Tactic:
simpa using integrable_rpow_mul_exp_neg_mul_sq hb (by norm_num : (-1 : ℝ) < 1)

Result:
no goals

Proof state:
b : ℝ
hb : 0 < b
⊢ -1 < 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/W/Cardinal.lean
theorem cardinalMk_le_max_aleph0_of_finite [∀ a, Finite (β a)] : #(WType β) ≤ max #α ℵ₀ :=
  cardinalMk_le_max_aleph0_of_finite'.trans_eq <| by rw [lift_id]

Proof state:
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ lift.{u, u} #α ⊔ ℵ₀ = #α ⊔ ℵ₀

Tactic:
rw [lift_id]

Result:
no goals
-- Mathlib/Topology/Instances/Real/Lemmas.lean
theorem Real.cobounded_eq : cobounded ℝ = atBot ⊔ atTop

Proof state:
⊢ cobounded ℝ = atBot ⊔ atTop

Tactic:
simp only [← comap_dist_right_atTop (0 : ℝ), Real.dist_eq, sub_zero, comap_abs_atTop]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_mul_le_left [StrongRankCondition R] (A : Matrix m n R) (B : Matrix n o R) :
    (A * B).rank ≤ A.rank

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ finrank R ↥(LinearMap.range (A.mulVecLin ∘ₗ B.mulVecLin)) ≤ finrank R ↥(LinearMap.range A.mulVecLin)

Tactic:
exact Cardinal.toNat_le_toNat (LinearMap.rank_comp_le_left _ _) (rank_lt_aleph0 _ _)

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ (A * B).rank ≤ A.rank

Tactic:
rw [rank, rank, mulVecLin_mul]

Result:
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_5
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix m n R
B : Matrix n o R
⊢ finrank R ↥(LinearMap.range (A.mulVecLin ∘ₗ B.mulVecLin)) ≤ finrank R ↥(LinearMap.range A.mulVecLin)
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_add_one (a : α) : ⌊a + 1⌋ = ⌊a⌋ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌊a + 1⌋ = ⌊a⌋ + 1

Tactic:
rw [← cast_one, floor_add_int]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem sInf_empty : sInf (∅ : Set ℝ) = 0

Proof state:
⊢ sInf ∅ = 0

Tactic:
simp [sInf_def, sSup_empty]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem prod_fst_mk {α β : TypeVec n} (i : Fin2 n) (a : α i) (b : β i) :
    TypeVec.prod.fst i (prod.mk i a b) = a

Proof state:
case fz
n n✝ : ℕ
α β : TypeVec.{u_1} (n✝ + 1)
a : α Fin2.fz
b : β Fin2.fz
⊢ prod.fst Fin2.fz (prod.mk Fin2.fz a b) = a

Tactic:
simp_all only [prod.fst, prod.mk]

Result:
no goals

Proof state:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec.{u_1} n✝} (a : α a✝) (b : β a✝), prod.fst a✝ (prod.mk a✝ a b) = a
α β : TypeVec.{u_1} (n✝ + 1)
a : α a✝.fs
b : β a✝.fs
⊢ prod.fst a✝.fs (prod.mk a✝.fs a b) = a

Tactic:
apply i_ih

Result:
no goals

Proof state:
n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.fst i (prod.mk i a b) = a

Tactic:
induction i with
| fz => simp_all only [prod.fst, prod.mk]
| fs _ i_ih => apply i_ih

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_smul {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E]
    [SMulCommClass ℝ 𝕜 E] (r : 𝕜) (f : ℝ → E) :
    ∫ x in a..b, r • f x ∂μ = r • ∫ x in a..b, f x ∂μ

Proof state:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
𝕜 : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
r : 𝕜
f : ℝ → E
⊢ ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
simp only [intervalIntegral, integral_smul, smul_sub]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem edist_le_of_le (h : HolderOnWith C r f s) {x y : X} (hx : x ∈ s) (hy : y ∈ s) {d : ℝ≥0∞}
    (hd : edist x y ≤ d) : edist (f x) (f y) ≤ (C : ℝ≥0∞) * d ^ (r : ℝ) :=
  (h.edist_le hx hy).trans <| by gcongr

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
x y : X
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0∞
hd : edist x y ≤ d
⊢ ↑C * edist x y ^ ↑r ≤ ↑C * d ^ ↑r

Tactic:
gcongr

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem modular_T_zpow_smul (z : ℍ) (n : ℤ) : ModularGroup.T ^ n • z = (n : ℝ) +ᵥ z

Proof state:
z : ℍ
n : ℤ
⊢ (↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 0 1))) /
      (↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 1 1))) =
    ↑z + ↑↑n

Tactic:
simp [toGL, ModularGroup.coe_T_zpow,
  of_apply, cons_val_zero, algebraMap.coe_one, Complex.ofReal_one, one_mul, cons_val_one,
  head_cons, algebraMap.coe_zero, zero_mul, zero_add, div_one]

Result:
no goals

Proof state:
z : ℍ
n : ℤ
⊢ ModularGroup.T ^ n • z = ↑n +ᵥ z

Tactic:
rw [UpperHalfPlane.ext_iff, coe_vadd, add_comm, specialLinearGroup_apply, coe_mk]

Result:
z : ℍ
n : ℤ
⊢ (↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 0 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 0 1))) /
      (↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 1 0)) * ↑z + ↑((algebraMap ℤ ℝ) (↑(ModularGroup.T ^ n) 1 1))) =
    ↑z + ↑↑n
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem add_lt_aleph0 {a b : Cardinal} (ha : a < ℵ₀) (hb : b < ℵ₀) : a + b < ℵ₀ :=
  match a, b, lt_aleph0.1 ha, lt_aleph0.1 hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by rw [← Nat.cast_add]; apply nat_lt_aleph0

Proof state:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m + n) < ℵ₀

Tactic:
apply nat_lt_aleph0

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m + ↑n < ℵ₀

Tactic:
rw [← Nat.cast_add]

Result:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m + n) < ℵ₀
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ico_succ_succ_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) :
    Ico (succ a) (succ b) = Ioc a b :=
  coe_injective <| by simpa using Set.Ico_succ_succ_eq_Ioc_of_not_isMax hb _

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ ↑(Ico (succ a) (succ b)) = ↑(Ioc a b)

Tactic:
simpa using Set.Ico_succ_succ_eq_Ioc_of_not_isMax hb _

Result:
no goals
-- Mathlib/Data/Finset/Empty.lean
theorem coe_eq_empty {s : Finset α} : (s : Set α) = ∅ ↔ s = ∅

Proof state:
α : Type u_1
s : Finset α
⊢ ↑s = ∅ ↔ s = ∅

Tactic:
rw [← coe_empty, coe_inj]

Result:
no goals