harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem toList_cons :
    (.cons x r s : RBNode.Stream α).toList = x :: r.toList ++ s.toList

Proof state:
α : Type u_1
x : α
r : RBNode α
s : RBNode.Stream α
⊢ x :: (r.toList ++ foldr (fun x1 x2 => x1 :: x2) s []) = x :: r.toList ++ foldr (fun x1 x2 => x1 :: x2) s []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
x : α
r : RBNode α
s : RBNode.Stream α
⊢ (cons x r s).toList = x :: r.toList ++ s.toList

Tactic:
rw [toList, toList, foldr, RBNode.foldr_cons]

Result:
α : Type u_1
x : α
r : RBNode α
s : RBNode.Stream α
⊢ x :: (r.toList ++ foldr (fun x1 x2 => x1 :: x2) s []) = x :: r.toList ++ foldr (fun x1 x2 => x1 :: x2) s []
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem IsOrtho.map_iff (f : E ≃ₗᵢ[𝕜] F) {U V : Submodule 𝕜 E} : U.map f ⟂ V.map f ↔ U ⟂ V :=
  ⟨fun h => by
    have hf : ∀ p : Submodule 𝕜 E, (p.map f).comap f.toLinearIsometry = p :=
      comap_map_eq_of_injective f.injective
    simpa only [hf] using h.comap f.toLinearIsometry, IsOrtho.map f.toLinearIsometry⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map f U ⟂ Submodule.map f V
⊢ U ⟂ V

Tactic:
have hf : ∀ p : Submodule 𝕜 E, (p.map f).comap f.toLinearIsometry = p :=
  comap_map_eq_of_injective f.injective

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map f U ⟂ Submodule.map f V
hf : ∀ (p : Submodule 𝕜 E), Submodule.comap f.toLinearIsometry (Submodule.map f p) = p
⊢ U ⟂ V

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map f U ⟂ Submodule.map f V
hf : ∀ (p : Submodule 𝕜 E), Submodule.comap f.toLinearIsometry (Submodule.map f p) = p
⊢ U ⟂ V

Tactic:
simpa only [hf] using h.comap f.toLinearIsometry

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem apply_apply_apply (f : Bool → Bool) (x : Bool) : f (f (f x)) = f x

Proof state:
f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x

Tactic:
cases x <;> cases h₁ : f true <;> cases h₂ : f false <;> simp only [h₁, h₂]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) : a ≡ b [ZMOD m / gcd m c] :=
  cancel_right_div_gcd hm <| by simpa [mul_comm] using h

Proof state:
m a b c : ℤ
hm : 0 < m
h : c * a ≡ c * b [ZMOD m]
⊢ a * c ≡ b * c [ZMOD m]

Tactic:
simpa [mul_comm] using h

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean
@[reassoc, to_app]
lemma mapComp_assoc_right {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
    F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) =
      (α_ (F.map f) (F.map g) (F.map h)).inv ≫ F.mapComp f g ▷ F.map h ≫
        F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : LaxFunctor B C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) =
    (α_ (F.map f) (F.map g) (F.map h)).inv ≫ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom

Tactic:
simp only [map₂_associator, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isSuccPrelimit_toDual_iff : IsSuccPrelimit (toDual a) ↔ IsPredPrelimit a

Proof state:
α : Type u_1
a : α
inst✝ : LT α
⊢ IsSuccPrelimit (toDual a) ↔ IsPredPrelimit a

Tactic:
simp [IsSuccPrelimit, IsPredPrelimit]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the arithmetic function `ζ` equals the Riemann Zeta Function on its
domain of convergence `1 < re s`. -/
lemma LSeries_zeta_eq_riemannZeta {s : ℂ} (hs : 1 < s.re) : L ↗ζ s = riemannZeta s

Proof state:
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ↑(ζ n)) s = riemannZeta s

Tactic:
suffices ∑' n, term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' n : ℕ, 1 / (n : ℂ) ^ s by
  simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]

