harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_one_one_eq_chebyshev_C : ∀ n, dickson 1 (1 : R) n = Chebyshev.C R n
  | 0 => by
    simp only [Chebyshev.C_zero, mul_one, one_comp, dickson_zero]
    norm_num
  | 1 => by
    rw [dickson_one, Nat.cast_one, Chebyshev.C_one]
  | n + 2 => by
    rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.C_add_two,
      dickson_one_one_eq_chebyshev_C (n + 1), dickson_one_one_eq_chebyshev_C n]
    push_cast
    ring

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.C R (↑n + 1) - 1 * Chebyshev.C R ↑n = X * Chebyshev.C R (↑n + 1) - Chebyshev.C R ↑n

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑1 = Chebyshev.C R ↑0

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.C R ↑(n + 1) - 1 * Chebyshev.C R ↑n = X * Chebyshev.C R (↑n + 1) - Chebyshev.C R ↑n

Tactic:
push_cast

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.C R (↑n + 1) - 1 * Chebyshev.C R ↑n = X * Chebyshev.C R (↑n + 1) - Chebyshev.C R ↑n

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ dickson 1 1 0 = Chebyshev.C R ↑0

Tactic:
simp only [Chebyshev.C_zero, mul_one, one_comp, dickson_zero]

Result:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑1 = Chebyshev.C R ↑0

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ dickson 1 1 1 = Chebyshev.C R ↑1

Tactic:
rw [dickson_one, Nat.cast_one, Chebyshev.C_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ dickson 1 1 (n + 2) = Chebyshev.C R ↑(n + 2)

Tactic:
rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.C_add_two,
  dickson_one_one_eq_chebyshev_C (n + 1), dickson_one_one_eq_chebyshev_C n]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.C R ↑(n + 1) - 1 * Chebyshev.C R ↑n = X * Chebyshev.C R (↑n + 1) - Chebyshev.C R ↑n
-- Mathlib/Data/Rat/Floor.lean
theorem isInt_intCeil {R} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℤ) :
    IsInt r m → IsInt ⌈r⌉ m

Proof state:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌈↑m⌉ m

Tactic:
exact ⟨by simp⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ ⌈↑m⌉ = ↑m

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
m : ℤ
⊢ IsInt r m → IsInt ⌈r⌉ m

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌈↑m⌉ m
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_congr (h : f.support ⊆ g.support) (h' : ∀ x ∈ g.support, f x = g x) : f = g

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
⊢ f x = g x

Tactic:
by_cases hx : x ∈ g.support

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
hx : x ∈ g.support
⊢ f x = g x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
hx : x ∉ g.support
⊢ f x = g x

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
hx : x ∉ g.support
⊢ f x = g x

Tactic:
rw [not_mem_support.mp hx, ← not_mem_support]

Result:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
hx : x ∉ g.support
⊢ x ∉ f.support

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
hx : x ∉ g.support
⊢ x ∉ f.support

Tactic:
exact fun H => hx (h H)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
⊢ f = g

Tactic:
ext x

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
⊢ f x = g x

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, f x = g x
x : α
hx : x ∈ g.support
⊢ f x = g x

Tactic:
exact h' x hx

Result:
no goals
-- Mathlib/Topology/Algebra/Field.lean
theorem affineHomeomorph_image_Ioc {𝕜 : Type*} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜]
    [IsTopologicalRing 𝕜] (a b c d : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne' '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)

Proof state:
𝕜 : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b c d : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Set.Ioc c d = Set.Ioc (a * c + b) (a * d + b)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAtFilter.comp (hh₂ : HasDerivAtFilter h₂ h₂' (h x) L')
    (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
    HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'
hh : HasDerivAtFilter h h' x L
hL : Tendsto h L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h' * h₂') x L

Tactic:
exact hh₂.scomp x hh hL

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'
hh : HasDerivAtFilter h h' x L
hL : Tendsto h L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L

Tactic:
rw [mul_comm]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter 𝕜'
hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'
hh : HasDerivAtFilter h h' x L
hL : Tendsto h L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h' * h₂') x L
-- Mathlib/Logic/Basic.lean
theorem eq_iff_eq_cancel_left {b c : α} : (∀ {a}, a = b ↔ a = c) ↔ b = c :=
  ⟨fun h ↦ by rw [← h], fun h a ↦ by rw [h]⟩

