harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fin/Tuple/Basic.lean
lemma insertNth_rev {α : Sort*} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)) :
    insertNth (α := fun _ ↦ α) i a f (rev j) = insertNth (α := fun _ ↦ α) i.rev a (f ∘ rev) j

Proof state:
case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (i.rev.succAbove j✝).rev = i.rev.insertNth a (f ∘ rev) (i.rev.succAbove j✝)

Tactic:
simp [rev_succAbove]

Result:
no goals

Proof state:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j : Fin (n + 1)
⊢ i.insertNth a f j.rev = i.rev.insertNth a (f ∘ rev) j

Tactic:
induction j using Fin.succAboveCases

Result:
case i
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ Fin (n + 1)

case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ i.insertNth a f (rev ?i) = i.rev.insertNth a (f ∘ rev) ?i

case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j✝ : Fin n
⊢ i.insertNth a f (succAbove ?i j✝).rev = i.rev.insertNth a (f ∘ rev) (succAbove ?i j✝)

Proof state:
case i
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ Fin (n + 1)

Tactic:
exact rev i

Result:
no goals

Proof state:
case x
n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
⊢ i.insertNth a f i.rev.rev = i.rev.insertNth a (f ∘ rev) i.rev

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem sum_rec_congr (P : α ⊕ β → Sort*) (f : ∀ i, P (inl i)) (g : ∀ i, P (inr i))
    {x y : α ⊕ β} (h : x = y) :
    @Sum.rec _ _ _ f g x = cast (congr_arg P h.symm) (@Sum.rec _ _ _ f g y)

Proof state:
case refl
α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x : α ⊕ β
⊢ rec f g x = cast ⋯ (rec f g x)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x y : α ⊕ β
h : x = y
⊢ rec f g x = cast ⋯ (rec f g y)

Tactic:
cases h

Result:
case refl
α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x : α ⊕ β
⊢ rec f g x = cast ⋯ (rec f g x)
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
lemma degreesLE_add : degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
⊢ degreesLE R σ (s + t) ≤ degreesLE R σ s * degreesLE R σ t ∧
    ∀ m ∈ degreesLE R σ s, ∀ n ∈ degreesLE R σ t, m * n ∈ degreesLE R σ (s + t)

Tactic:
refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
  fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : i ∈ x.support
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
let a := (i.toMultiset - t).toFinsupp

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
⊢ (monomial i) (coeff i x) ∈ degreesLE R σ s * degreesLE R σ t

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s t : Multiset σ
x : MvPolynomial σ R
hx : x ∈ degreesLE R σ (s + t)
i : σ →₀ ℕ
hi : toMultiset i ≤ s + t
a : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i - t)
b : σ →₀ ℕ := Multiset.toFinsupp (toMultiset i ⊓ t)
this : a + b = i
ha : toMultiset a ≤ s
hb : toMultiset b ≤ t
⊢ (monomial a) (coeff i x) * (monomial b) 1 ∈ degreesLE R σ s * degreesLE R σ t

Tactic:
exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
private lemma continuousAt_mul_top_pos {a : ℝ} (h : 0 < a) :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (⊤, a)

Proof state:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Tactic:
replace lock := le_trans lock key

Result:
case h.refine_1.intro
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < p.1 * p.2

Proof state:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2

Tactic:
intros p p_in_prod

Result:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2)
⊢ ↑x < p.1 * p.2

Proof state:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ ↑x < ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2)

Tactic:
rw [← EReal.coe_mul, EReal.coe_lt_coe_iff, _root_.div_mul_div_comm, mul_comm,
  ← _root_.div_mul_div_comm, mul_div_right_comm]

Result:
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p1_gt : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1
p2_gt : ↑(a / 2) < p.2
p1_pos : 0 < p.1
a2_pos : 0 < ↑(a / 2)
key : p.1 * ↑(a / 2) ≤ p.1 * p.2
lock : ↑(2 * ((x + 1) ⊔ 0) / a) * ↑(a / 2) ≤ p.1 * p.2
⊢ x < a / a * (2 / 2 * ((x + 1) ⊔ 0))

