harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Lemmas.lean
theorem Heap.WF.size_eq :
    ∀ {s : Heap α}, s.WF le n → s.size = s.realSize
  | .nil, _ => rfl
  | .cons .., ⟨_, h₁, h₂⟩ => by
    simp [size, Nat.shiftLeft, size_eq h₂, Nat.pow_succ, Nat.mul_succ]
    simp [Nat.add_assoc, Nat.one_shiftLeft, h₁.realSize_eq, h₂.size_eq]

Proof state:
α : Type u_1
le : α → α → Bool
n a✝³ : Nat
a✝² : α
a✝¹ : HeapNode α
a✝ : Heap α
left✝ : n ≤ a✝³
h₁ : HeapNode.WF le a✝² a✝¹ a✝³
h₂ : WF le (a✝³ + 1) a✝
⊢ (cons a✝³ a✝² a✝¹ a✝).size = (cons a✝³ a✝² a✝¹ a✝).realSize

Tactic:
simp [size, Nat.shiftLeft, size_eq h₂, Nat.pow_succ, Nat.mul_succ]

Result:
α : Type u_1
le : α → α → Bool
n a✝³ : Nat
a✝² : α
a✝¹ : HeapNode α
a✝ : Heap α
left✝ : n ≤ a✝³
h₁ : HeapNode.WF le a✝² a✝¹ a✝³
h₂ : WF le (a✝³ + 1) a✝
⊢ 1 <<< a✝³ = a✝¹.realSize + 1

Proof state:
α : Type u_1
le : α → α → Bool
n a✝³ : Nat
a✝² : α
a✝¹ : HeapNode α
a✝ : Heap α
left✝ : n ≤ a✝³
h₁ : HeapNode.WF le a✝² a✝¹ a✝³
h₂ : WF le (a✝³ + 1) a✝
⊢ 1 <<< a✝³ = a✝¹.realSize + 1

Tactic:
simp [Nat.add_assoc, Nat.one_shiftLeft, h₁.realSize_eq, h₂.size_eq]

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
@[simp]
lemma matPolyEquiv_map_smul (p : R[X]) (M : Matrix n n R[X]) :
    matPolyEquiv (p • M) = p.map (algebraMap _ _) * matPolyEquiv M

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
M : Matrix n n R[X]
⊢ matPolyEquiv (p • M) = Polynomial.map (algebraMap R (Matrix n n R)) p * matPolyEquiv M

Tactic:
rw [← one_mul M, ← smul_mul_assoc, _root_.map_mul, matPolyEquiv_smul_one, one_mul]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j) :
    X.δ i ≫ X.δ j =
      X.δ (j.pred fun (hj : j = 0) => by simp only [hj, Fin.not_lt_zero] at H) ≫
        X.δ (Fin.castSucc i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.δ i ≫ X.δ j = X.δ (j.pred ⋯) ≫ X.δ i.castSucc

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) =
    X.map (SimplexCategory.δ (j.pred ⋯)) ≫ X.map (SimplexCategory.δ i.castSucc)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
hj : j = 0
⊢ False

Tactic:
simp only [hj, Fin.not_lt_zero] at H

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) =
    X.map (SimplexCategory.δ (j.pred ⋯)) ≫ X.map (SimplexCategory.δ i.castSucc)

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem eq_of_dist_eq_of_dist_eq_of_finrank_eq_two [FiniteDimensional ℝ V] (hd : finrank ℝ V = 2)
    {c₁ c₂ p₁ p₂ p : P} {r₁ r₂ : ℝ} (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : dist p₁ c₁ = r₁)
    (hp₂c₁ : dist p₂ c₁ = r₁) (hpc₁ : dist p c₁ = r₁) (hp₁c₂ : dist p₁ c₂ = r₂)
    (hp₂c₂ : dist p₂ c₂ = r₂) (hpc₂ : dist p c₂ = r₂) : p = p₁ ∨ p = p₂ :=
  haveI hd' : finrank ℝ (⊤ : AffineSubspace ℝ P).direction = 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = 2
c₁ c₂ p₁ p₂ p : P
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ finrank ℝ V = 2

Tactic:
exact hd

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
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = 2
c₁ c₂ p₁ p₂ p : P
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ finrank ℝ ↥⊤.direction = 2