Proof state:
α : Sort u_1
b c : α
h : ∀ {a : α}, a = b ↔ a = c
⊢ b = c

Tactic:
rw [← h]

Result:
no goals

Proof state:
α : Sort u_1
b c : α
h : b = c
a : α
⊢ a = b ↔ a = c

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_image_nhd_mem_nhds_of_mem_interior_range {x} (hx : x ∈ f.source)
    (h'x : f.extend I x ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 x) :
    (f.extend I) '' s ∈ 𝓝 ((f.extend I) x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) '' s ∈ 𝓝 (↑(f.extend I) x)

Tactic:
rw [← f.map_extend_nhds_of_mem_interior_range hx h'x, Filter.mem_map]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) ⁻¹' (↑(f.extend I) '' s) ∈ 𝓝 x

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) ⁻¹' (↑(f.extend I) '' s) ∈ 𝓝 x

Tactic:
filter_upwards [h] using subset_preimage_image (f.extend I) s

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set!_mk (a : Array α) (h : a.size = n) (i x) :
    (Vector.mk a h).set! i x = Vector.mk (a.set! i x) (by simp [h]) := rfl

Proof state:
α : Type ?u.14270
n : Nat
a : Array α
h : a.size = n
i : Nat
x : α
⊢ (a.set! i x).size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem eq_zero_of_measure_zero {β : Type*} [NormedAddCommGroup β] {T : Set α → β} {C : ℝ}
    (hT : DominatedFinMeasAdditive μ T C) {s : Set α} (hs : MeasurableSet s) (hs_zero : μ s = 0) :
    T s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ T s = 0

Tactic:
refine norm_eq_zero.mp ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ ‖T s‖ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ μ s < ⊤

Tactic:
simp [hs_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ ‖T s‖ = 0

Tactic:
refine ((hT.2 s hs (by simp [hs_zero])).trans (le_of_eq ?_)).antisymm (norm_nonneg _)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ C * (μ s).toReal = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : μ s = 0
⊢ C * (μ s).toReal = 0

Tactic:
rw [hs_zero, ENNReal.zero_toReal, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem eq_top_iff {S : NonUnitalSubalgebra R A} : S = ⊤ ↔ ∀ x : A, x ∈ S :=
  ⟨fun h x => by rw [h]; exact mem_top, fun h => by ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩⟩

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x

Result:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Proof state:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]

Result:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Tactic:
exact mem_top

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem pow_two : t ^ 2 = 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ t ^ 2 = 1

Tactic:
rcases ht with ⟨w, i, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ (w * cs.simple i * w⁻¹) ^ 2 = 1

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ (w * cs.simple i * w⁻¹) ^ 2 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem inv_def (a : Rat) : a.inv = a.den /. a.num

Proof state:
a : Rat
⊢ (if h : a.num < 0 then { num := -↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ }
    else if h : a.num > 0 then { num := ↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } else a) =
    ↑a.den /. a.num

Tactic:
split

Result:
case isTrue
a : Rat
h✝ : a.num < 0
⊢ { num := -↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } = ↑a.den /. a.num

case isFalse
a : Rat
h✝ : ¬a.num < 0
⊢ (if h : a.num > 0 then { num := ↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } else a) = ↑a.den /. a.num

Proof state:
case isFalse
a : Rat
h✝ : ¬a.num < 0
⊢ (if h : a.num > 0 then { num := ↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } else a) = ↑a.den /. a.num

Tactic:
split

Result:
case isFalse.isTrue
a : Rat
h✝¹ : ¬a.num < 0
h✝ : a.num > 0
⊢ { num := ↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } = ↑a.den /. a.num

case isFalse.isFalse
a : Rat
h✝¹ : ¬a.num < 0
h✝ : ¬a.num > 0
⊢ a = ↑a.den /. a.num

Proof state:
a : Rat
h✝ : ¬a.num < 0
h : a.num > 0
⊢ { num := ↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } = ↑a.den /. a.num

Tactic:
rw [mk_eq_divInt, Int.natAbs_of_nonneg (Int.le_of_lt h)]

Result:
no goals

Proof state:
a : Rat
h₁ : ¬a.num < 0
h₂ : ¬a.num > 0
⊢ a.num /. ↑a.den = ↑a.den /. a.num

Tactic:
simp [Int.le_antisymm (Int.not_lt.1 h₂) (Int.not_lt.1 h₁)]

Result:
no goals

Proof state:
a : Rat
h : a.num < 0
⊢ { num := -↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } = ↑a.den /. a.num

Tactic:
rw [mk_eq_divInt, ← Int.natAbs_neg,
Int.natAbs_of_nonneg (Int.le_of_lt <| Int.neg_pos_of_neg h), neg_divInt_neg]

Result:
no goals

Proof state:
case isFalse.isTrue
a : Rat
h✝¹ : ¬a.num < 0
h✝ : a.num > 0
⊢ { num := ↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } = ↑a.den /. a.num

Tactic:
next h => rw [mk_eq_divInt, Int.natAbs_of_nonneg (Int.le_of_lt h)]

Result:
no goals

Proof state:
case isTrue
a : Rat
h✝ : a.num < 0
⊢ { num := -↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } = ↑a.den /. a.num

Tactic:
next h => rw [mk_eq_divInt, ← Int.natAbs_neg,
  Int.natAbs_of_nonneg (Int.le_of_lt <| Int.neg_pos_of_neg h), neg_divInt_neg]

Result:
no goals

Proof state:
a : Rat
h₁ : ¬a.num < 0
h₂ : ¬a.num > 0
⊢ a = ↑a.den /. a.num

Tactic:
apply (divInt_self _).symm.trans

Result:
a : Rat
h₁ : ¬a.num < 0
h₂ : ¬a.num > 0
⊢ a.num /. ↑a.den = ↑a.den /. a.num

Proof state:
case isFalse.isFalse
a : Rat
h✝¹ : ¬a.num < 0
h✝ : ¬a.num > 0
⊢ a = ↑a.den /. a.num

Tactic:
next h₁ h₂ =>
apply (divInt_self _).symm.trans
simp [Int.le_antisymm (Int.not_lt.1 h₂) (Int.not_lt.1 h₁)]

Result:
no goals

Proof state:
a : Rat
⊢ a.inv = ↑a.den /. a.num

Tactic:
unfold Rat.inv

Result:
a : Rat
⊢ (if h : a.num < 0 then { num := -↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ }
    else if h : a.num > 0 then { num := ↑a.den, den := a.num.natAbs, den_nz := ⋯, reduced := ⋯ } else a) =
    ↑a.den /. a.num
-- Mathlib/Analysis/Analytic/Linear.lean
theorem hasFPowerSeriesOnBall_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
    HasFPowerSeriesOnBall (fun x : E × F => f x.1 x.2) (f.fpowerSeriesBilinear x) x ∞ :=
  { r_le

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ ⊤ ≤ (f.fpowerSeriesBilinear x).radius

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => (f.fpowerSeriesBilinear x (n + 3)) fun x => y✝)
    ((f x.1) x.2 + (f.deriv₂ (x.1, x.2)) (y✝.1, y✝.2) + (f y✝.1) y✝.2 -
      ((((∑ i ∈ Finset.range 0, (f.fpowerSeriesBilinear x i) fun x => y✝) + (f.fpowerSeriesBilinear x 0) fun x => y✝) +
          (f.fpowerSeriesBilinear x 1) fun x => y✝) +
        (f.fpowerSeriesBilinear x 2) fun x => y✝))

Tactic:
simp [fpowerSeriesBilinear, hasSum_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => (f.fpowerSeriesBilinear x (n + 3)) fun x => y✝)
    ((f (x + y✝).1) (x + y✝).2 - ∑ i ∈ Finset.range 3, (f.fpowerSeriesBilinear x i) fun x => y✝)

Tactic:
simp only [Finset.sum_range_succ, Finset.sum_range_one, Prod.fst_add, Prod.snd_add,
  f.map_add_add]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y✝ : E × F
x✝ : y✝ ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => (f.fpowerSeriesBilinear x (n + 3)) fun x => y✝)
    ((f x.1) x.2 + (f.deriv₂ (x.1, x.2)) (y✝.1, y✝.2) + (f y✝.1) y✝.2 -
      ((((∑ i ∈ Finset.range 0, (f.fpowerSeriesBilinear x i) fun x => y✝) + (f.fpowerSeriesBilinear x 0) fun x => y✝) +
          (f.fpowerSeriesBilinear x 1) fun x => y✝) +
        (f.fpowerSeriesBilinear x 2) fun x => y✝))
-- Mathlib/RingTheory/Localization/NormTrace.lean
theorem Algebra.trace_localization [Module.Free R S] [Module.Finite R S] (a : S) :
    Algebra.trace Rₘ Sₘ (algebraMap S Sₘ a) = algebraMap R Rₘ (Algebra.trace R S a)

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ

Result:
case inl
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Subsingleton R
this : Subsingleton Rₘ
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Proof state:
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)

