harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Equiv/Fin.lean
@[simp] lemma Equiv.coe_embeddingFinSucc_symm {n : ℕ} {ι : Type*}
    (f : Σ (e : Fin n ↪ ι), {i // i ∉ Set.range e}) :
    ((Equiv.embeddingFinSucc n ι).symm f : Fin (n + 1) → ι) = Fin.cons f.2.1 f.1

Proof state:
n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }
⊢ ⇑((embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst

Tactic:
ext i

Result:
case h
n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }
i : Fin (n + 1)
⊢ ((embeddingFinSucc n ι).symm f) i = Fin.cons (↑f.snd) (⇑f.fst) i

Proof state:
case h
n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }
i : Fin (n + 1)
⊢ ((embeddingFinSucc n ι).symm f) i = Fin.cons (↑f.snd) (⇑f.fst) i

Tactic:
exact Fin.cases rfl (fun j ↦ rfl) i

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem getLast_filterMap (f : α → Option β) (l : List α) (h) :
    (l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none])

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
h : filterMap f l ≠ []
⊢ (filterMap f l).getLast h = (findSome? f l.reverse).get ⋯

Tactic:
simp [getLast_eq_iff_getLast_eq_some]

Result:
no goals

Proof state:
α : Type ?u.21922
β : Type ?u.21919
f : α → Option β
l : List α
h : filterMap f l ≠ []
⊢ (findSome? f l.reverse).isSome = true

Tactic:
simp_all [Option.isSome_iff_ne_none]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.Quot_mk_eq_mk (I : (FractionalIdeal R⁰ (FractionRing R))ˣ) :
    Quot.mk _ I = ClassGroup.mk I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I = mk I

Tactic:
rw [ClassGroup.mk, canonicalEquiv_self, RingEquiv.coe_monoidHom_refl, Units.map_id]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I =
    ((QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range).comp
        (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ))
      I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I = ↑I

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I)