Result:
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), term (fun n => if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s

Proof state:
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ term (fun n => if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

Tactic:
rcases eq_or_ne n 0 with hn | hn <;>
simp [hn, ne_zero_of_one_lt_re hs]

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), term (fun n => if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
refine tsum_congr fun n ↦ ?_

Result:
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ term (fun n => if n = 0 then 0 else 1) s n = 1 / ↑n ^ s

Proof state:
s : ℂ
hs : 1 < s.re
this : ∑' (n : ℕ), term (fun n => if n = 0 then 0 else 1) s n = ∑' (n : ℕ), 1 / ↑n ^ s
⊢ L (fun n => ↑(ζ n)) s = riemannZeta s

Tactic:
simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem v_sq_scalar (m : M) : v Q m * v Q m = algebraMap _ _ (Q m) :=
  (ι_sq_scalar _ _).trans <| by simp

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
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) ((Q' Q) ((LinearMap.inl R M R) m)) =
    (algebraMap R (CliffordAlgebra (Q' Q))) (Q m)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isBigO_exp_comp_one {f : α → ℝ} :
    (fun x => exp (f x)) =O[l] (fun _ => 1 : α → ℝ) ↔ IsBoundedUnder (· ≤ ·) l f

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ ((fun x => rexp (f x)) =O[l] fun x => 1) ↔ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f

Tactic:
simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean
lemma injective_eq_monomorphisms [(forget C).PreservesMonomorphisms] :
    MorphismProperty.injective C = monomorphisms C

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget C).PreservesMonomorphisms

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesMonomorphisms
⊢ MorphismProperty.injective C = monomorphisms C

Tactic:
rw [injective_eq_monomorphisms_iff]

Result:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesMonomorphisms
⊢ (forget C).PreservesMonomorphisms
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem balance2_eq {l : RBNode α} {v : α} {r : RBNode α}
    (hr : r.Balanced c n) : balance2 l v r = node black l v r :=
  (reverse_reverse _).symm.trans <| by simp [balance1_eq hr.reverse]

Proof state:
α : Type u_1
c : RBColor
n : Nat
l : RBNode α
v : α
r : RBNode α
hr : r.Balanced c n
⊢ (l.balance2 v r).reverse.reverse = node black l v r

Tactic:
simp [balance1_eq hr.reverse]

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@[simp]
lemma right_top_iff :
    p.IsPerfectCompl U ⊤ ↔ U = ⊤

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
U : Submodule R M
⊢ p.IsPerfectCompl U ⊤ ↔ U = ⊤

Tactic:
rw [← IsPerfectCompl.flip_iff]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
U : Submodule R M
⊢ p.flip.IsPerfectCompl ⊤ U ↔ U = ⊤

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
U : Submodule R M
⊢ p.flip.IsPerfectCompl ⊤ U ↔ U = ⊤

Tactic:
exact left_top_iff

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem le_self_mul_self {I : FractionalIdeal S P} (hI : 1 ≤ I) : I ≤ I * I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
hI : 1 ≤ I
⊢ I ≤ I * I

Tactic:
convert mul_left_mono I hI

Result:
case h.e'_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
hI : 1 ≤ I
⊢ I = (fun x => I * x) 1

Proof state:
case h.e'_3
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
hI : 1 ≤ I
⊢ I = (fun x => I * x) 1

Tactic:
exact (mul_one I).symm

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem get_cyclicPermutations (l : List α) (n : Fin (length (cyclicPermutations l))) :
    (cyclicPermutations l).get n = l.rotate n

Proof state:
α : Type u
l : List α
n : Fin l.cyclicPermutations.length
⊢ l.cyclicPermutations.get n = l.rotate ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem ground_not_isBase (M : Matroid α) [h : RankPos M✶] : ¬M.IsBase M.E

Proof state:
α : Type u_1
M : Matroid α
h : M✶.RankPos
⊢ ¬M.IsBase M.E

Tactic:
rwa [rankPos_iff, dual_isBase_iff, diff_empty] at h

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.isInducing {f : α → β} (h : IsUniformInducing f) : IsInducing f

Proof state:
α : Type u
β : Type v
inst✝ : UniformSpace β
f : α → β
h : IsUniformInducing f
⊢ IsInducing f

Tactic:
exact .induced f

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : IsUniformInducing f
⊢ IsInducing f

Tactic:
obtain rfl := h.comap_uniformSpace

Result:
α : Type u
β : Type v
inst✝ : UniformSpace β
f : α → β
h : IsUniformInducing f
⊢ IsInducing f
-- Mathlib/Data/Finmap.lean
theorem ext : ∀ {s t : Finmap β}, s.entries = t.entries → s = t
  | ⟨l₁, h₁⟩, ⟨l₂, _⟩, H => by congr

Proof state:
α : Type u
β : α → Type v
l₁ : Multiset (Sigma β)
h₁ : l₁.NodupKeys
l₂ : Multiset (Sigma β)
nodupKeys✝ : l₂.NodupKeys
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Complex.logDeriv_sin : logDeriv (Complex.sin) = Complex.cot

Proof state:
case h
x✝ : ℂ
⊢ logDeriv sin x✝ = x✝.cot

Tactic:
rw [logDeriv, Complex.deriv_sin, Pi.div_apply, Complex.cot]

Result:
no goals

Proof state:
⊢ logDeriv sin = cot

Tactic:
ext

Result:
case h
x✝ : ℂ
⊢ logDeriv sin x✝ = x✝.cot
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mul_left_mono (I : FractionalIdeal S P) : Monotone (I * ·)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ (fun x => I * x) J ≤ (fun x => I * x) J'

Tactic:
simp only [mul_def]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ ⟨↑I * ↑J, ⋯⟩ ≤ ⟨↑I * ↑J', ⋯⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ Monotone fun x => I * x

Tactic:
intro J J' h

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ (fun x => I * x) J ≤ (fun x => I * x) J'

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J J' : FractionalIdeal S P
h : J ≤ J'
⊢ ⟨↑I * ↑J, ⋯⟩ ≤ ⟨↑I * ↑J', ⋯⟩

Tactic:
exact mul_le.mpr fun x hx y hy => mul_mem_mul hx (h hy)

Result:
no goals
-- Mathlib/RingTheory/Invariant.lean
theorem isIntegral [Finite G] : Algebra.IsIntegral A B

Proof state:
case intro
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
val✝ : Fintype G
⊢ Algebra.IsIntegral A B

Tactic:
refine ⟨fun b ↦ ?_⟩

Result:
case intro
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
val✝ : Fintype G
b : B
⊢ IsIntegral A b

Proof state:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
⊢ Algebra.IsIntegral A B

Tactic:
cases nonempty_fintype G

Result:
case intro
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
val✝ : Fintype G
⊢ Algebra.IsIntegral A B

Proof state:
case intro
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
val✝ : Fintype G
b : B
⊢ IsIntegral A b

Tactic:
obtain ⟨p, hp1, -, hp2⟩ := Polynomial.lifts_and_natDegree_eq_and_monic
  (charpoly_mem_lifts A B G b) (monic_charpoly G b)

Result:
case intro.intro.intro.intro
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
val✝ : Fintype G
b : B
p : A[X]
hp1 : map (algebraMap A B) p = charpoly G b
hp2 : p.Monic
⊢ IsIntegral A b

Proof state:
case intro.intro.intro.intro
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
val✝ : Fintype G
b : B
p : A[X]
hp1 : map (algebraMap A B) p = charpoly G b
hp2 : p.Monic
⊢ IsIntegral A b

Tactic:
exact ⟨p, hp2, by rw [← eval_map, hp1, eval_charpoly]⟩

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Group G
inst✝² : MulSemiringAction G B
inst✝¹ : IsInvariant A B G
inst✝ : Finite G
val✝ : Fintype G
b : B
p : A[X]
hp1 : map (algebraMap A B) p = charpoly G b
hp2 : p.Monic
⊢ eval₂ (algebraMap A B) b p = 0

Tactic:
rw [← eval_map, hp1, eval_charpoly]

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
theorem min_div_div_right' (a b c : α) : min (a / c) (b / c) = min a b / c

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b c : α
⊢ a / c ⊓ b / c = (a ⊓ b) / c

Tactic:
simpa only [div_eq_mul_inv] using min_mul_mul_right a b c⁻¹

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
theorem mulShift_mul (ψ : AddChar R M) (r s : R) :
    mulShift ψ r * mulShift ψ s = mulShift ψ (r + s)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ (r * x✝) * ψ (s * x✝)

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s : R
⊢ ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = (ψ.mulShift (r + s)) x✝

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = (ψ.mulShift (r + s)) x✝

Tactic:
rw [mulShift_apply, right_distrib, map_add_eq_mul]

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ (ψ.mulShift r * ψ.mulShift s) x✝ = ψ (r * x✝) * ψ (s * x✝)
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem _root_.schwartz_withSeminorms : WithSeminorms (schwartzSeminormFamily 𝕜 E F)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
A : nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0)
⊢ ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0) =
    ⨅ i, Filter.comap (⇑(schwartzSeminormFamily 𝕜 E F i)) (nhds 0)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
A : WithSeminorms (schwartzSeminormFamily ℝ E F)
⊢ WithSeminorms (schwartzSeminormFamily 𝕜 E F)

Tactic:
rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf] at A ⊢

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
A : nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0)
⊢ nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily 𝕜 E F i)) (nhds 0)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
A : nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0)
⊢ nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily 𝕜 E F i)) (nhds 0)

