harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_inj [NeZero n] : map (n := n) f = map g ↔ f = g

Proof state:
case mp.h
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
h : map f = map g
a : α✝¹
⊢ f a = g a

Tactic:
replace h := congrFun h (mkVector n a)

Result:
case mp.h
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
a : α✝¹
h : map f (mkVector n a) = map g (mkVector n a)
⊢ f a = g a

Proof state:
case mpr
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
h : f = g
⊢ map f = map g

Tactic:
subst h

Result:
case mpr
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
inst✝ : NeZero n
⊢ map f = map f

Proof state:
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
⊢ map f = map g ↔ f = g

Tactic:
constructor

Result:
case mp
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
⊢ map f = map g → f = g

case mpr
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
⊢ f = g → map f = map g

Proof state:
case mpr
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
⊢ f = g → map f = map g

Tactic:
intro h

Result:
case mpr
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
h : f = g
⊢ map f = map g

Proof state:
case mp
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
h : map f = map g
⊢ f = g

Tactic:
ext a

Result:
case mp.h
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
h : map f = map g
a : α✝¹
⊢ f a = g a

Proof state:
case mp
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
⊢ map f = map g → f = g

Tactic:
intro h

Result:
case mp
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
h : map f = map g
⊢ f = g

Proof state:
case mp.h
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
a : α✝¹
h : n ≠ 0 → f a = g a
⊢ f a = g a

Tactic:
exact h (NeZero.ne n)

Result:
no goals

Proof state:
case mpr
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
inst✝ : NeZero n
⊢ map f = map f

Tactic:
rfl

Result:
no goals

Proof state:
case mp.h
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
a : α✝¹
h : map f (mkVector n a) = map g (mkVector n a)
⊢ f a = g a

Tactic:
simp only [mkVector, map_mk, mk.injEq, Array.map_inj_left, Array.mem_mkArray,  and_imp,
  forall_eq_apply_imp_iff] at h

Result:
case mp.h
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
inst✝ : NeZero n
a : α✝¹
h : n ≠ 0 → f a = g a
⊢ f a = g a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_map (f : β → α) (l : List β) : find? p (l.map f) = (l.find? (p ∘ f)).map f

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ find? p (map f l) = Option.map f (find? (p ∘ f) l)

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp only [map_cons, find?]
  by_cases h : p (f x) <;> simp [h, ih]

Result:
no goals

Proof state:
case cons
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
x : β
xs : List β
ih : find? p (map f xs) = Option.map f (find? (p ∘ f) xs)
⊢ find? p (map f (x :: xs)) = Option.map f (find? (p ∘ f) (x :: xs))

Tactic:
simp only [map_cons, find?]

Result:
case cons
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
x : β
xs : List β
ih : find? p (map f xs) = Option.map f (find? (p ∘ f) xs)
⊢ (match p (f x) with
    | true => some (f x)
    | false => find? p (map f xs)) =
    Option.map f
      (match (p ∘ f) x with
      | true => some x
      | false => find? (p ∘ f) xs)

Proof state:
case cons
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
x : β
xs : List β
ih : find? p (map f xs) = Option.map f (find? (p ∘ f) xs)
⊢ (match p (f x) with
    | true => some (f x)
    | false => find? p (map f xs)) =
    Option.map f
      (match (p ∘ f) x with
      | true => some x
      | false => find? (p ∘ f) xs)

Tactic:
by_cases h : p (f x) <;> simp [h, ih]

Result:
no goals

Proof state:
case nil
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
⊢ find? p (map f []) = Option.map f (find? (p ∘ f) [])

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_append (l₁ : Vector α n) (l₂ : Vector α m) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
n m : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ countP p
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    countP p { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } +
      countP p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Bool
n m : Nat
l₂ : Vector α m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP p ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ } + countP p l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
p : α → Bool
n m : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = m
⊢ countP p
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    countP p { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } +
      countP p { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
α : Type u_1
p : α → Bool
n m : Nat
l₁ : Vector α n
l₂ : Vector α m
⊢ countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
p : α → Bool
n m : Nat
l₂ : Vector α m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP p ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ } + countP p l₂
-- Mathlib/Algebra/BigOperators/Ring/List.lean
lemma dvd_sum [NonUnitalSemiring R] {a} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum

Proof state:
case cons
R : Type u_5
inst✝ : NonUnitalSemiring R
a x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ (x :: l).sum

Tactic:
rw [List.sum_cons]

