harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/RatFunc/Defs.lean
theorem liftOn_ofFractionRing_mk {P : Sort v} (n : K[X]) (d : K[X]⁰) (f : K[X] → K[X] → P)
    (H : ∀ {p q p' q'} (_hq : q ∈ K[X]⁰) (_hq' : q' ∈ K[X]⁰), q' * p = q * p' → f p q = f p' q') :
    RatFunc.liftOn (ofFractionRing (Localization.mk n d)) f @H = f n d

Proof state:
K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ { toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d

Tactic:
rw [RatFunc.liftOn]

Result:
K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d }.toFractionRing (fun p q => f p ↑q) ⋯ = f n ↑d

Proof state:
K : Type u
inst✝ : CommRing K
P : Sort v
n : K[X]
d : ↥K[X]⁰
f : K[X] → K[X] → P
H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'
⊢ Localization.liftOn { toFractionRing := Localization.mk n d }.toFractionRing (fun p q => f p ↑q) ⋯ = f n ↑d

Tactic:
exact Localization.liftOn_mk _ _ _ _

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem Finset.prod_toFinset_eq_subtype {M : Type*} [CommMonoid M] [Fintype α] (p : α → Prop)
    [DecidablePred p] (f : α → M) : ∏ a ∈ { x | p x }.toFinset, f a = ∏ a : Subtype p, f a

Proof state:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

Tactic:
simp_rw [Set.mem_toFinset]

Result:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Proof state:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Tactic:
intro

Result:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝

Proof state:
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∏ a ∈ {x | p x}.toFinset, f a = ∏ a : Subtype p, f ↑a

Tactic:
rw [← Finset.prod_subtype]