Tactic:
rw [MonoidHom.id_apply, QuotientGroup.mk'_apply]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I = ↑I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I =
    ((QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range).comp
        (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ))
      I

Tactic:
erw [MonoidHom.comp_apply]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem size_assignments_insertRupUnits {n : Nat} (f : DefaultFormula n)
    (units : CNF.Clause (PosFin n)) :
    (f.insertRupUnits units).1.assignments.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst.size = f.assignments.size

Tactic:
exact size_insertUnit_fold f.rupUnits f.assignments false

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (f.insertRupUnits units).fst.assignments.size = f.assignments.size

Tactic:
simp only [insertRupUnits]

Result:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst.size = f.assignments.size
-- Mathlib/Topology/Exterior.lean
@[simp] lemma exterior_subset_exterior_iff_nhdsSet : exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t

Tactic:
simp (config := {contextual := true}) only [subset_exterior_iff, (hasBasis_nhdsSet _).ge_iff,
  and_imp, IsOpen.mem_nhdsSet, IsOpen.exterior_subset]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
lemma mem_sInf {S : Set (TwoSidedIdeal R)} {x : R} :
    x ∈ sInf S ↔ ∀ I ∈ S, x ∈ I :=
  show (∀ _, _) ↔ _ by simp [mem_iff]

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
S : Set (TwoSidedIdeal R)
x : R
⊢ (∀ x_1 ∈ ringCon '' S, x_1 x 0) ↔ ∀ I ∈ S, x ∈ I

Tactic:
simp [mem_iff]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem Sorted.rel_of_mem_take_of_mem_drop {l : List α} (h : List.Sorted r l) {k : ℕ} {x y : α}
    (hx : x ∈ List.take k l) (hy : y ∈ List.drop k l) : r x y

Proof state:
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k : ℕ
x y : α
hx : x ∈ take k l
hy : y ∈ drop k l
⊢ r x y

Tactic:
obtain ⟨iy, hiy, rfl⟩ := getElem_of_mem hy

Result:
case intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k : ℕ
x : α
hx : x ∈ take k l
iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
⊢ r x (drop k l)[iy]

Proof state:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
ix : ℕ
hix : ix < (take k l).length
hx : (take k l)[ix] ∈ take k l
⊢ r (take k l)[ix] (drop k l)[iy]

Tactic:
rw [getElem_take, getElem_drop]

Result:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
ix : ℕ
hix : ix < (take k l).length
hx : (take k l)[ix] ∈ take k l
⊢ r l[ix] l[k + iy]

Proof state:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
ix : ℕ
hix : ix < (take k l).length
hx : (take k l)[ix] ∈ take k l
⊢ r l[ix] l[k + iy]

Tactic:
rw [length_take] at hix

Result:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
ix : ℕ
hix✝ : ix < (take k l).length
hix : ix < k ⊓ l.length
hx : (take k l)[ix] ∈ take k l
⊢ r l[ix] l[k + iy]

Proof state:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
ix : ℕ
hix✝ : ix < (take k l).length
hix : ix < k ⊓ l.length
hx : (take k l)[ix] ∈ take k l
⊢ r l[ix] l[k + iy]

Tactic:
exact h.rel_get_of_lt (Nat.lt_add_right _ (Nat.lt_min.mp hix).left)

Result:
no goals

Proof state:
case intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k : ℕ
x : α
hx : x ∈ take k l
iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
⊢ r x (drop k l)[iy]

Tactic:
obtain ⟨ix, hix, rfl⟩ := getElem_of_mem hx

Result:
case intro.intro.intro.intro
α : Type u
r : α → α → Prop
l : List α
h : Sorted r l
k iy : ℕ
hiy : iy < (drop k l).length
hy : (drop k l)[iy] ∈ drop k l
ix : ℕ
hix : ix < (take k l).length
hx : (take k l)[ix] ∈ take k l
⊢ r (take k l)[ix] (drop k l)[iy]
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_le_of_mem_closedBall' (h : b ∈ closedBall a r) : ‖b‖ ≤ ‖a‖ + r :=
  (norm_le_norm_add_norm_div' _ _).trans <| add_le_add_left (by rwa [← dist_eq_norm_div]) _

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
h : b ∈ closedBall a r
⊢ ‖b / a‖ ≤ r

Tactic:
rwa [← dist_eq_norm_div]

Result:
no goals
-- Mathlib/Algebra/Module/Lattice.lean
@[simp]
lemma _root_.Basis.extendOfIsLattice_apply [IsFractionRing R K] {κ : Type*}
    {M : Submodule R V} [IsLattice K M] (b : Basis κ R M) (k : κ) :
    b.extendOfIsLattice K k = (b k).val

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
K : Type u_2
inst✝⁷ : Field K
inst✝⁶ : Algebra R K
V : Type u_3
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : Module R V
inst✝² : IsScalarTower R K V
inst✝¹ : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst✝ : IsLattice K M
b : Basis κ R ↥M
k : κ
⊢ (Basis.extendOfIsLattice K b) k = ↑(b k)

Tactic:
simp [Basis.extendOfIsLattice]

Result:
no goals
-- Mathlib/Topology/Constructible.lean
lemma IsConstructible.isLocallyConstructible (hs : IsConstructible s) : IsLocallyConstructible s :=
  fun _ ↦ ⟨univ, by simp, by simp,
    (isConstructible_preimage_iff_of_isOpenEmbedding isOpen_univ.isOpenEmbedding_subtypeVal
      (by simp) (by simp)).2 hs⟩

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsOpen univ

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsRetrocompact (range Subtype.val)

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ univ ∈ 𝓝 x✝

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ s ⊆ range Subtype.val

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Hadamard.lean
theorem hadamard_one : M ⊙ (1 : Matrix n n α) = diagonal fun i => M i i

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j

Tactic:
by_cases h : i = j <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
⊢ M ⊙ 1 = diagonal fun i => M i i

Tactic:
ext i j

Result:
case a
α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (M ⊙ 1) i j = diagonal (fun i => M i i) i j
-- Mathlib/SetTheory/ZFC/Basic.lean
lemma Definable₁.out_equiv (f : ZFSet.{u} → ZFSet.{u}) [Definable₁ f]
    {x y : PSet} (h : x ≈ y) :
    out f x ≈ out f y :=
  Definable.out_equiv _ (by simp [h])

Proof state:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : PSet.{u}
h : x ≈ y
⊢ ∀ (i : Fin (Nat.succ 0)), ![x] i ≈ ![y] i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_const_of_cdf [CompleteSpace E] [IsFiniteMeasure μ] (c : E) :
    ∫ _ in a..b, c ∂μ = ((μ (Iic b)).toReal - (μ (Iic a)).toReal) • c

Proof state:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = ∫ (x : ℝ) in Iic b, c ∂μ - ∫ (x : ℝ) in Iic a, c ∂μ

Tactic:
refine (integral_Iic_sub_Iic ?_ ?_).symm <;>
  simp only [integrableOn_const, measure_lt_top, or_true]

Result:
no goals

Proof state:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = ((μ (Iic b)).toReal - (μ (Iic a)).toReal) • c

Tactic:
simp only [sub_smul, ← setIntegral_const]

Result:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = ∫ (x : ℝ) in Iic b, c ∂μ - ∫ (x : ℝ) in Iic a, c ∂μ
-- Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean
theorem discr_ne_zero : discr K ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ discr K ≠ 0

Tactic:
rw [← (Int.cast_injective (α := ℚ)).ne_iff, coe_discr]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Algebra.discr ℚ ⇑(integralBasis K) ≠ ↑0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Algebra.discr ℚ ⇑(integralBasis K) ≠ ↑0

Tactic:
exact Algebra.discr_not_zero_of_basis ℚ (integralBasis K)

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem prime_dvd_of_eq_neg_one {p : ℕ} [Fact p.Prime] {a : ℤ} (h : legendreSym p a = -1) {x y : ℤ}
    (hxy : (p : ℤ) ∣ x ^ 2 - a * y ^ 2) : ↑p ∣ x ∧ ↑p ∣ y

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑(x ^ 2 - a * y ^ 2) = 0
⊢ ↑x = 0 ∧ ↑y = 0

Tactic:
push_cast at hxy

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑x ^ 2 - ↑a * ↑y ^ 2 = 0
⊢ ↑x = 0 ∧ ↑y = 0

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑x ^ 2 - ↑a * ↑y ^ 2 = 0
⊢ ↑x = 0 ∧ ↑y = 0

Tactic:
exact eq_zero_mod_of_eq_neg_one h hxy

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y

Tactic:
simp_rw [← ZMod.intCast_zmod_eq_zero_iff_dvd] at hxy ⊢

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑(x ^ 2 - a * y ^ 2) = 0
⊢ ↑x = 0 ∧ ↑y = 0
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma Subgraph.Connected.induce_verts {H : G.Subgraph} (h : H.Connected) :
    (G.induce H.verts).Connected

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ (⊤.induce H.verts).Connected

Tactic:
exact h.mono le_induce_top_verts (by exact rfl)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts = (⊤.induce H.verts).verts

Tactic:
exact rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ (SimpleGraph.induce H.verts G).Connected

Tactic:
rw [connected_induce_iff]

Result:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ (⊤.induce H.verts).Connected
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem eq_of_sub_eq_zero {a b : Int} (h : a - b = 0) : a = b

Proof state:
a b : Int
h : a - b = 0
⊢ a = b

Tactic:
have : 0 + b = b := by rw [Int.zero_add]

Result:
a b : Int
h : a - b = 0
this : 0 + b = b
⊢ a = b

Proof state:
a b : Int
h : a - b = 0
⊢ 0 + b = b

Tactic:
rw [Int.zero_add]

Result:
no goals

Proof state:
a b : Int
h : a - b = 0
this : 0 + b = b
⊢ a - b + b = b

Tactic:
rwa [h]

Result:
no goals

Proof state:
a b : Int
h : a - b = 0
this✝ : 0 + b = b
this : a - b + b = b
⊢ a = b

Tactic:
rwa [Int.sub_eq_add_neg, Int.neg_add_cancel_right] at this

Result:
no goals

Proof state:
a b : Int
h : a - b = 0
this : 0 + b = b
⊢ a = b

Tactic:
have : a - b + b = b := by rwa [h]

Result:
a b : Int
h : a - b = 0
this✝ : 0 + b = b
this : a - b + b = b
⊢ a = b
-- Mathlib/Analysis/Convex/Visible.lean
lemma isVisible_comm : IsVisible 𝕜 s x y ↔ IsVisible 𝕜 s y x

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : AddTorsor V P
s : Set P
x y : P
⊢ IsVisible 𝕜 s x y ↔ IsVisible 𝕜 s y x

Tactic:
simp [IsVisible, sbtw_comm]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_zero (s : M) : IsLocalization.mk' S 0 s = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
s : ↥M
⊢ mk' S 0 s = 0

Tactic:
rw [eq_comm, IsLocalization.eq_mk'_iff_mul_eq, zero_mul, map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem admissible_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β → Prop)
    (hadm : admissible P) : admissible (fun (x : α ×' β) => P x.2)

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : β → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.snd) x
⊢ P (CCPO.csup c).snd

Tactic:
apply hadm _ (PProd.chain.chain_snd hchain)

Result:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : β → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.snd) x
⊢ ∀ (x : β), PProd.chain.snd c x → P x

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : β → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.snd) x
⊢ ∀ (x : β), PProd.chain.snd c x → P x

Tactic:
intro y ⟨x, hxy⟩

Result:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : β → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.snd) x
y : β
x : α
hxy : c ⟨x, y⟩
⊢ P y

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : β → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.snd) x
y : β
x : α
hxy : c ⟨x, y⟩
⊢ P y