Tactic:
rw [direction_top, finrank_top]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = 2
c₁ c₂ p₁ p₂ p : P
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
⊢ finrank ℝ V = 2
-- Mathlib/Data/Set/Image.lean
theorem range_subset_singleton {f : ι → α} {x : α} : range f ⊆ {x} ↔ f = const ι x

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
x : α
⊢ range f ⊆ {x} ↔ f = const ι x

Tactic:
simp [range_subset_iff, funext_iff, mem_singleton]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem card_nsmul_le_card_nsmul [∀ a b, Decidable (r a b)]
    (hm : ∀ a ∈ s, m ≤ #(t.bipartiteAbove r a))
    (hn : ∀ b ∈ t, #(s.bipartiteBelow r b) ≤ n) : #s • m ≤ #t • n :=
  calc
    _ ≤ ∑ a ∈ s, (#(t.bipartiteAbove r a) : R) := s.card_nsmul_le_sum _ _ hm
    _ = ∑ b ∈ t, (#(s.bipartiteBelow r b) : R)

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : OrderedSemiring R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ↑(∑ x ∈ s, #(bipartiteAbove r t x)) = ↑(∑ x ∈ t, #(bipartiteBelow r s x))

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : OrderedSemiring R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast

Result:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : OrderedSemiring R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ↑(∑ x ∈ s, #(bipartiteAbove r t x)) = ↑(∑ x ∈ t, #(bipartiteBelow r s x))
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_one (m : M) : mk' f m (1 : S) = f m

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ mk' f m 1 = f m

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = f m

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m 1) = f m

Tactic:
rw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one,
  one_smul]

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem cmp_self_eq_eq : cmp x x = Ordering.eq

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
⊢ cmp x x = eq

Tactic:
rw [cmp_eq_eq_iff]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_eq_toNNReal_tsum {f : β → ℝ≥0} : ∑' b, f b = (∑' b, (f b : ℝ≥0∞)).toNNReal

Proof state:
case pos
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
rw [← ENNReal.coe_tsum h, ENNReal.toNNReal_coe]

Result:
no goals

Proof state:
case neg
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
have A := tsum_eq_zero_of_not_summable h

Result:
case neg
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
A : ∑' (b : β), f b = 0
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Proof state:
case neg
β : Type u_2
f : β → ℝ≥0
A : ∑' (b : β), f b = 0
h : ∑' (b : β), ↑(f b) = ⊤
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
simp only [h, ENNReal.top_toNNReal, A]

Result:
no goals

Proof state:
case neg
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
A : ∑' (b : β), f b = 0
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Classical.not_not] at h

Result:
case neg
β : Type u_2
f : β → ℝ≥0
A : ∑' (b : β), f b = 0
h : ∑' (b : β), ↑(f b) = ⊤
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Proof state:
β : Type u_2
f : β → ℝ≥0
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
by_cases h : Summable f

Result:
case pos
β : Type u_2
f : β → ℝ≥0
h : Summable f
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

case neg
β : Type u_2
f : β → ℝ≥0
h : ¬Summable f
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_inter (x y : ZFSet.{u}) : (x ∩ y).toSet = x.toSet ∩ y.toSet

Proof state:
case h
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ (ZFSet.sep (fun z => z ∈ y) x).toSet ↔ x✝ ∈ x.toSet ∩ y.toSet

Tactic:
simp

Result:
no goals

Proof state:
x y : ZFSet.{u}
⊢ (x ∩ y).toSet = x.toSet ∩ y.toSet

Tactic:
change (ZFSet.sep (fun z => z ∈ y) x).toSet = _

Result:
x y : ZFSet.{u}
⊢ (ZFSet.sep (fun z => z ∈ y) x).toSet = x.toSet ∩ y.toSet

Proof state:
x y : ZFSet.{u}
⊢ (ZFSet.sep (fun z => z ∈ y) x).toSet = x.toSet ∩ y.toSet

Tactic:
ext

Result:
case h
x y x✝ : ZFSet.{u}
⊢ x✝ ∈ (ZFSet.sep (fun z => z ∈ y) x).toSet ↔ x✝ ∈ x.toSet ∩ y.toSet
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma opcyclesMap_comp_descOpcycles (φ : S₁ ⟶ S) [S₁.HasRightHomology] :
    opcyclesMap φ ≫ S.descOpcycles k hk =
      S₁.descOpcycles (φ.τ₂ ≫ k) (by rw [← φ.comm₁₂_assoc, hk, comp_zero])

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ : ShortComplex C
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : S.HasRightHomology
φ : S₁ ⟶ S
inst✝ : S₁.HasRightHomology
⊢ opcyclesMap φ ≫ S.descOpcycles k hk = S₁.descOpcycles (φ.τ₂ ≫ k) ⋯

Tactic:
simp only [← cancel_epi (S₁.pOpcycles), p_opcyclesMap_assoc, p_descOpcycles]

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{?u.263089, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : S.HasRightHomology
φ : S₁ ⟶ S
inst✝ : S₁.HasRightHomology
⊢ S₁.f ≫ φ.τ₂ ≫ k = 0

Tactic:
rw [← φ.comm₁₂_assoc, hk, comp_zero]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjUnion_eq_union (s t h) : @disjUnion α s t h = s ∪ t :=
  ext fun a => by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
a : α
⊢ a ∈ s.disjUnion t h ↔ a ∈ s ∪ t

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma nonempty_of_neZero (μ : Measure α) [NeZero μ] : Nonempty α :=
  (isEmpty_or_nonempty α).resolve_left fun h ↦ by
    simpa [eq_empty_of_isEmpty] using NeZero.ne (μ univ)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NeZero μ
h : IsEmpty α
⊢ False

Tactic:
simpa [eq_empty_of_isEmpty] using NeZero.ne (μ univ)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem isLocalHom_expand {p : ℕ} (hp : 0 < p) : IsLocalHom (expand R p)

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
⊢ IsUnit f

Tactic:
have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (((expand R p) f).coeff 0)
⊢ IsUnit f

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (((expand R p) f).coeff 0)
⊢ IsUnit f

Tactic:
rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
rwa [hf2, isUnit_C]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
rw [expand_eq_C hp] at hf2

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = C (f.coeff 0)
⊢ IsUnit f

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalHom (expand R p)

Tactic:
refine ⟨fun f hf1 => ?_⟩

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
⊢ IsUnit f

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit ((expand R p) f)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f

Tactic:
rw [hf2, isUnit_C] at hf1

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : (expand R p) f = C (f.coeff 0)
⊢ IsUnit f
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem toIdeal_iSup₂ {κ : Sort*} {κ' : κ → Sort*} (s : ∀ i, κ' i → HomogeneousIdeal 𝒜) :
    (⨆ (i) (j), s i j).toIdeal = ⨆ (i) (j), (s i j).toIdeal

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ (⨆ i, ⨆ j, s i j).toIdeal = ⨆ i, ⨆ j, (s i j).toIdeal

Tactic:
simp_rw [toIdeal_iSup]

Result:
no goals
-- Mathlib/Order/Interval/Set/Image.lean
private lemma image_subtype_val_Ixx_Ixi {p q r : α → α → Prop} {a b : α} (c : {x // p a x ∧ q x b})
    (h : ∀ {x}, r c x → p a x) :
    Subtype.val '' {y : {x // p a x ∧ q x b} | r c.1 y.1} = {y : α | r c.1 y ∧ q y b} :=
  (Subtype.image_preimage_val {x | p a x ∧ q x b} {y | r c.1 y}).trans <| by
    ext; simp +contextual [@and_comm (r _ _), h]

Proof state:
case h
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} ↔ x✝ ∈ {y | r (↑c) y ∧ q y b}

Tactic:
simp +contextual [@and_comm (r _ _), h]

Result:
no goals

Proof state:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
⊢ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} = {y | r (↑c) y ∧ q y b}

Tactic:
ext

Result:
case h
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} ↔ x✝ ∈ {y | r (↑c) y ∧ q y b}
-- Mathlib/Order/LiminfLimsup.lean
theorem IsBoundedUnder.bddAbove_range_of_cofinite [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β}
    (hf : IsBoundedUnder (· ≤ ·) cofinite f) : BddAbove (range f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) cofinite f
⊢ BddAbove (range f)

Tactic:
rcases hf with ⟨b, hb⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 => x1 ≤ x2) x b
⊢ BddAbove (range f)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 => x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (range f)

Tactic:
rw [← image_univ, ← union_compl_self { x | f x ≤ b }, image_union, bddAbove_union]

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 => x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 => x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)

Tactic:
exact ⟨⟨b, forall_mem_image.2 fun x => id⟩, (hb.image f).bddAbove⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 => x1 ≤ x2) x b
⊢ BddAbove (range f)

Tactic:
haveI : Nonempty β := ⟨b⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirected β fun x1 x2 => x1 ≤ x2
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 => x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (range f)
-- Mathlib/Topology/Sheaves/Skyscraper.lean
theorem fromStalk_to_skyscraper {𝓕 : Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c) :
    fromStalk p₀ (toSkyscraperPresheaf _ f) = f

Proof state:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
⊢ fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f

Tactic:
refine 𝓕.stalk_hom_ext fun U hxU ↦ ?_

Result:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U : Opens ↑X
hxU : p₀ ∈ U
⊢ 𝓕.germ U p₀ hxU ≫ fromStalk p₀ (toSkyscraperPresheaf p₀ f) = 𝓕.germ U p₀ hxU ≫ f

Proof state:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U : Opens ↑X
hxU : p₀ ∈ U
⊢ 𝓕.germ U p₀ hxU ≫ fromStalk p₀ (toSkyscraperPresheaf p₀ f) = 𝓕.germ U p₀ hxU ≫ f

Tactic:
rw [germ_fromStalk, toSkyscraperPresheaf_app, dif_pos hxU, Category.assoc, Category.assoc,
  eqToHom_trans, eqToHom_refl, Category.comp_id, Presheaf.germ]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_lt_self (ha : 0 < a) (hb : 1 < b) : a / b < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
hb : 1 < b
⊢ a / b < a

Tactic:
simpa only [div_one] using div_lt_div_of_pos_left ha zero_lt_one hb

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_sup : span R s ⊔ p = span R (s ∪ p)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
s : Set M
⊢ span R s ⊔ p = span R (s ∪ ↑p)

Tactic:
rw [Submodule.span_union, p.span_eq]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem opRingEquiv_single [AddCommMonoid G] (r : k) (x : G) :
    AddMonoidAlgebra.opRingEquiv (op (single x r)) = single x (op r)

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddCommMonoid G
r : k
x : G
⊢ AddMonoidAlgebra.opRingEquiv (op (single x r)) = single x (op r)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sq_sqrt (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt a ^ 2 = a

Tactic:
rw [pow_two, sqrt_mul_sqrt_self (A := A) a]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supported_empty : supported M R (∅ : Set α) = ⊥ :=
  eq_bot_iff.2 fun l h => (Submodule.mem_bot R).2 <| by ext; simp_all [mem_supported']

Proof state:
case h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
a✝ : α
⊢ l a✝ = 0 a✝

Tactic:
simp_all [mem_supported']

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
⊢ l = 0

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
l : α →₀ M
h : l ∈ supported M R ∅
a✝ : α
⊢ l a✝ = 0 a✝
-- Mathlib/GroupTheory/CoprodI.lean
theorem prod_singleton {i} (x : M i) (hne_one : x ≠ 1) : (singleton x hne_one).prod = of x

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
x : M i
hne_one : x ≠ 1
⊢ (singleton x hne_one).prod = of x

Tactic:
simp [toWord, prod, Word.prod]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
lemma disjoint_supp_of_not_mem (hrep : Represents s C) (h : c ∉ C) : Disjoint s c.supp

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
a : V
ha : a ∈ s
h : G.connectedComponentMk a ∉ C
⊢ False

Tactic:
exact h (hrep.1 ha)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ Disjoint s c.supp

Tactic:
rw [Set.disjoint_left]

Result:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ ∀ ⦃a : V⦄, a ∈ s → a ∉ c.supp

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
⊢ ∀ ⦃a : V⦄, a ∈ s → a ∉ c.supp

Tactic:
intro a ha hc

Result:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
ha : a ∈ s
hc : a ∈ c.supp
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
ha : a ∈ s
hc : a ∈ c.supp
⊢ False

Tactic:
simp only [mem_supp_iff] at hc

Result:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
ha : a ∈ s
hc : G.connectedComponentMk a = c
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∉ C
a : V
ha : a ∈ s
hc : G.connectedComponentMk a = c
⊢ False

Tactic:
subst hc

Result:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
hrep : Represents s C
a : V
ha : a ∈ s
h : G.connectedComponentMk a ∉ C
⊢ False
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
lemma c_iso' {V : Opens Y} (U : Opens X) (h : V = (opensFunctor f).obj U) :
    IsIso (f.c.app (Opposite.op V))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ IsIso (f.c.app (op ((opensFunctor f).obj U)))

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
V : Opens ↑↑Y
U : Opens ↑↑X
h : V = (opensFunctor f).obj U
⊢ IsIso (f.c.app (op V))

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ IsIso (f.c.app (op ((opensFunctor f).obj U)))