harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Image.lean
theorem image_preimage_eq_iff {f : α → β} {s : Set β} : f '' (f ⁻¹' s) = s ↔ s ⊆ range f :=
  ⟨by
    intro h
    rw [← h]
    apply image_subset_range,
   image_preimage_eq_of_subset⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ f '' (f ⁻¹' s) ⊆ range f

Tactic:
apply image_subset_range

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ s ⊆ range f

Tactic:
rw [← h]

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ f '' (f ⁻¹' s) ⊆ range f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s) = s → s ⊆ range f

Tactic:
intro h

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ s ⊆ range f
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin

Proof state:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ 2 • ⅟2 (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝

Tactic:
rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', LinearMap.one_apply,
  polar]

Result:
no goals

Proof state:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((2 • (associatedHom S) Q) x✝¹) x✝ = (Q.polarBilin x✝¹) x✝

Tactic:
dsimp

Result:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ 2 • ⅟2 (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
⊢ 2 • (associatedHom S) Q = Q.polarBilin

Tactic:
ext

Result:
case h.h
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((2 • (associatedHom S) Q) x✝¹) x✝ = (Q.polarBilin x✝¹) x✝
-- Mathlib/Data/Rat/Lemmas.lean
theorem num_mk (n d : ℤ) : (n /. d).num = d.sign * n / n.gcd d

Proof state:
n d : ℤ
this : ∀ (m : ℕ), (↑m + 1).natAbs = m + 1
⊢ (n /. d).num = d.sign * n / ↑(n.gcd d)

Tactic:
rcases d with ((_ | _) | _) <;>
rw [← Int.tdiv_eq_ediv_of_dvd] <;>
simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd,
  Int.zero_ediv, Int.ofNat_dvd_left, Nat.gcd_dvd_left, this]

Result:
no goals

Proof state:
n d : ℤ
⊢ (n /. d).num = d.sign * n / ↑(n.gcd d)

Tactic:
have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by
  rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]

Result:
n d : ℤ
this : ∀ (m : ℕ), (↑m + 1).natAbs = m + 1
⊢ (n /. d).num = d.sign * n / ↑(n.gcd d)

Proof state:
n d : ℤ
m : ℕ
⊢ (↑m + 1).natAbs = m + 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem insertRatUnits_postcondition {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n)
    (units : CNF.Clause (PosFin n)) :
    let assignments := (insertRatUnits f units).fst.assignments
    have hsize : assignments.size = n

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
hsize : f.assignments.size = n
h0 : InsertUnitInvariant f.assignments ⋯ f.ratUnits f.assignments hsize
⊢ InsertUnitInvariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯

Tactic:
exact insertUnitInvariant_insertUnit_fold f.assignments hf.2 f.ratUnits f.assignments hsize false units h0

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : CNF.Clause (PosFin n)
⊢ f.assignments.size = n

Tactic:
rw [hf.2]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preAleph_le_of_isLimit {o : Ordinal} (l : o.IsLimit) {c} :
    preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c :=
  ⟨fun h o' h' => (preAleph_le_preAleph.2 <| h'.le).trans h, fun h => by
    rw [← preAleph.apply_symm_apply c, preAleph_le_preAleph, limit_le l]
    intro x h'
    rw [← preAleph_le_preAleph, preAleph.apply_symm_apply]
    exact h _ h'⟩

Proof state:
o : Ordinal.{u_1}
l : o.IsLimit
c : Cardinal.{u_1}
h : ∀ o' < o, preAleph o' ≤ c
⊢ ∀ x < o, x ≤ preAleph.symm c

Tactic:
intro x h'

Result:
o : Ordinal.{u_1}
l : o.IsLimit
c : Cardinal.{u_1}
h : ∀ o' < o, preAleph o' ≤ c
x : Ordinal.{u_1}
h' : x < o
⊢ x ≤ preAleph.symm c

Proof state:
o : Ordinal.{u_1}
l : o.IsLimit
c : Cardinal.{u_1}
h : ∀ o' < o, preAleph o' ≤ c
x : Ordinal.{u_1}
h' : x < o
⊢ x ≤ preAleph.symm c

Tactic:
rw [← preAleph_le_preAleph, preAleph.apply_symm_apply]

Result:
o : Ordinal.{u_1}
l : o.IsLimit
c : Cardinal.{u_1}
h : ∀ o' < o, preAleph o' ≤ c
x : Ordinal.{u_1}
h' : x < o
⊢ preAleph x ≤ c

Proof state:
o : Ordinal.{u_1}
l : o.IsLimit
c : Cardinal.{u_1}
h : ∀ o' < o, preAleph o' ≤ c
⊢ preAleph o ≤ c

Tactic:
rw [← preAleph.apply_symm_apply c, preAleph_le_preAleph, limit_le l]

Result:
o : Ordinal.{u_1}
l : o.IsLimit
c : Cardinal.{u_1}
h : ∀ o' < o, preAleph o' ≤ c
⊢ ∀ x < o, x ≤ preAleph.symm c

Proof state:
o : Ordinal.{u_1}
l : o.IsLimit
c : Cardinal.{u_1}
h : ∀ o' < o, preAleph o' ≤ c
x : Ordinal.{u_1}
h' : x < o
⊢ preAleph x ≤ c

Tactic:
exact h _ h'

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem lintegral_comp_polarCoord_symm (f : ℂ → ℝ≥0∞) :
    (∫⁻ p in polarCoord.target, ENNReal.ofReal p.1 • f (Complex.polarCoord.symm p)) =
      ∫⁻ p, f p

Proof state:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) = ∫⁻ (p : ℂ), f p

Tactic:
rw [← (volume_preserving_equiv_real_prod.symm).lintegral_comp_emb
  measurableEquivRealProd.symm.measurableEmbedding, ← lintegral_comp_polarCoord_symm]

Result:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))