Result:
case cons
R : Type u_5
inst✝ : NonUnitalSemiring R
a x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ x + l.sum

Proof state:
case cons
R : Type u_5
inst✝ : NonUnitalSemiring R
a x : R
l : List R
ih : (∀ (x : R), x ∈ l → a ∣ x) → a ∣ l.sum
h : ∀ (x_1 : R), x_1 ∈ x :: l → a ∣ x_1
⊢ a ∣ x + l.sum

Tactic:
exact dvd_add (h _ (mem_cons_self _ _)) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

Result:
no goals

Proof state:
case nil
R : Type u_5
inst✝ : NonUnitalSemiring R
a : R
h : ∀ (x : R), x ∈ [] → a ∣ x
⊢ a ∣ [].sum

Tactic:
exact dvd_zero _

Result:
no goals

Proof state:
R : Type u_5
inst✝ : NonUnitalSemiring R
a : R
l : List R
h : ∀ (x : R), x ∈ l → a ∣ x
⊢ a ∣ l.sum

Tactic:
induction l with
| nil => exact dvd_zero _
| cons x l ih =>
  rw [List.sum_cons]
  exact dvd_add (h _ (mem_cons_self _ _)) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma sum_eq_zero_iff_ne_zero : ∑ x, ψ x = 0 ↔ ψ ≠ 0

Proof state:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ∑ x : A, ψ x = 0 ↔ ψ ≠ 0

Tactic:
classical
rw [sum_eq_ite, Ne.ite_eq_right_iff]; exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

Result:
no goals

Proof state:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ∑ x : A, ψ x = 0 ↔ ψ ≠ 0

Tactic:
rw [sum_eq_ite, Ne.ite_eq_right_iff]

Result:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ↑(card A) ≠ 0

Proof state:
A : Type u_1
R : Type u_2
inst✝⁴ : AddGroup A
inst✝³ : Fintype A
inst✝² : CommSemiring R
inst✝¹ : IsDomain R
ψ : AddChar A R
inst✝ : CharZero R
⊢ ↑(card A) ≠ 0

Tactic:
exact Nat.cast_ne_zero.2 Fintype.card_ne_zero

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem mem_selfAdjointMatricesSubmodule :
    A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁

Proof state:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁

Tactic:
erw [mem_pairSelfAdjointMatricesSubmodule]

Result:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ J.IsAdjointPair J A₁ A₁ ↔ J.IsSelfAdjoint A₁

Proof state:
R : Type u_1
n : Type u_11
inst✝² : CommRing R
inst✝¹ : Fintype n
J A₁ : Matrix n n R
inst✝ : DecidableEq n
⊢ J.IsAdjointPair J A₁ A₁ ↔ J.IsSelfAdjoint A₁

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem singleton_pi (i : ι) (t : ∀ i, Set (α i)) : pi {i} t = eval i ⁻¹' t i

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ {i}.pi t ↔ x✝ ∈ eval i ⁻¹' t i

Tactic:
simp [pi]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
i : ι
t : (i : ι) → Set (α i)
⊢ {i}.pi t = eval i ⁻¹' t i

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
i : ι
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ {i}.pi t ↔ x✝ ∈ eval i ⁻¹' t i
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem dist_div_sin_oangle_div_two_eq_radius {s : Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s)
    (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₁p₂ : p₁ ≠ p₂) (hp₁p₃ : p₁ ≠ p₃) (hp₂p₃ : p₂ ≠ p₃) :
    dist p₁ p₃ / |Real.Angle.sin (∡ p₁ p₂ p₃)| / 2 = s.radius

Proof state:
case h.e'_2.h.e'_5.h.e'_6
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₁ p₂ p₃).sin| = (∡ p₃ p₁ s.center).cos

Tactic:
rw [← Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi
  (two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi hp₁ hp₂ hp₃ hp₁p₂.symm hp₂p₃ hp₁p₃),
  abs_of_nonneg (Real.Angle.cos_nonneg_iff_abs_toReal_le_pi_div_two.2 _)]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₃ p₁ s.center).toReal| ≤ π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₃ p₁ s.center).toReal| ≤ π / 2

Tactic:
exact (abs_oangle_center_right_toReal_lt_pi_div_two hp₁ hp₃).le

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| / 2 = s.radius

Tactic:
convert dist_div_cos_oangle_center_div_two_eq_radius hp₁ hp₃ hp₁p₃