Tactic:
apply h ⟨x,y⟩ hxy

Result:
no goals

Proof state:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : β → Prop
hadm : admissible P
⊢ admissible fun x => P x.snd

Tactic:
intro c hchain h

Result:
α : Sort u
β : Sort v
inst✝¹ : CCPO α
inst✝ : CCPO β
P : β → Prop
hadm : admissible P
c : α ×' β → Prop
hchain : chain c
h : ∀ (x : α ×' β), c x → (fun x => P x.snd) x
⊢ P (CCPO.csup c).snd
-- Mathlib/Topology/Basic.lean
/-- Interior and frontier are disjoint. -/
lemma disjoint_interior_frontier : Disjoint (interior s) (frontier s)

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ Disjoint (interior s) (frontier s)

Tactic:
rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
  ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Icc_right (f : ∀ i, α i) (i : ι) (b : α i) :
    update f i '' Icc (f i) b = Icc f (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Icc (f i) b = Icc f (update f i b)

Tactic:
simpa using image_update_Icc f i (f i) b

Result:
no goals
-- Mathlib/NumberTheory/GaussSum.lean
lemma mul_gaussSum_inv_eq_gaussSum (χ : MulChar R R') (ψ : AddChar R R') :
    χ (-1) * gaussSum χ ψ⁻¹ = gaussSum χ ψ

Proof state:
R : Type u
inst✝² : Field R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ χ (-1) * gaussSum χ ψ⁻¹ = gaussSum χ ψ

Tactic:
rw [ψ.inv_mulShift, ← Units.coe_neg_one]

Result:
R : Type u
inst✝² : Field R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = gaussSum χ ψ

Proof state:
R : Type u
inst✝² : Field R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = gaussSum χ ψ

Tactic:
exact gaussSum_mulShift χ ψ (-1)

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
@[to_additive] lemma mabs_mul_eq_mul_mabs_iff (a b : α) :
    |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b : α
⊢ mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
obtain ab | ab := le_total a b

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b : α
ab : a ≤ b
⊢ mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b : α
ab : b ≤ a
⊢ mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b : α
ab : a ≤ b
⊢ mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
exact mabs_mul_eq_mul_mabs_le ab

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b : α
ab : b ≤ a
⊢ mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem one_le_pow_of_le (ha : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n
  | 0 => by simp
  | k + 1 => by
    rw [pow_succ]
    exact one_le_mul (one_le_pow_of_le ha k) ha

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ k * a

Tactic:
exact one_le_mul (one_le_pow_of_le ha k) ha

Result:
no goals

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ (k + 1)

Tactic:
rw [pow_succ]

Result:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ k * a

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
⊢ 1 ≤ a ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Over.lean
lemma mem_over_iff {X : C} {Y : Over X} (S : Sieve Y) :
    S ∈ (J.over X) Y ↔ Sieve.overEquiv _ S ∈ J Y.left

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
⊢ S ∈ (J.over X) Y ↔ (Sieve.overEquiv Y) S ∈ J Y.left

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem eq_zero_cpow_iff {x : ℂ} {a : ℂ} : a = (0 : ℂ) ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
x a : ℂ
⊢ a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [← zero_cpow_eq_iff, eq_comm]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {f : β → ℝ≥0∞} {a : ℝ≥0∞}
    (ha : a ≠ ∞) : Tendsto f atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε) :=
  .trans (atTop_basis.tendsto_iff (hasBasis_nhds_of_ne_top ha)) (by simp only [true_and]; rfl)

Proof state:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)

Tactic:
rfl

Result:
no goals

Proof state:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)