Proof state:
f : ℂ → ℝ≥0∞
⊢ ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (↑Complex.polarCoord.symm p) =
    ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))

Tactic:
simp_rw [measurableEquivRealProd_symm_polarCoord_symm_apply]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem extend_function_finite {α : Type u} {β : Type v} [Finite α] {s : Set α} (f : s ↪ β)
    (h : Nonempty (α ≃ β)) : ∃ g : α ≃ β, ∀ x : s, g x = f x

Proof state:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{max u v, u} #α = lift.{max u v, v} #β
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
rw [← lift_mk_eq.{u, v, max u v}, mk_compl_eq_mk_compl_finite_lift.{u, v, max u v} h]

Result:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{max u v, u} #α = lift.{max u v, v} #β
g : α ≃ β
⊢ lift.{max u v, u} #↑s = lift.{max u v, v} #↑(range ⇑f)

Proof state:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
obtain ⟨g⟩ := id h

Result:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Proof state:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
rw [← lift_mk_eq.{u, v, max u v}] at h

Result:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{max u v, u} #α = lift.{max u v, v} #β
g : α ≃ β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Proof state:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{max u v, u} #α = lift.{max u v, v} #β
g : α ≃ β
⊢ Injective ⇑f

Tactic:
exact f.2

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
apply extend_function.{u, v} f

Result:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Proof state:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{max u v, u} #α = lift.{max u v, v} #β
g : α ≃ β
⊢ lift.{max u v, u} #↑s = lift.{max u v, v} #↑(range ⇑f)

Tactic:
rw [mk_range_eq_lift.{u, v, max u v}]

Result:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{max u v, u} #α = lift.{max u v, v} #β
g : α ≃ β
⊢ Injective ⇑f
-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp : 1 < p) :
    1 + p * s < (1 + s) ^ p

Proof state:
s : ℝ
hs✝ : -1 ≤ s
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs' : 1 + p * s = 1
⊢ s = 0

Tactic:
rwa [add_right_eq_self, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs'

Result:
no goals

Proof state:
case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
rcases le_or_lt (1 + p * s) 0 with hs2 | hs2

Result:
case inr.inl
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 1 + p * s ≤ 0
⊢ 1 + p * s < (1 + s) ^ p

case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
⊢ 1 + p * s < (1 + s) ^ p

Proof state:
s : ℝ
hs : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
rcases eq_or_lt_of_le hs with rfl | hs

Result:
case inl
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 ≤ -1
hs' : -1 ≠ 0
⊢ 1 + p * -1 < (1 + -1) ^ p

case inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
⊢ 1 + p * s < (1 + s) ^ p

Proof state:
case inr.inr.a
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ log (1 + p * s) < log (1 + s) * p

Tactic:
rcases lt_or_gt_of_ne hs' with hs' | hs'

Result:
case inr.inr.a.inl
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s < 0
⊢ log (1 + p * s) < log (1 + s) * p

case inr.inr.a.inr
s : ℝ
hs✝ : -1 ≤ s
hs'✝ : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
hs' : s > 0
⊢ log (1 + p * s) < log (1 + s) * p

Proof state:
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ 1 + p * s < (1 + s) ^ p

Tactic:
rw [rpow_def_of_pos hs1, ← exp_log hs2]

Result:
case inr.inr
s : ℝ
hs✝ : -1 ≤ s
hs' : s ≠ 0
p : ℝ
hp : 1 < p
hp' : 0 < p
hs : -1 < s
hs1 : 0 < 1 + s
hs2 : 0 < 1 + p * s
hs3 : 1 + s ≠ 1
hs4 : 1 + p * s ≠ 1
⊢ rexp (log (1 + p * s)) < rexp (log (1 + s) * p)
-- Mathlib/Data/Real/Archimedean.lean
/-- As `sInf s = 0` when `s` is a set of reals that's unbounded below, it suffices to show that `s`
contains a nonpositive element to show that `sInf s ≤ 0`. -/
lemma sInf_nonpos' (hs : ∃ x ∈ s, x ≤ 0) : sInf s ≤ 0

Proof state:
s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0

Tactic:
obtain ⟨x, hxs, hx⟩ := hs

Result:
case intro.intro
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : x ≤ 0
⊢ sInf s ≤ 0

Proof state:
s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0

Tactic:
classical
obtain ⟨x, hxs, hx⟩ := hs
exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le

Result:
no goals

Proof state:
case intro.intro
s : Set ℝ
x : ℝ
hxs : x ∈ s
hx : x ≤ 0
⊢ sInf s ≤ 0

Tactic:
exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem is_coprod_iff_isPushout {X E Y YE : C} (c : BinaryCofan X E) (hc : IsColimit c) {f : X ⟶ Y}
    {iY : Y ⟶ YE} {fE : c.pt ⟶ YE} (H : CommSq f c.inl iY fE) :
    Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) ↔ IsPushout f c.inl iY fE