Tactic:
rw [A]

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
A : nhds 0 = ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0)
⊢ ⨅ i, Filter.comap (⇑(schwartzSeminormFamily ℝ E F i)) (nhds 0) =
    ⨅ i, Filter.comap (⇑(schwartzSeminormFamily 𝕜 E F i)) (nhds 0)

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
⊢ WithSeminorms (schwartzSeminormFamily 𝕜 E F)

Tactic:
have A : WithSeminorms (schwartzSeminormFamily ℝ E F) := ⟨rfl⟩

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
A : WithSeminorms (schwartzSeminormFamily ℝ E F)
⊢ WithSeminorms (schwartzSeminormFamily 𝕜 E F)
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp] lemma map_snd_prod : Measure.map Prod.snd (μ.prod ν) = (μ univ) • ν

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
⊢ map Prod.snd (μ.prod ν) = μ univ • ν

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set β
hs : MeasurableSet s
⊢ (map Prod.snd (μ.prod ν)) s = (μ univ • ν) s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set β
hs : MeasurableSet s
⊢ (map Prod.snd (μ.prod ν)) s = (μ univ • ν) s

Tactic:
simp [Measure.map_apply measurable_snd hs, ← univ_prod]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem support_onFinset [DecidableEq M] {s : Finset α} {f : α → M}
    (hf : ∀ a : α, f a ≠ 0 → a ∈ s) :
    (Finsupp.onFinset s f hf).support = {a ∈ s | f a ≠ 0}

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ filter (fun a => ¬f a = 0) s = filter (fun a => ¬f a = 0) s

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (onFinset s f hf).support = filter (fun a => f a ≠ 0) s