Result:
case h.e'_2.h.e'_5.h.e'_6
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁p₃ : p₁ ≠ p₃
hp₂p₃ : p₂ ≠ p₃
⊢ |(∡ p₁ p₂ p₃).sin| = (∡ p₃ p₁ s.center).cos
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) :
    a = b * c

Proof state:
a b c : Nat
H1 : b ∣ a
H2 : a / b = c
⊢ a = b * c

Tactic:
rw [← H2, Nat.mul_div_cancel' H1]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Finset.lean
protected lemma add_sup (hs : s.Nonempty) (f : ι → M) (a : M) :
    a + s.sup f = s.sup fun i ↦ a + f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝⁴ : LinearOrderedAddCommMonoid M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
hs : s.Nonempty
f : ι → M
a : M
⊢ a + s.sup f = s.sup fun i => a + f i

Tactic:
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']

Result:
no goals
-- Mathlib/AlgebraicGeometry/Limits.lean
@[simp]
lemma sigmaMk_mk (i) (x : f i) :
    sigmaMk f (.mk i x) = (Sigma.ι f i).base x

Proof state:
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ (ConcreteCategory.hom
        ((TopCat.sigmaCofan fun x => (f x).toTopCat).inj i ≫
          (colimit.isoColimitCocone
                { cocone := TopCat.sigmaCofan fun x => (f x).toTopCat,
                  isColimit := TopCat.sigmaCofanIsColimit fun x => (f x).toTopCat }).inv ≫
            (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map (Sigma.ι f i))) x

Tactic:
congr 2

Result:
case e_a.e_a
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ (TopCat.sigmaCofan fun x => (f x).toTopCat).inj i ≫
      (colimit.isoColimitCocone
            { cocone := TopCat.sigmaCofan fun x => (f x).toTopCat,
              isColimit := TopCat.sigmaCofanIsColimit fun x => (f x).toTopCat }).inv ≫
        (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)

Proof state:
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ (sigmaMk f) ⟨i, x⟩ = (ConcreteCategory.hom (Sigma.ι f i).base) x

Tactic:
show ((TopCat.sigmaCofan (fun x ↦ (f x).toTopCat)).inj i ≫
  (colimit.isoColimitCocone ⟨_, TopCat.sigmaCofanIsColimit _⟩).inv ≫ _) x =
    Scheme.forgetToTop.map (Sigma.ι f i) x

Result:
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ (ConcreteCategory.hom
        ((TopCat.sigmaCofan fun x => (f x).toTopCat).inj i ≫
          (colimit.isoColimitCocone
                { cocone := TopCat.sigmaCofan fun x => (f x).toTopCat,
                  isColimit := TopCat.sigmaCofanIsColimit fun x => (f x).toTopCat }).inv ≫
            (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom))
      x =
    (ConcreteCategory.hom (Scheme.forgetToTop.map (Sigma.ι f i))) x

Proof state:
case e_a.e_a
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ (TopCat.sigmaCofan fun x => (f x).toTopCat).inj i ≫
      (colimit.isoColimitCocone
            { cocone := TopCat.sigmaCofan fun x => (f x).toTopCat,
              isColimit := TopCat.sigmaCofanIsColimit fun x => (f x).toTopCat }).inv ≫
        (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.sigmaCofanIsColimit _⟩ _ _).trans ?_

Result:
case e_a.e_a
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ colimit.ι (Discrete.functor fun x => (f x).toTopCat) { as := i } ≫
      (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)

Proof state:
case e_a.e_a
ι : Type u
f : ι → Scheme
i : ι
x : ↑↑(f i).toPresheafedSpace
⊢ colimit.ι (Discrete.functor fun x => (f x).toTopCat) { as := i } ≫
      (PreservesCoproduct.iso Scheme.forgetToTop f).symm.hom =
    Scheme.forgetToTop.map (Sigma.ι f i)

Tactic:
exact ι_comp_sigmaComparison Scheme.forgetToTop _ _

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
theorem apply_apply_toDualRight_symm (x : M) (f : Dual R M) :
    (p x) (p.toDualRight.symm f) = f x

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
x : M
f : Dual R M
⊢ (p x) (p.toDualRight.symm f) = f x

Tactic:
have h := LinearEquiv.apply_symm_apply p.toDualRight f

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
x : M
f : Dual R M
h : p.toDualRight (p.toDualRight.symm f) = f
⊢ (p x) (p.toDualRight.symm f) = f x

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
x : M
f : Dual R M
h : p.toDualRight (p.toDualRight.symm f) = f
⊢ (p x) (p.toDualRight.symm f) = f x

Tactic:
rw [toDualRight_apply] at h

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
x : M
f : Dual R M
h : p.flip (p.toDualRight.symm f) = f
⊢ (p x) (p.toDualRight.symm f) = f x

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
x : M
f : Dual R M
h : p.flip (p.toDualRight.symm f) = f
⊢ (p x) (p.toDualRight.symm f) = f x

Tactic:
exact congrFun (congrArg DFunLike.coe h) x

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem dvd_to_int (m n : ZNum) : (m : ℤ) ∣ n ↔ m ∣ n :=
  ⟨fun ⟨k, e⟩ => ⟨k, by rw [← of_to_int n, e]; simp⟩, fun ⟨k, e⟩ => ⟨k, by simp [e]⟩⟩

Proof state:
m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ n = m * ↑k

Tactic:
rw [← of_to_int n, e]

Result:
m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k

Proof state:
m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k

Tactic:
simp

Result:
no goals

Proof state:
m n : ZNum
x✝ : m ∣ n
k : ZNum
e : n = m * k
⊢ ↑n = ↑m * ↑k

Tactic:
simp [e]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem add (hT : DominatedFinMeasAdditive μ T C) (hT' : DominatedFinMeasAdditive μ T' C') :
    DominatedFinMeasAdditive μ (T + T') (C + C')

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖T s + T' s‖ ≤ C * (μ s).toReal + C' * (μ s).toReal

Tactic:
exact (norm_add_le _ _).trans (add_le_add (hT.2 s hs hμs) (hT'.2 s hs hμs))

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖(T + T') s‖ ≤ (C + C') * (μ s).toReal

Tactic:
rw [Pi.add_apply, add_mul]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖T s + T' s‖ ≤ C * (μ s).toReal + C' * (μ s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
⊢ DominatedFinMeasAdditive μ (T + T') (C + C')

Tactic:
refine ⟨hT.1.add hT'.1, fun s hs hμs => ?_⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ‖(T + T') s‖ ≤ (C + C') * (μ s).toReal
-- Mathlib/Data/Real/Sqrt.lean
theorem sq_le (h : 0 ≤ y) : x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y

Proof state:
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y

Tactic:
constructor

Result:
case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -√y ≤ x ∧ x ≤ √y

case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y

Proof state:
case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -√y ≤ x ∧ x ≤ √y

Tactic:
simpa only [abs_le] using abs_le_sqrt

Result:
no goals

Proof state:
case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y

Tactic:
rw [← abs_le, ← sq_abs]

Result:
case mpr
x y : ℝ
h : 0 ≤ y
⊢ |x| ≤ √y → |x| ^ 2 ≤ y

Proof state:
case mpr
x y : ℝ
h : 0 ≤ y
⊢ |x| ≤ √y → |x| ^ 2 ≤ y

Tactic:
exact (le_sqrt (abs_nonneg x) h).mp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem pullbackFstιToV_fst (i j : 𝒰.J) :
    pullbackFstιToV 𝒰 f g i j ≫ pullback.fst _ _ = pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j : 𝒰.J
⊢ pullbackFstιToV 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j)

Tactic:
simp [pullbackFstιToV, p1]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := simp)] lemma mulEnergy_eq_zero_iff : Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅

Tactic:
simp [← (Nat.zero_le _).not_gt_iff_eq, not_and_or, imp_iff_or_not, or_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticOn.fderivWithin (h : AnalyticOn 𝕜 f s) (hu : UniqueDiffOn 𝕜 s) :
    AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ AnalyticWithinAt 𝕜 (fderivWithin 𝕜 f s) s x

Tactic:
rcases h x hx with ⟨p, r, hr⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticWithinAt 𝕜 (fderivWithin 𝕜 f s) s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (fderivWithin 𝕜 f s) s

Tactic:
intro x hx

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ AnalyticWithinAt 𝕜 (fderivWithin 𝕜 f s) s x

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticWithinAt 𝕜 (fderivWithin 𝕜 f s) s x

Tactic:
refine ⟨p.derivSeries, r, hr.fderivWithin_of_mem_of_analyticOn h hu hx⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Star.lean
theorem HasStrictDerivAt.star (h : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (fun x => star (f x)) (star f') x

Proof state:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
f' : F
x : 𝕜
h : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun x => star (f x)) (star f') x

Tactic:
simpa using h.star.hasStrictDerivAt

Result:
no goals