Tactic:
let b := Module.Free.chooseBasis R S

Result:
case inr
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
inst✝⁹ : CommRing Sₘ
inst✝⁸ : Algebra S Sₘ
M : Submonoid R
inst✝⁷ : IsLocalization M Rₘ
inst✝⁶ : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : Algebra R Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : Module.Free R S
inst✝ : Module.Finite R S
a : S
h✝ : Nontrivial R
b : Basis (Module.Free.ChooseBasisIndex R S) R S := Module.Free.chooseBasis R S
⊢ (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) a)
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma lintegral_nnnorm_le (f : X →ᵇ E) :
    ∫⁻ x, ‖f x‖₊ ∂μ ≤ ‖f‖₊ * (μ Set.univ)

Proof state:
case hfg.a
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
x✝ : X
⊢ ‖f x✝‖₊ ≤ ‖f‖₊

Tactic:
apply nnnorm_coe_le_nnnorm

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ↑‖f‖₊ * μ Set.univ

Tactic:
calc  ∫⁻ x, ‖f x‖₊ ∂μ
  _ ≤ ∫⁻ _, ‖f‖₊ ∂μ         := by gcongr; apply nnnorm_coe_le_nnnorm
  _ = ‖f‖₊ * (μ Set.univ)   := by rw [lintegral_const]

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f‖₊ ∂μ = ↑‖f‖₊ * μ Set.univ