Result:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem lt_length_left_of_zipWith {f : α → β → γ} {i : Nat} {l : List α} {l' : List β}
    (h : i < (zipWith f l l').length) : i < l.length

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : List α
l' : List β
h : i < (zipWith f l l').length
⊢ i < l.length

Tactic:
rw [length_zipWith] at h

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : List α
l' : List β
h : i < min l.length l'.length
⊢ i < l.length

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : List α
l' : List β
h : i < min l.length l'.length
⊢ i < l.length

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_add_mul_monomial (a : R) :
    coeff R (m + n) (φ * monomial R n a) = coeff R m φ * a

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R (m + n)) (φ * (monomial R n) a) = (coeff R m) φ * a

Tactic:
rw [coeff_mul_monomial, if_pos, add_tsub_cancel_right]

Result:
case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ n ≤ m + n

Proof state:
case hc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ n ≤ m + n

Tactic:
exact le_add_left le_rfl

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_inter [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
    eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∩ t) ↔ a✝ ∈ eraseNone s ∩ eraseNone t

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∩ t) = eraseNone s ∩ eraseNone t

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∩ t) ↔ a✝ ∈ eraseNone s ∩ eraseNone t
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.eraseMin_aux {s l} {x : α} {r o₁ o₂} (H : Valid' o₁ (.node s l x r) o₂) :
    Valid' ↑(findMin' l x) (@eraseMin α (.node' l x r)) o₂ ∧
      size (.node' l x r) = size (eraseMin (.node' l x r)) + 1

Proof state:
α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax ↑(findMax' x l.dual) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

Tactic:
rwa [← dual_node', size_dual, ← dual_eraseMin, size_dual, ← Valid'.dual_iff, findMax'_dual]
  at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1

Tactic:
have := H.dual.eraseMax_aux

Result:
α : Type u_1
inst✝ : Preorder α
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ (Ordnode.node s l x r) o₂
this :
  Valid' o₂ (r.dual.node' x l.dual).eraseMax ↑(findMax' x l.dual) ∧
    (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1
⊢ Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
theorem isometric_cfc (f : C(S, R)) (halg : Isometry (algebraMap R S)) (h0 : p 0)
    (h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) :
    IsometricContinuousFunctionalCalculus R A p where
  toContinuousFunctionalCalculus := SpectrumRestricts.cfc f halg.isUniformEmbedding h0 h
  isometric a ha

Proof state:
case intro.refine_2
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
_inst : ∀ (a : A), CompactSpace ↑(σ R a)
this : ContinuousFunctionalCalculus R p
g₁ g₂ : C(↑(σ R a), R)
⊢ dist g₁ g₂ ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))

Tactic:
refine ContinuousMap.dist_le dist_nonneg |>.mpr fun x ↦ ?_

Result:
case intro.refine_2
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Semifield S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalSemiring S
inst✝¹² : ContinuousStar S
inst✝¹¹ : Ring A
inst✝¹⁰ : StarRing A
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : IsScalarTower R S A
inst✝⁵ : StarModule R S
inst✝⁴ : ContinuousSMul R S
inst✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
_inst : ∀ (a : A), CompactSpace ↑(σ R a)
this : ContinuousFunctionalCalculus R p
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
⊢ dist (g₁ x) (g₂ x) ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
-- Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean
theorem coe_pow (p : SubMulAction R M) : ∀ {n : ℕ} (_ : n ≠ 0), ↑(p ^ n) = (p : Set M) ^ n
  | 0, hn => (hn rfl).elim
  | 1, _ => by rw [pow_one, pow_one]
  | n + 2, _ => by
    rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
x✝ : 1 ≠ 0
⊢ ↑(p ^ 1) = ↑p ^ 1

Tactic:
rw [pow_one, pow_one]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : Monoid M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
p : SubMulAction R M
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ↑(p ^ (n + 2)) = ↑p ^ (n + 2)

Tactic:
rw [pow_succ _ (n + 1), pow_succ _ (n + 1), coe_mul, coe_pow _ n.succ_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_antisymm {a b : Int} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

Proof state:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : b + ↑(m + n) = b
⊢ a = b

Tactic:
have := Int.ofNat.inj <| Int.add_left_cancel <| this.trans (Int.add_zero _).symm

Result:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this✝ : b + ↑(m + n) = b
this : m + n = 0
⊢ a = b

Proof state:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this✝ : b + ↑(m + n) = b
this : m + n = 0
⊢ a = b

Tactic:
rw [← hn, Nat.eq_zero_of_add_eq_zero_left this, ofNat_zero, Int.add_zero a]

Result:
no goals

Proof state:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
⊢ a = b

Tactic:
let ⟨n, hn⟩ := le.dest h₁

Result:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
⊢ a = b

Proof state:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
⊢ a = b

Tactic:
have := hn

Result:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : a + ↑n = b
⊢ a = b

Proof state:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : a + ↑n = b
⊢ a = b

Tactic:
rw [← hm, Int.add_assoc, ← ofNat_add] at this

Result:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
this : b + ↑(m + n) = b
⊢ a = b

Proof state:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
⊢ a = b

Tactic:
let ⟨m, hm⟩ := le.dest h₂

Result:
a b : Int
h₁ : a ≤ b
h₂ : b ≤ a
n : Nat
hn : a + ↑n = b
m : Nat
hm : b + ↑m = a
⊢ a = b
-- Mathlib/Topology/StoneCech.lean
theorem denseRange_stoneCechUnit : DenseRange (stoneCechUnit : α → StoneCech α)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ Function.Surjective t2Quotient.mk

Tactic:
exact Quot.mk_surjective

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
this : Function.Surjective t2Quotient.mk
⊢ DenseRange fun x => ⟦preStoneCechUnit x⟧

Tactic:
exact this.denseRange.comp denseRange_preStoneCechUnit continuous_coinduced_rng

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ DenseRange stoneCechUnit

Tactic:
unfold stoneCechUnit t2Quotient.mk

Result:
α : Type u
inst✝ : TopologicalSpace α
⊢ DenseRange fun x => ⟦preStoneCechUnit x⟧

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ DenseRange fun x => ⟦preStoneCechUnit x⟧

Tactic:
have : Function.Surjective (t2Quotient.mk : PreStoneCech α → StoneCech α) := by
  exact Quot.mk_surjective

Result:
α : Type u
inst✝ : TopologicalSpace α
this : Function.Surjective t2Quotient.mk
⊢ DenseRange fun x => ⟦preStoneCechUnit x⟧
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_is_product {c : BinaryFan X Y} (h : Limits.IsLimit c) (t : IsTerminal Z) :
    IsPullback c.fst c.snd (t.from _) (t.from _) :=
  of_isLimit
    (isPullbackOfIsTerminalIsProduct _ _ _ _ t
      (IsLimit.ofIsoLimit h
        (Limits.Cones.ext (Iso.refl c.pt)
          (by
            rintro ⟨⟨⟩⟩ <;>
              · dsimp
                simp))))

Proof state:
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.π.app { as := WalkingPair.right } =
    (Iso.refl c.pt).hom ≫
      (BinaryFan.mk (c.π.1 { as := WalkingPair.left }) (c.π.1 { as := WalkingPair.right })).π.app
        { as := WalkingPair.right }

Tactic:
dsimp

Result:
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.snd = 𝟙 c.pt ≫ c.snd

Proof state:
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
c : BinaryFan X Y
h : IsLimit c
t : IsTerminal Z
⊢ c.snd = 𝟙 c.pt ≫ c.snd

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem norm_id_of_nontrivial_seminorm (h : ∃ x : E, ‖x‖ ≠ 0) : ‖id 𝕜 E‖ = 1 :=
  le_antisymm norm_id_le <| by
    let ⟨x, hx⟩ := h
    have := (id 𝕜 E).ratio_le_opNorm x
    rwa [id_apply, div_self hx] at this

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
this : ‖(id 𝕜 E) x‖ / ‖x‖ ≤ ‖id 𝕜 E‖
⊢ 1 ≤ ‖id 𝕜 E‖

Tactic:
rwa [id_apply, div_self hx] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ∃ x, ‖x‖ ≠ 0
⊢ 1 ≤ ‖id 𝕜 E‖

Tactic:
let ⟨x, hx⟩ := h

Result:
𝕜 : Type u_1
E : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id 𝕜 E‖

Proof state:
𝕜 : Type u_1
E : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id 𝕜 E‖

Tactic:
have := (id 𝕜 E).ratio_le_opNorm x

Result:
𝕜 : Type u_1
E : Type u_4
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
this : ‖(id 𝕜 E) x‖ / ‖x‖ ≤ ‖id 𝕜 E‖
⊢ 1 ≤ ‖id 𝕜 E‖
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Hom.cast_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) :
    HEq (e.cast hu hv) e

Proof state:
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ HEq (cast ⋯ ⋯ e) e

Tactic:
rfl

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ HEq (cast hu hv e) e

Tactic:
subst_vars

Result:
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ HEq (cast ⋯ ⋯ e) e
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.zero_beq_or_iff (a b : BitVec w) : (0#w == a ||| b) = (a == 0#w && b == 0#w)

Proof state:
w : Nat
a b : BitVec w
⊢ (0#w == a ||| b) = (a == 0#w && b == 0#w)

Tactic:
rw [Bool.eq_iff_iff, beq_iff_eq, Eq.comm]

Result:
w : Nat
a b : BitVec w
⊢ a ||| b = 0#w ↔ (a == 0#w && b == 0#w) = true

Proof state:
w : Nat
a b : BitVec w
⊢ a ||| b = 0#w ↔ (a == 0#w && b == 0#w) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_div_sin_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖

Tactic:
rw [← neg_ne_zero] at h0

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖

Tactic:
rw [sub_eq_add_neg, ← norm_neg, norm_div_sin_angle_add_of_inner_eq_zero h h0]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma contMDiffWithinAt_mpullbackWithin_extChartAt_symm
    {V : Π (x : M), TangentSpace I x}
    (hV : ContMDiffWithinAt I I.tangent m (fun x ↦ (V x : TangentBundle I M)) s x)
    (hs : UniqueMDiffOn I s) (hx : x ∈ s) (hmn : m + 1 ≤ n) :
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
      (fun y ↦ (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I) y :
        TangentBundle 𝓘(𝕜, E) E))
      ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
  ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq' hV
    (contMDiffWithinAt_extChartAt_symm_range (n := n) _ (mem_extChartAt_target x))
    (isInvertible_mfderivWithin_extChartAt_symm (mem_extChartAt_target x))
    (by simp [hx]) (UniqueMDiffOn.uniqueMDiffOn_target_inter hs x) hmn
    ((mapsTo_preimage _ _).mono_left inter_subset_right).preimage_mem_nhdsWithin
    (Subset.trans inter_subset_left (extChartAt_target_subset_range x)) (extChartAt_to_inv x)

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁷ : TopologicalSpace H
E : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
s : Set M
x : M
m n : WithTop ℕ∞
inst✝² : IsManifold I n M
inst✝¹ : CompleteSpace E
inst✝ : IsManifold I 1 M
V : (x : M) → TangentSpace I x
hV : ContMDiffWithinAt I I.tangent m (fun x => { proj := x, snd := V x }) s x
hs : UniqueMDiffOn I s
hx : x ∈ s
hmn : m + 1 ≤ n
⊢ ↑(extChartAt I x) x ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma fin3_def (P : Fin 3 → R) : ![P x, P y, P z] = P

Proof state:
R : Type r
P : Fin 3 → R
⊢ ![P x, P y, P z] = P

Tactic:
ext n

Result:
case h
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n

Proof state:
case h
R : Type r
P : Fin 3 → R
n : Fin (Nat.succ 0).succ.succ
⊢ ![P x, P y, P z] n = P n

Tactic:
fin_cases n <;> rfl

Result:
no goals
-- Mathlib/Data/Set/Monotone.lean
lemma strictMonoOn_insert_iff [Preorder α] [Preorder β] {f : α → β} {s : Set α} {a : α} :
    StrictMonoOn f (insert a s) ↔
       (∀ b ∈ s, b < a → f b < f a) ∧ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
⊢ StrictMonoOn f (insert a s) ↔ (∀ b ∈ s, b < a → f b < f a) ∧ (∀ b ∈ s, a < b → f a < f b) ∧ StrictMonoOn f s

Tactic:
simp [StrictMonoOn, forall_and]

Result:
no goals
-- Mathlib/Data/Nat/Size.lean
theorem shiftLeft'_tt_ne_zero (m) : ∀ {n}, (n ≠ 0) → shiftLeft' true m n ≠ 0
  | 0, h => absurd rfl h
  | succ _, _ => by dsimp [shiftLeft', bit]; omega

Proof state:
m n✝ : ℕ
x✝ : n✝.succ ≠ 0
⊢ ¬2 * shiftLeft' true m n✝ + 1 = 0

Tactic:
omega

Result:
no goals

Proof state:
m n✝ : ℕ
x✝ : n✝.succ ≠ 0
⊢ shiftLeft' true m n✝.succ ≠ 0

Tactic:
dsimp [shiftLeft', bit]

Result:
m n✝ : ℕ
x✝ : n✝.succ ≠ 0
⊢ ¬2 * shiftLeft' true m n✝ + 1 = 0
-- Mathlib/Order/CountableDenseLinearOrder.lean
theorem embedding_from_countable_to_dense [Countable α] [DenselyOrdered β] [Nontrivial β] :
    Nonempty (α ↪o β)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
val✝ : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯
⊢ Nonempty (α ↪o β)

Tactic:
refine
  ⟨RelEmbedding.trans (OrderEmbedding.ofStrictMono (fun a ↦ (F a).val) fun a₁ a₂ ↦ ?_)
      (OrderEmbedding.subtype _)⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
val✝ : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯
a₁ a₂ : α
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
⊢ Nonempty (α ↪o β)

Tactic:
cases nonempty_encodable α

Result:
case intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
val✝ : Encodable α
⊢ Nonempty (α ↪o β)

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
val✝ : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂

Tactic:
rcases (F a₂).prop with ⟨g, hg, ha₂⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : Countable α
inst✝¹ : DenselyOrdered β
inst✝ : Nontrivial β
val✝ : Encodable α
x y : β
hxy : x < y
a : β
ha : x < a ∧ a < y
this : Nonempty ↑(Set.Ioo x y)
our_ideal : Ideal (PartialIso α ↑(Set.Ioo x y)) := idealOfCofinals default (definedAtLeft ↑(Set.Ioo x y))
F : (a : α) → { b // ∃ f ∈ our_ideal, (a, b) ∈ ↑f } := fun a => funOfIdeal a our_ideal ⋯
a₁ a₂ : α
f : PartialIso α ↑(Set.Ioo x y)
hf : f ∈ our_ideal
ha₁ : (a₁, ↑(F a₁)) ∈ ↑f
g : PartialIso α ↑(Set.Ioo x y)
hg : g ∈ our_ideal
ha₂ : (a₂, ↑(F a₂)) ∈ ↑g
⊢ a₁ < a₂ → (fun a => ↑(F a)) a₁ < (fun a => ↑(F a)) a₂