Proof state:
case mpr.uniq
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext H.isColimit

Result:
case mpr.uniq.h₀
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ H.cocone.inl ≫ m =
    H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

case mpr.uniq.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ H.cocone.inr ≫ m =
    H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Proof state:
case mpr.uniq.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ H.cocone.inr ≫ m = (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right

Tactic:
apply BinaryCofan.IsColimit.hom_ext hc

Result:
case mpr.uniq.h₁.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inl ≫ H.cocone.inr ≫ m =
    c.inl ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right

case mpr.uniq.h₁.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inr ≫ H.cocone.inr ≫ m =
    c.inr ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right
-- Mathlib/Analysis/PSeries.lean
theorem summable_nat_rpow {p : ℝ} : Summable (fun n => (n : ℝ) ^ p : ℕ → ℝ) ↔ p < -1

Proof state:
case intro
p : ℝ
⊢ (Summable fun n => ↑n ^ (-p)) ↔ -p < -1

Tactic:
simp [rpow_neg]

Result:
no goals

Proof state:
p : ℝ
⊢ (Summable fun n => ↑n ^ p) ↔ p < -1

Tactic:
rcases neg_surjective p with ⟨p, rfl⟩

Result:
case intro
p : ℝ
⊢ (Summable fun n => ↑n ^ (-p)) ↔ -p < -1
-- Mathlib/Data/PEquiv.lean
theorem trans_symm_eq_iff_forall_isSome {f : α ≃. β} :
    f.trans f.symm = PEquiv.refl α ↔ ∀ a, isSome (f a)

Proof state:
α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), (f a).isSome = true

Tactic:
rw [self_trans_symm, ofSet_eq_refl, Set.eq_univ_iff_forall]

Result:
α : Type u
β : Type v
f : α ≃. β
⊢ (∀ (x : α), x ∈ {a | (f a).isSome = true}) ↔ ∀ (a : α), (f a).isSome = true
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_sentence (φ : L.Sentence) : M ⊨ φ ↔ N ⊨ φ

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Sentence
⊢ M ⊨ φ ↔ N ⊨ φ

Tactic:
rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
  Unique.eq_default (g ∘ default)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.and (hR : Pairwise R l) (hS : Pairwise S l) :
    l.Pairwise fun a b => R a b ∧ S a b

Proof state:
case nil
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
S : α✝ → α✝ → Prop
hS : Pairwise S []
⊢ Pairwise (fun a b => R a b ∧ S a b) []