Tactic:
dsimp [onFinset]

Result:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ filter (fun a => ¬f a = 0) s = filter (fun a => ¬f a = 0) s
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma lt_smul_of_one_lt_left [SMulPosStrictMono α β] (hb : 0 < b) (h : 1 < a) : b < a • b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Monoid α
inst✝⁴ : Zero β
inst✝³ : MulAction α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosStrictMono α β
hb : 0 < b
h : 1 < a
⊢ b < a • b

Tactic:
simpa only [one_smul] using smul_lt_smul_of_pos_right h hb

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma quasispectrum_le (a : A) ⦃x : ℝ≥0⦄ (hx : x ∈ σₙ ℝ≥0 a) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalNormedRing A
inst✝⁷ : StarRing A
inst✝⁶ : NormedSpace ℝ A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
x : ℝ≥0
hx : x ∈ σₙ ℝ≥0 a
ha : autoParam (0 ≤ a) _auto✝
⊢ x ≤ ‖a‖₊

Tactic:
simpa [cfcₙ_id ℝ≥0 a] using apply_le_nnnorm_cfcₙ_nnreal id a hx

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_r_lt_n : ∀ᶠ (n : ℕ) in atTop, ∀ i, r i n < n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), r i n < n

Tactic:
filter_upwards [eventually_ge_atTop R.n₀] with n hn

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : R.n₀ ≤ n
⊢ ∀ (i : α), r i n < n

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
n : ℕ
hn : R.n₀ ≤ n
⊢ ∀ (i : α), r i n < n

Tactic:
exact fun i => R.r_lt_n i n hn

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr_mapAccumr₂ (f₁ : γ → σ₁ → σ₁ × ζ) (f₂ : α → β → σ₂ → σ₂ × γ) :
    (mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).snd s₁)
    = let m := mapAccumr₂ (fun x y s =>
          let r₂ := f₂ x y s.snd
          let r₁ := f₁ r₂.snd s.fst
          ((r₁.fst, r₂.fst), r₁.snd)
        ) xs ys (s₁, s₂)
      (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ζ : Type u_4
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : γ → σ₁ → σ₁ × ζ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y s =>
          let r₂ := f₂ x y s.2;
          let r₁ := f₁ r₂.2 s.1;
          ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem isThreeCycle_isConj (h5 : 5 ≤ Fintype.card α) {σ τ : alternatingGroup α}
    (hσ : IsThreeCycle (σ : Perm α)) (hτ : IsThreeCycle (τ : Perm α)) : IsConj σ τ :=
  alternatingGroup.isConj_of (isConj_iff_cycleType_eq.2 (hσ.trans hτ.symm))
    (by rwa [hσ.card_support])

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ card α
σ τ : ↥(alternatingGroup α)
hσ : (↑σ).IsThreeCycle
hτ : (↑τ).IsThreeCycle
⊢ (↑σ).support.card + 2 ≤ card α

Tactic:
rwa [hσ.card_support]

Result:
no goals