Tactic:
simp only [true_and]

Result:
β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem Prime.eq_one_or_self_of_dvd {p : ℕ} (pp : p.Prime) (m : ℕ) (hm : m ∣ p) :
    m = 1 ∨ m = p

Proof state:
p : ℕ
pp : Prime p
m : ℕ
hm : m ∣ p
⊢ m = 1 ∨ m = p

Tactic:
obtain ⟨n, hn⟩ := hm

Result:
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ m = 1 ∨ m = p

Proof state:
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p

Tactic:
rw [hn, mul_one]

Result:
no goals

Proof state:
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ m = p

Tactic:
rw [Nat.isUnit_iff, Nat.isUnit_iff] at this

Result:
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ m = 1 ∨ m = p

Proof state:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ n = 1 → m = p

Tactic:
rintro rfl

Result:
p : ℕ
pp : Prime p
m : ℕ
hn : p = m * 1
this : m = 1 ∨ 1 = 1
⊢ m = p

Proof state:
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
⊢ m = 1 ∨ m = p

Tactic:
have := pp.isUnit_or_isUnit hn

Result:
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : IsUnit m ∨ IsUnit n
⊢ m = 1 ∨ m = p

Proof state:
case intro
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ m = 1 ∨ m = p

Tactic:
apply Or.imp_right _ this

Result:
p : ℕ
pp : Prime p
m n : ℕ
hn : p = m * n
this : m = 1 ∨ n = 1
⊢ n = 1 → m = p