Tactic:
rw [lintegral_const]

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ∫⁻ (x : X), ↑‖f‖₊ ∂μ

Tactic:
gcongr

Result:
case hfg.a
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
x✝ : X
⊢ ‖f x✝‖₊ ≤ ‖f‖₊
-- Mathlib/Topology/Algebra/Order/UpperLower.lean
theorem Set.OrdConnected.interior (h : s.OrdConnected) : (interior s).OrdConnected

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : s.OrdConnected
⊢ (interior ↑(upperClosure s) ∩ interior ↑(lowerClosure s)).OrdConnected

Tactic:
exact
  (upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : s.OrdConnected
⊢ (interior s).OrdConnected

Tactic:
rw [← h.upperClosure_inter_lowerClosure, interior_inter]

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : s.OrdConnected
⊢ (interior ↑(upperClosure s) ∩ interior ↑(lowerClosure s)).OrdConnected
-- Mathlib/Data/TypeVec.lean
theorem const_iff_true {α : TypeVec n} {i x p} : ofRepeat (TypeVec.const p α i x) ↔ p

Proof state:
case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec.{u_1} n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec.{u_1} (n✝ + 1)
x : α a✝.fs
⊢ ofRepeat (TypeVec.const p α a✝.fs x) ↔ p

Tactic:
erw [TypeVec.const, @ih (drop α) x]

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
p : Prop
⊢ ofRepeat (TypeVec.const p α i x) ↔ p

Tactic:
induction i with
| fz      => rfl
| fs _ ih => erw [TypeVec.const, @ih (drop α) x]

Result:
no goals

Proof state:
case fz
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p

Tactic:
rfl

Result:
no goals