harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
/-- The `vectorSpan` of a finite affinely independent family has dimension one less than its
cardinality. -/
lemma AffineIndependent.finrank_vectorSpan_add_one [Fintype ι] [Nonempty ι] {p : ι → P}
    (hi : AffineIndependent k p) : finrank k (vectorSpan k (Set.range p)) + 1 = Fintype.card ι

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ι → P
hi : AffineIndependent k p
⊢ finrank k ↥(vectorSpan k (Set.range p)) + 1 = Fintype.card ι

Tactic:
rw [hi.finrank_vectorSpan (tsub_add_cancel_of_le _).symm, tsub_add_cancel_of_le] <;>
  exact Fintype.card_pos

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem sum_mulShift {R : Type*} [CommRing R] [Fintype R] [DecidableEq R]
    {R' : Type*} [CommRing R'] [IsDomain R'] {ψ : AddChar R R'} (b : R)
    (hψ : IsPrimitive ψ) : ∑ x : R, ψ (x * b) = if b = 0 then Fintype.card R else 0

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : b = 0
⊢ ∑ x : R, ψ (x * b) = ↑(Fintype.card R)

Tactic:
simp only [h, mul_zero, map_zero_eq_one, Finset.sum_const, Nat.smul_one_eq_cast]

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : b = 0
⊢ ↑Finset.univ.card = ↑(Fintype.card R)

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x : R, ψ (b * x) = ↑0

Tactic:
exact mod_cast sum_eq_zero_of_ne_one (hψ h)

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x : R, ψ (x * b) = ↑0

Tactic:
simp_rw [mul_comm]

Result:
case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x : R, ψ (b * x) = ↑0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
⊢ ∑ x : R, ψ (x * b) = ↑(if b = 0 then Fintype.card R else 0)

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : b = 0
⊢ ∑ x : R, ψ (x * b) = ↑(Fintype.card R)

case neg
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : ¬b = 0
⊢ ∑ x : R, ψ (x * b) = ↑0

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Fintype R
inst✝² : DecidableEq R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
b : R
hψ : ψ.IsPrimitive
h : b = 0
⊢ ↑Finset.univ.card = ↑(Fintype.card R)

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiff_iff_target :
    ContMDiff I I' n f ↔
      Continuous f ∧ ∀ y : M',
        ContMDiffOn I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) (f ⁻¹' (extChartAt I' y).source)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ ContMDiff I I' n f ↔
    Continuous f ∧ ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)

Tactic:
rw [← contMDiffOn_univ, contMDiffOn_iff_target]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ (ContinuousOn f univ ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (univ ∩ f ⁻¹' (extChartAt I' y).source)) ↔
    Continuous f ∧ ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝¹ : IsManifold I n M
inst✝ : IsManifold I' n M'
⊢ (ContinuousOn f univ ∧
      ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (univ ∩ f ⁻¹' (extChartAt I' y).source)) ↔
    Continuous f ∧ ∀ (y : M'), ContMDiffOn I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) (f ⁻¹' (extChartAt I' y).source)

Tactic:
simp [continuous_iff_continuousOn_univ]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
lemma norm_pi_le_of_le {ι : Type*} [Fintype ι]
    {M : ι → Type*} [∀ i, SeminormedAddCommGroup (M i)] [∀ i, NormedSpace 𝕜 (M i)] {C : ℝ}
    {L : (i : ι) → (E →L[𝕜] M i)} (hL : ∀ i, ‖L i‖ ≤ C) (hC : 0 ≤ C) :
    ‖pi L‖ ≤ C

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
⊢ 0 ≤ C * ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
i : ι
⊢ ‖(pi L) x i‖ ≤ C * ‖x‖

Tactic:
exact (L i).le_of_opNorm_le (hL i) _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
⊢ ‖pi L‖ ≤ C

Tactic:
refine opNorm_le_bound _ hC (fun x ↦ ?_)

Result:
𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
⊢ ‖(pi L) x‖ ≤ C * ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
⊢ ‖(pi L) x‖ ≤ C * ‖x‖

Tactic:
refine (pi_norm_le_iff_of_nonneg (by positivity)).mpr (fun i ↦ ?_)

Result:
𝕜 : Type u_1
E : Type u_4
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
M : ι → Type u_10
inst✝¹ : (i : ι) → SeminormedAddCommGroup (M i)
inst✝ : (i : ι) → NormedSpace 𝕜 (M i)
C : ℝ
L : (i : ι) → E →L[𝕜] M i
hL : ∀ (i : ι), ‖L i‖ ≤ C
hC : 0 ≤ C
x : E
i : ι
⊢ ‖(pi L) x i‖ ≤ C * ‖x‖
-- Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean
theorem projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj (P : C) :
    Projective P ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
intro

Result:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
a✝ : (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms

Proof state:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGrp).PreservesEpimorphisms
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P))
    (forget _)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (coyoneda.obj (op P)).PreservesEpimorphisms ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