Proof state:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : p ∈ Ioi ↑(2 * ((x + 1) ⊔ 0) / a) ×ˢ Ioi ↑(a / 2)
⊢ ↑x < p.1 * p.2

Tactic:
simp only [Set.mem_prod, Set.mem_Ioi] at p_in_prod

Result:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
p : EReal × EReal
p_in_prod : ↑(2 * ((x + 1) ⊔ 0) / a) < p.1 ∧ ↑(a / 2) < p.2
⊢ ↑x < p.1 * p.2
-- Mathlib/Data/Multiset/NatAntidiagonal.lean
theorem mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n

Proof state:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ antidiagonal n ↔ x.1 + x.2 = n

Tactic:
rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]

Result:
no goals
-- Mathlib/Data/Set/Card/Arithmetic.lean
theorem Infinite.exists_union_disjoint_cardinal_eq_of_infinite (h : s.Infinite) :
    ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u

Proof state:
case intro.refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' (⇑f ⁻¹' range Sum.inl)) = #↑(Subtype.val '' (⇑f ⁻¹' range Sum.inr))

Tactic:
simp [mk_image_eq Subtype.val_injective]

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Disjoint (Subtype.val '' (⇑f ⁻¹' range Sum.inl)) (Subtype.val '' (⇑f ⁻¹' range Sum.inr))

Tactic:
exact disjoint_image_of_injective Subtype.val_injective
  (isCompl_range_inl_range_inr.disjoint.preimage f)

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.Infinite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
have := h.to_subtype

Result:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Proof state:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
obtain ⟨f⟩ : Nonempty (s ≃ s ⊕ s) := by
  rw [← Cardinal.eq, ← add_def, add_mk_eq_self]

Result:
case intro
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Proof state:
case intro
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
refine ⟨Subtype.val '' (f ⁻¹' (range .inl)), Subtype.val '' (f ⁻¹' (range .inr)), ?_, ?_, ?_⟩

Result:
case intro.refine_1
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Subtype.val '' (⇑f ⁻¹' range Sum.inl) ∪ Subtype.val '' (⇑f ⁻¹' range Sum.inr) = s

case intro.refine_2
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Disjoint (Subtype.val '' (⇑f ⁻¹' range Sum.inl)) (Subtype.val '' (⇑f ⁻¹' range Sum.inr))

case intro.refine_3
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ #↑(Subtype.val '' (⇑f ⁻¹' range Sum.inl)) = #↑(Subtype.val '' (⇑f ⁻¹' range Sum.inr))

Proof state:
case intro.refine_1
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
f : ↑s ≃ ↑s ⊕ ↑s
⊢ Subtype.val '' (⇑f ⁻¹' range Sum.inl) ∪ Subtype.val '' (⇑f ⁻¹' range Sum.inr) = s

Tactic:
simp [← image_union, ← preimage_union]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite ↑s
⊢ Nonempty (↑s ≃ ↑s ⊕ ↑s)

Tactic:
rw [← Cardinal.eq, ← add_def, add_mk_eq_self]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHoms_v (ψ : ∀ (p : ℤ), F.X p ⟶ G.X p) (p : ℤ) :
    (ofHoms ψ).v p p (add_zero p) = ψ p

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
ψ : (p : ℤ) → F.X p ⟶ G.X p
p : ℤ
⊢ (ofHoms ψ).v p p ⋯ = ψ p

Tactic:
simp only [ofHoms, mk_v, eqToHom_refl, comp_id]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Lean/Except.lean
theorem map_mk [Monad m] [LawfulMonad m] (f : α → β) (x : m (Except ε α)) :
    f <$> ExceptT.mk x = ExceptT.mk ((f <$> · ) <$> x)