Tactic:
simp only [Pairwise.nil]

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
S : α✝ → α✝ → Prop
a✝¹ : α✝
l✝ : List α✝
R1 : ∀ (a' : α✝), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : Pairwise S l✝ → Pairwise (fun a b => R a b ∧ S a b) l✝
hS : (∀ (a' : α✝), a' ∈ l✝ → S a✝¹ a') ∧ Pairwise S l✝
⊢ (∀ (a' : α✝), a' ∈ l✝ → R a✝¹ a' ∧ S a✝¹ a') ∧ Pairwise (fun a b => R a b ∧ S a b) l✝

Tactic:
exact ⟨fun b bl => ⟨R1 b bl, hS.1 b bl⟩, IH hS.2⟩

Result:
no goals

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
S : α✝ → α✝ → Prop
hR : Pairwise R l
hS : Pairwise S l
⊢ Pairwise (fun a b => R a b ∧ S a b) l

Tactic:
induction hR with
| nil => simp only [Pairwise.nil]
| cons R1 _ IH =>
  simp only [Pairwise.nil, pairwise_cons] at hS ⊢
  exact ⟨fun b bl => ⟨R1 b bl, hS.1 b bl⟩, IH hS.2⟩

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
S : α✝ → α✝ → Prop
a✝¹ : α✝
l✝ : List α✝
R1 : ∀ (a' : α✝), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : Pairwise S l✝ → Pairwise (fun a b => R a b ∧ S a b) l✝
hS : Pairwise S (a✝¹ :: l✝)
⊢ Pairwise (fun a b => R a b ∧ S a b) (a✝¹ :: l✝)

Tactic:
simp only [Pairwise.nil, pairwise_cons] at hS ⊢

Result:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
S : α✝ → α✝ → Prop
a✝¹ : α✝
l✝ : List α✝
R1 : ∀ (a' : α✝), a' ∈ l✝ → R a✝¹ a'
a✝ : Pairwise R l✝
IH : Pairwise S l✝ → Pairwise (fun a b => R a b ∧ S a b) l✝
hS : (∀ (a' : α✝), a' ∈ l✝ → S a✝¹ a') ∧ Pairwise S l✝
⊢ (∀ (a' : α✝), a' ∈ l✝ → R a✝¹ a' ∧ S a✝¹ a') ∧ Pairwise (fun a b => R a b ∧ S a b) l✝
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive]
lemma LocallyLipschitzOn.mul (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
    LocallyLipschitzOn s fun x ↦ f x * g x := fun x hx ↦ by
  obtain ⟨Kf, t, ht, hKf⟩ := hf hx
  obtain ⟨Kg, u, hu, hKg⟩ := hg hx
  exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu,
    (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩

Proof state:
case intro.intro.intro
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x => f x * g x) t

Tactic:
obtain ⟨Kg, u, hu, hKg⟩ := hg hx

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
Kg : ℝ≥0
u : Set α
hu : u ∈ 𝓝[s] x
hKg : LipschitzOnWith Kg g u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x => f x * g x) t

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
Kg : ℝ≥0
u : Set α
hu : u ∈ 𝓝[s] x
hKg : LipschitzOnWith Kg g u
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x => f x * g x) t

Tactic:
exact ⟨Kf + Kg, t ∩ u, inter_mem ht hu,
  (hKf.mono Set.inter_subset_left).mul (hKg.mono Set.inter_subset_right)⟩

Result:
no goals

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x => f x * g x) t

Tactic:
obtain ⟨Kf, t, ht, hKf⟩ := hf hx

Result:
case intro.intro.intro
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
x : α
hx : x ∈ s
Kf : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] x
hKf : LipschitzOnWith Kf f t
⊢ ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K (fun x => f x * g x) t
-- Mathlib/Order/Fin/Basic.lean
lemma orderHom_injective_iff {α : Type*} [PartialOrder α] {n : ℕ} (f : Fin (n + 1) →o α) :
    Function.Injective f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Proof state:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f → ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Tactic:
intro hf i hi

Result:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
i : Fin n
hi : f i.castSucc = f i.succ
⊢ False

Proof state:
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f ↔ ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f → ∀ (i : Fin n), f i.castSucc ≠ f i.succ

case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ (∀ (i : Fin n), f i.castSucc ≠ f i.succ) → Injective ⇑f

Proof state:
case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), f i.castSucc ≠ f i.succ
i : Fin n
⊢ f i.castSucc < f i.succ

Tactic:
exact lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), f i.castSucc ≠ f i.succ
⊢ Injective ⇑f

Tactic:
refine (strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective

Result:
case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), f i.castSucc ≠ f i.succ
i : Fin n
⊢ f i.castSucc < f i.succ

Proof state:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
i : Fin n
hi : f i.castSucc = f i.succ
this : i.castSucc = i.succ
⊢ False

Tactic:
simp [Fin.ext_iff] at this

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
i : Fin n
hi : f i.castSucc = f i.succ
⊢ False

Tactic:
have := hf hi

Result:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
i : Fin n
hi : f i.castSucc = f i.succ
this : i.castSucc = i.succ
⊢ False

Proof state:
case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ (∀ (i : Fin n), f i.castSucc ≠ f i.succ) → Injective ⇑f

Tactic:
intro hf

Result:
case mpr
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), f i.castSucc ≠ f i.succ
⊢ Injective ⇑f