refine ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
    forget AddCommGrp).PreservesEpimorphisms => ?_, ?_⟩

Result:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
h : (preadditiveCoyoneda.obj (op P) ⋙ forget AddCommGrp).PreservesEpimorphisms
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms → (coyoneda.obj (op P)).PreservesEpimorphisms
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_pow : ∀ (n : ℕ), (p^n).smeval x = (p.smeval x)^n
  | 0 => by
    simp only [npow_zero, smeval_one, one_smul]
  | n + 1 => by
    rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, npow_one]

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
⊢ (p ^ (n + 1)).smeval x = p.smeval x ^ (n + 1)

Tactic:
rw [npow_add, smeval_mul, smeval_pow n, pow_one, npow_add, npow_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
p : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
⊢ (p ^ 0).smeval x = p.smeval x ^ 0

Tactic:
simp only [npow_zero, smeval_one, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_map (f : α → β) (a : Array α) (i : Nat) (hi : i < (a.map f).size) :
    (a.map f)[i] = f (a[i]'(by simpa using hi))

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : Array α
i : Nat
hi : i < (map f a).size
⊢ (map f a)[i] = f a[i]

Tactic:
cases a

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
i : Nat
toList✝ : List α
hi : i < (map f { toList := toList✝ }).size
⊢ (map f { toList := toList✝ })[i] = f { toList := toList✝ }[i]

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
i : Nat
toList✝ : List α
hi : i < (map f { toList := toList✝ }).size
⊢ (map f { toList := toList✝ })[i] = f { toList := toList✝ }[i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.156330
β : Type ?u.156336
f : α → β
a : Array α
i : Nat
hi : i < (map f a).size
⊢ i < a.size

Tactic:
simpa using hi

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasFDerivWithinAt.abs_of_neg (hf : HasFDerivWithinAt f f' s x)
    (h₀ : f x < 0) : HasFDerivWithinAt (fun x ↦ |f x|) (-f') s x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
⊢ HasFDerivWithinAt (fun x => |f x|) (-f') s x

Tactic:
convert (hasDerivAt_abs_neg h₀).comp_hasFDerivWithinAt x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
⊢ -f' = -1 • f'

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
⊢ -f' = -1 • f'

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeries.term_sum : term (∑ i ∈ S, f i) s  = ∑ i ∈ S, term (f i) s :=
  funext fun _ ↦ by simp

Proof state:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
x✝ : ℕ
⊢ term (∑ i ∈ S, f i) s x✝ = (∑ i ∈ S, term (f i) s) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_fintypeIoo : Fintype.card (Set.Ioo a b) = b - a - 1

Proof state:
a b : ℕ
⊢ Fintype.card ↑(Set.Ioo a b) = b - a - 1

Tactic:
rw [Fintype.card_ofFinset, card_Ioo]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertManyIfNewUnit_empty_list_le [EquivBEq α] [LawfulHashable α]
    {l : List α} :
    (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1.1.size ≤ l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ (insertManyIfNewUnit empty l).val.val.size ≤ l.length

Tactic:
apply Nat.le_trans (size_insertManyIfNewUnit_list_le _ Raw.WF.empty₀)

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ empty.val.size + l.length ≤ l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ empty.val.size + l.length ≤ l.length

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem unitors_equal : (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom

Tactic:
rw [← whiskerLeft_iff, ← cancel_epi (α_ _ _ _).hom, ← cancel_mono (ρ_ _).hom, triangle, ←
    rightUnitor_comp, rightUnitor_naturality]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ`. -/
lemma sum_mul_le_sqrt_mul_sqrt (s : Finset ι) (f g : ι → ℝ) :
    ∑ i ∈ s, f i * g i ≤ √(∑ i ∈ s, f i ^ 2) * √(∑ i ∈ s, g i ^ 2) :=
  (le_sqrt_of_sq_le <| sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq <| sqrt_mul
    (sum_nonneg fun _ _ ↦ by positivity) _

Proof state:
ι : Type u_2
s : Finset ι
f g : ι → ℝ
x✝¹ : ι
x✝ : x✝¹ ∈ s
⊢ 0 ≤ f x✝¹ ^ 2

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem realPart_apply_coe (a : A) : (ℜ a : A) = (2 : ℝ)⁻¹ • (a + star a)

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑((selfAdjointPart ℝ) a) = 2⁻¹ • (a + star a)

Tactic:
simp only [selfAdjointPart_apply_coe, invOf_eq_inv]

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℜ a) = 2⁻¹ • (a + star a)

Tactic:
unfold realPart

Result:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑((selfAdjointPart ℝ) a) = 2⁻¹ • (a + star a)
-- Mathlib/Data/Nat/Sqrt.lean
lemma exists_mul_self' (x : ℕ) : (∃ n, n ^ 2 = x) ↔ sqrt x ^ 2 = x

Proof state:
x : ℕ
⊢ (∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x

Tactic:
simpa only [Nat.pow_two] using exists_mul_self x

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem cthickening_cthickening (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (s : Set E) :
    cthickening ε (cthickening δ s) = cthickening (ε + δ) s :=
  (cthickening_cthickening_subset hε hδ _).antisymm fun x => by
    simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ, infEdist_cthickening]
    exact tsub_le_iff_right.2

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ s)

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ, infEdist_cthickening]

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEdist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEdist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
exact tsub_le_iff_right.2

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_eq_max' {a b : Cardinal} (h : ℵ₀ ≤ a * b) : a * b = max a b

Proof state:
case intro.intro.inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = a ⊔ b

Tactic:
exact mul_eq_max_of_aleph0_le_left ha' hb

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
⊢ a * b = a ⊔ b

Tactic:
rcases aleph0_le_mul_iff.mp h with ⟨ha, hb, ha' | hb'⟩

Result:
case intro.intro.inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = a ⊔ b

case intro.intro.inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = a ⊔ b

Proof state:
case intro.intro.inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = a ⊔ b

Tactic:
exact mul_eq_max_of_aleph0_le_right ha hb'

Result:
no goals
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem wittPolyProd_vars (n : ℕ) : (wittPolyProd p n).vars ⊆ univ ×ˢ range (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
apply Subset.trans (vars_mul _ _)

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 0)) (wittPolynomial p ℤ n)).vars ∪ ((rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆
    univ ×ˢ range (n + 1)

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ image (Prod.mk 1) (wittPolynomial p ℤ n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
simp [wittPolynomial_vars, image_subset_iff]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (wittPolyProd p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rw [wittPolyProd]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 0)) (wittPolynomial p ℤ n) * (rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆
    univ ×ˢ range (n + 1)

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
refine Subset.trans (vars_rename _ _) ?_

Result:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ image (Prod.mk 1) (wittPolynomial p ℤ n).vars ⊆ univ ×ˢ range (n + 1)
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_zero : integral (0 : α →₁[μ] E) = 0

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ integral 0 = 0

Tactic:
simp only [integral]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ integralCLM 0 = 0

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ integralCLM 0 = 0

Tactic:
exact map_zero integralCLM

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem le_val_last (i : Fin (n + 1)) : i ≤ n

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ last n

Tactic:
exact Fin.le_last i

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ ↑n

Tactic:
rw [Fin.natCast_eq_last]

Result:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ last n
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma r_lower_bound_on_verticalStrip {A B : ℝ} (h : 0 < B) (hz : z ∈ verticalStrip A B) :
    r ⟨⟨A, B⟩, h⟩ ≤ r z

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 < z.re ^ 2 / z.im ^ 2 + 1

Tactic:
positivity

Result:
no goals

Proof state:
case hac.hab
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ≤ UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩

case hdb.hab
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ≤ z.im

Tactic:
exacts [hz.1, hz.2]

Result:
no goals

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ (UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2 / UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ^ 2 + 1)⁻¹ ≤
    (z.re ^ 2 / z.im ^ 2 + 1)⁻¹

Tactic:
rw [inv_le_inv₀ (by positivity) (by positivity), add_le_add_iff_right, ← even_two.pow_abs]

Result:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ^ 2 / z.im ^ 2 ≤
    UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2 / UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ^ 2

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 ≤ r1 z

Tactic:
apply (r1_pos z).le

Result:
no goals

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r1 ⟨{ re := A, im := B }, h⟩ ≤ r1 z

Tactic:
simp only [r1_eq, div_pow, one_div]

Result:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ (UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2 / UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ^ 2 + 1)⁻¹ ≤
    (z.re ^ 2 / z.im ^ 2 + 1)⁻¹

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ^ 2 / z.im ^ 2 ≤
    UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2 / UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ^ 2

Tactic:
gcongr

Result:
case hac.hab
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ≤ UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩

case hdb.hab
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ≤ z.im

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 < UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2 / UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ^ 2 + 1

Tactic:
positivity

Result:
no goals

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ √(r1 ⟨{ re := A, im := B }, h⟩) ≤ √(r1 z)

Tactic:
rw [Real.sqrt_le_sqrt_iff (by apply (r1_pos z).le)]

Result:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r1 ⟨{ re := A, im := B }, h⟩ ≤ r1 z

Proof state:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r ⟨{ re := A, im := B }, h⟩ ≤ r z

Tactic:
apply min_le_min hz.2

Result:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ √(r1 ⟨{ re := A, im := B }, h⟩) ≤ √(r1 z)