Proof state:
case e_x.e_a
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m (Except ε α)
⊢ (fun a =>
      match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
    fun a =>
    pure
      (match a with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok (f v))

Tactic:
funext a

Result:
case e_x.e_a.h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m (Except ε α)
a : Except ε α
⊢ (match a with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure
      (match a with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok (f v))

Proof state:
case e_x.e_a.h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m (Except ε α)
a : Except ε α
⊢ (match a with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure
      (match a with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok (f v))

Tactic:
split <;> simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m (Except ε α)
⊢ (mk do
      let a ← mk x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    mk do
      let a ← x
      pure
          (match a with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (f v))

Tactic:
congr

Result:
case e_x.e_a
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m (Except ε α)
⊢ (fun a =>
      match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
    fun a =>
    pure
      (match a with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok (f v))

Proof state:
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m (Except ε α)
⊢ f <$> mk x = mk ((fun x => f <$> x) <$> x)

Tactic:
simp only [Functor.map, Except.map, ExceptT.map, map_eq_pure_bind]

Result:
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : m (Except ε α)
⊢ (mk do
      let a ← mk x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    mk do
      let a ← x
      pure
          (match a with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (f v))
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma pred_eq_succ_iff : n - 1 = m + 1 ↔ n = m + 2

Proof state:
m n : ℕ
⊢ n - 1 = m + 1 ↔ n = m + 2

Tactic:
cases n <;> constructor <;> rintro ⟨⟩ <;> rfl

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem natDegree_pos [Nontrivial B] (hx : IsIntegral A x) : 0 < natDegree (minpoly A x)

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ C ((minpoly A x).coeff 0) = 1

Tactic:
convert C_1 (R := A)

Result:
case h.e'_2.h.e'_6
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ (minpoly A x).coeff 0 = 1

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ 0 < (minpoly A x).natDegree

Tactic:
rw [pos_iff_ne_zero]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ (minpoly A x).natDegree ≠ 0

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
⊢ (minpoly A x).natDegree ≠ 0

Tactic:
intro ndeg_eq_zero

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ False

Proof state:
case h.e'_2.h.e'_6
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ (minpoly A x).coeff 0 = 1

Tactic:
simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
eq_one : minpoly A x = 1
⊢ False

Tactic:
simpa only [eq_one, map_one, one_ne_zero] using aeval A x

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ False

Tactic:
have eq_one : minpoly A x = 1 := by
  rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
  convert C_1 (R := A)
  simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
eq_one : minpoly A x = 1
⊢ False

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ minpoly A x = 1

Tactic:
rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
hx : IsIntegral A x
ndeg_eq_zero : (minpoly A x).natDegree = 0
⊢ C ((minpoly A x).coeff 0) = 1
-- Mathlib/Topology/MetricSpace/GromovHausdorff.lean
theorem GHSpace.toGHSpace_rep (p : GHSpace) : toGHSpace p.Rep = p

Proof state:
p : GHSpace
⊢ ⟦Quot.out p⟧ = p

Tactic:
exact Quot.out_eq p

Result:
no goals

Proof state:
p : GHSpace
⊢ toGHSpace ↥(Quot.out p) = p

Tactic:
rw [← eq_toGHSpace]

Result:
p : GHSpace
⊢ ⟦Quot.out p⟧ = p

Proof state:
p : GHSpace
⊢ toGHSpace p.Rep = p

Tactic:
change toGHSpace (Quot.out p : NonemptyCompacts ℓ_infty_ℝ) = p

Result:
p : GHSpace
⊢ toGHSpace ↥(Quot.out p) = p
-- Mathlib/Data/ENat/Lattice.lean
lemma finite_of_sSup_lt_top (h : sSup s < ⊤) : s.Finite

Proof state:
s : Set ℕ∞
h : ¬s.Finite
⊢ ⊤ ≤ sSup s

Tactic:
simp only [top_le_iff]

Result:
s : Set ℕ∞
h : ¬s.Finite
⊢ sSup s = ⊤

Proof state:
s : Set ℕ∞
h : sSup s < ⊤
⊢ s.Finite

Tactic:
contrapose! h

Result:
s : Set ℕ∞
h : ¬s.Finite
⊢ ⊤ ≤ sSup s

Proof state:
s : Set ℕ∞
h : ¬s.Finite
⊢ sSup s = ⊤

Tactic:
exact sSup_eq_top_of_infinite h

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiableWithinAt.mdifferentiableAt (h : MDifferentiableWithinAt I I' f s x)
    (hs : s ∈ 𝓝 x) : MDifferentiableAt I I' f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
hs : s ∈ 𝓝 x
⊢ s = univ ∩ s

Tactic:
rw [univ_inter]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
hs : s ∈ 𝓝 x
this : s = univ ∩ s
⊢ MDifferentiableAt I I' f x

Tactic:
rwa [this, mdifferentiableWithinAt_inter hs, mdifferentiableWithinAt_univ] at h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
hs : s ∈ 𝓝 x
⊢ MDifferentiableAt I I' f x

Tactic:
have : s = univ ∩ s := by rw [univ_inter]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
h : MDifferentiableWithinAt I I' f s x
hs : s ∈ 𝓝 x
this : s = univ ∩ s
⊢ MDifferentiableAt I I' f x
-- Mathlib/Data/Nat/Init.lean
lemma div_mul_div_le_div (a b c : ℕ) : a / c * b / a ≤ b / c

Proof state:
a b c : ℕ
ha : a > 0
⊢ a / c * b ≤ b * a / c

Tactic:
rw [Nat.mul_comm]

Result:
a b c : ℕ
ha : a > 0
⊢ b * (a / c) ≤ b * a / c

Proof state:
a b c : ℕ
ha : a > 0
⊢ b * a / c / a = b / c

Tactic:
rw [Nat.div_div_eq_div_mul, Nat.mul_comm b, Nat.mul_comm c,
Nat.mul_div_mul_left _ _ ha]

Result:
no goals

Proof state:
a b c : ℕ
⊢ a / c * b / a ≤ b / c

Tactic:
obtain rfl | ha := Nat.eq_zero_or_pos a

Result:
case inl
b c : ℕ
⊢ 0 / c * b / 0 ≤ b / c

case inr
a b c : ℕ
ha : a > 0
⊢ a / c * b / a ≤ b / c

Proof state:
a b c : ℕ
ha : a > 0
⊢ b * (a / c) ≤ b * a / c

Tactic:
exact mul_div_le_mul_div_assoc _ _ _

Result:
no goals

Proof state:
case inr
a b c : ℕ
ha : a > 0
⊢ a / c * b / a ≤ b / c

Tactic:
calc
  a / c * b / a ≤ b * a / c / a :=
    Nat.div_le_div_right (by rw [Nat.mul_comm]; exact mul_div_le_mul_div_assoc _ _ _)
  _ = b / c := by rw [Nat.div_div_eq_div_mul, Nat.mul_comm b, Nat.mul_comm c,
      Nat.mul_div_mul_left _ _ ha]

Result:
no goals

Proof state:
case inl
b c : ℕ
⊢ 0 / c * b / 0 ≤ b / c

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem mapRange_zero {f : M → N} {hf : f 0 = 0} : mapRange f hf (0 : α →₀ M) = 0 :=
  ext fun _ => by simp only [hf, zero_apply, mapRange_apply]

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : Zero M
inst✝ : Zero N
f : M → N
hf : f 0 = 0
x✝ : α
⊢ (mapRange f hf 0) x✝ = 0 x✝

Tactic:
simp only [hf, zero_apply, mapRange_apply]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_inf {f g : Filter α} {m : α → β} (h : Injective m) :
    map m (f ⊓ g) = map m f ⊓ map m g

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m f ⊓ map m g ≤ map m (f ⊓ g)

Tactic:
rintro t ⟨s₁, hs₁, s₂, hs₂, ht : m ⁻¹' t = s₁ ∩ s₂⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ t ∈ map m f ⊓ map m g

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ t ∈ map m f ⊓ map m g

Tactic:
refine mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
refine map_inf_le.antisymm ?_

Result:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m f ⊓ map m g ≤ map m (f ⊓ g)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
t : Set β
s₁ : Set α
hs₁ : s₁ ∈ f
s₂ : Set α
hs₂ : s₂ ∈ g
ht : m ⁻¹' t = s₁ ∩ s₂
⊢ m '' s₁ ∩ m '' s₂ ⊆ t

Tactic:
rw [← image_inter h, image_subset_iff, ht]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_of_Z_eq_zero {P : Fin 3 → F} (hPz : P z = 0) : toAffine W P = 0

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z = 0
⊢ toAffine W P = 0

Tactic:
rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]

Result:
no goals