harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Closed.lean
theorem topologyOfClosureOperator_close (c : ∀ X : C, ClosureOperator (Sieve X))
    (pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), c Y (S.pullback f) = (c X S).pullback f) (X : C)
    (S : Sieve X) : (topologyOfClosureOperator c pb).close S = c X S

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ((topologyOfClosureOperator c pb).close S).arrows f ↔ ((c X) S).arrows f

Tactic:
change c _ (Sieve.pullback f S) = ⊤ ↔ c _ S f

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ (c Y) (Sieve.pullback f S) = ⊤ ↔ ((c X) S).arrows f

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ (c Y) (Sieve.pullback f S) = ⊤ ↔ ((c X) S).arrows f

Tactic:
rw [pb, Sieve.mem_iff_pullback_eq_top]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
⊢ (topologyOfClosureOperator c pb).close S = (c X) S

Tactic:
ext Y f

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ((topologyOfClosureOperator c pb).close S).arrows f ↔ ((c X) S).arrows f
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_unique_of_nndist_ne_zero {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β]
    [FunLike F α β] [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : nndist x y ≠ 0)
    (hr : nndist (f x) (f y) = r * nndist x y) : r = ratio f :=
  ratio_unique (by rwa [edist_nndist, ENNReal.coe_ne_zero]) (edist_ne_top x y)
    (by rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul])

Proof state:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ edist x y ≠ 0

Tactic:
rwa [edist_nndist, ENNReal.coe_ne_zero]

Result:
no goals

Proof state:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (f x) (f y) = r * nndist x y
⊢ edist (f x) (f y) = ↑r * edist x y

Tactic:
rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem ne_mex {ι : Type u} (f : ι → Ordinal.{max u v}) : ∀ i, f i ≠ mex.{_, v} f

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ ∀ (i : ι), f i ≠ mex f

Tactic:
simpa using mex_not_mem_range.{_, v} f

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
/-- If the distances between distinct points in a (pseudo) metric space
are uniformly bounded away from zero, then the space has discrete topology. -/
lemma DiscreteTopology.of_forall_le_dist {α} [PseudoMetricSpace α] {r : ℝ} (hpos : 0 < r)
    (hr : Pairwise (r ≤ dist · · : α → α → Prop)) : DiscreteTopology α :=
  ⟨by rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]⟩

Proof state:
α : Type u_3
inst✝ : PseudoMetricSpace α
r : ℝ
hpos : 0 < r
hr : Pairwise fun x1 x2 => r ≤ dist x1 x2
⊢ UniformSpace.toTopologicalSpace = ⊥

Tactic:
rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem ConcaveOn.le_map_integral [IsProbabilityMeasure μ] (hg : ConcaveOn ℝ s g)
    (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ)
    (hgi : Integrable (g ∘ f) μ) : (∫ x, g (f x) ∂μ) ≤ g (∫ x, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst✝ : IsProbabilityMeasure μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ ∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)

Tactic:
simpa only [average_eq_integral] using hg.le_map_average hgc hsc hfs hfi hgi

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem op_smul_one_eq_diagonal [DecidableEq m] (a : α) :
    MulOpposite.op a • (1 : Matrix m m α) = diagonal fun _ => a

Proof state:
m : Type u_2
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq m
a : α
⊢ MulOpposite.op a • 1 = diagonal fun x => a

Tactic:
simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]

Result:
no goals
-- Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
theorem wellFounded
    {r : α → α → Prop} [IsTrichotomous α r] (hr : WellFounded (Function.swap r))
    {s : ℕ → ℕ → Prop} (hs : WellFounded s) (hs0 : ∀ ⦃n⦄, ¬ s n 0) :
    WellFounded (Finsupp.DegLex r s)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
⊢ WellFounded (Finsupp.DegLex r s)

Tactic:
have wft := WellFounded.prod_lex hs (Finsupp.Lex.wellFounded' hs0 hs hr)

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : WellFounded (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Finsupp.DegLex r s)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Function.onFun (Prod.Lex s (Finsupp.Lex r s)) fun x => (x.degree, x))

Tactic:
rw [← Set.wellFoundedOn_range]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ (Set.range fun x => (x.degree, x)).WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ (Set.range fun x => (x.degree, x)).WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))

Tactic:
exact Set.WellFoundedOn.mono wft (le_refl _) (fun _ _ ↦ trivial)

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Finsupp.DegLex r s)

Tactic:
unfold Finsupp.DegLex

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Function.onFun (Prod.Lex s (Finsupp.Lex r s)) fun x => (x.degree, x))

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : WellFounded (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Finsupp.DegLex r s)

Tactic:
rw [← Set.wellFoundedOn_univ] at wft

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsTrichotomous α r
hr : WellFounded (Function.swap r)
s : ℕ → ℕ → Prop
hs : WellFounded s
hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0
wft : Set.univ.WellFoundedOn (Prod.Lex s (Finsupp.Lex r s))
⊢ WellFounded (Finsupp.DegLex r s)
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem rel_flip_eq {s t : Multiset α} : Rel (fun a b => b = a) s t ↔ s = t :=
  show Rel (flip (· = ·)) s t ↔ s = t by rw [rel_flip, rel_eq, eq_comm]

Proof state:
α : Type u_1
s t : Multiset α
⊢ Rel (flip fun x1 x2 => x1 = x2) s t ↔ s = t

Tactic:
rw [rel_flip, rel_eq, eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isZero₂_of_isZero₁₃ (h₁ : IsZero T.obj₁) (h₃ : IsZero T.obj₃) : IsZero T.obj₂

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : IsZero T.obj₁
h₃ : IsZero T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0

Tactic:
exact ⟨h₁.eq_of_src _ _, h₃.eq_of_tgt _ _⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : IsZero T.obj₁
h₃ : IsZero T.obj₃
⊢ IsZero T.obj₂

Tactic:
rw [T.isZero₂_iff hT]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : IsZero T.obj₁
h₃ : IsZero T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0
-- Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
lemma isoClosure_eq_self [IsClosedUnderIsomorphisms P] : isoClosure P = P

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure = P

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure ≤ P

case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.isoClosure ≤ P

Tactic:
intro X ⟨Y, hY, ⟨e⟩⟩

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X Y : C
hY : P Y
e : X ≅ Y
⊢ P X

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P ≤ P.isoClosure

Tactic:
exact le_isoClosure P

Result:
no goals

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
X Y : C
hY : P Y
e : X ≅ Y
⊢ P X

Tactic:
exact prop_of_iso P e.symm hY

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem Nodup.mem_erase_iff [LawfulBEq α] {a : α} (d : Nodup l) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
l : List α
b : α
inst✝ : LawfulBEq α
a : α
d : l.Nodup
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Tactic:
rw [Nodup.erase_eq_filter d, mem_filter, and_comm, bne_iff_ne]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.isOpenMap_iff {β} [TopologicalSpace β] {B : Set (Set α)}
    (hB : IsTopologicalBasis B) {f : α → β} : IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)

Proof state:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
⊢ IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)

Tactic:
refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩

Result:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (f '' o)

Proof state:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (⋃ i, f '' ↑i)

Tactic:
exact isOpen_iUnion fun s => hf s s.2.1

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (f '' o)

Tactic:
rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]

Result:
α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (⋃ i, f '' ↑i)
-- Mathlib/Algebra/Order/SuccPred.lean
lemma strictMono_of_lt_add_one : (∀ a, ¬ IsMax a → f a < f (a + 1)) → StrictMono f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
f : α → β
⊢ (∀ (a : α), ¬IsMax a → f a < f (a + 1)) → StrictMono f

Tactic:
simpa [Order.succ_eq_add_one] using strictMono_of_lt_succ (f := f)

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem zipWith_flip (f : α → β → γ) : ∀ as bs, zipWith (flip f) bs as = zipWith f as bs
  | [], [] => rfl
  | [], _ :: _ => rfl
  | _ :: _, [] => rfl
  | a :: as, b :: bs => by
    simp! [zipWith_flip]
    rfl

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ flip f b a = f a b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ zipWith (flip f) (b :: bs) (a :: as) = zipWith f (a :: as) (b :: bs)

Tactic:
simp! [zipWith_flip]

Result:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
as : List α
b : β
bs : List β
⊢ flip f b a = f a b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
theorem blastShiftRight.go_decl_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
    (acc : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
        (go aig distance curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isTrue.h2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
res : AIG.RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size
⊢ idx✝ < (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftRight.twoPowShift)

Result:
case isTrue.h2.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
res : AIG.RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size
⊢ idx✝ < aig.decls.size
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_half_period_eq : ‖(↑(p / 2) : AddCircle p)‖ = |p| / 2

Proof state:
case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2

Tactic:
rw [norm_eq, ← mul_div_assoc, inv_mul_cancel₀ hp, one_div, round_two_inv, Int.cast_one,
  one_mul, (by linarith : p / 2 - p = -(p / 2)), abs_neg, abs_div, abs_two]

Result:
no goals

Proof state:
p : ℝ
⊢ ‖↑(p / 2)‖ = |p| / 2

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Result:
case inl

⊢ ‖↑(0 / 2)‖ = |0| / 2

case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2

Proof state:
case inl

⊢ ‖↑(0 / 2)‖ = |0| / 2

Tactic:
simp

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ p / 2 - p = -(p / 2)

Tactic:
linarith

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem quadratic_reciprocity_three_mod_four {a b : ℕ} (ha : a % 4 = 3) (hb : b % 4 = 3) :
    J(a | b) = -J(b | a)

Proof state:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
⊢ J(↑a | b) = -J(↑b | a)

Tactic:
let nop := @neg_one_pow_div_two_of_three_mod_four

Result:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ J(↑a | b) = -J(↑b | a)

Proof state:
a b : ℕ
ha : a % 4 = 3
hb : b % 4 = 3
nop : ∀ {n : ℕ}, n % 4 = 3 → (-1) ^ (n / 2) = -1 := @neg_one_pow_div_two_of_three_mod_four
⊢ J(↑a | b) = -J(↑b | a)

Tactic:
rw [quadratic_reciprocity, pow_mul, nop ha, nop hb, neg_one_mul] <;>
  rwa [odd_iff, odd_of_mod_four_eq_three]

Result:
no goals
-- Mathlib/Data/Matrix/Diagonal.lean
theorem diagonal_map [Zero α] [Zero β] {f : α → β} (h : f 0 = 0) {d : n → α} :
    (diagonal d).map f = diagonal fun m => f (d m)

Proof state:
case a
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
⊢ (diagonal d).map f i✝ j✝ = diagonal (fun m => f (d m)) i✝ j✝

Tactic:
simp only [diagonal_apply, map_apply]

Result:
case a
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
⊢ f (if i✝ = j✝ then d i✝ else 0) = if i✝ = j✝ then f (d i✝) else 0

Proof state:
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
⊢ (diagonal d).map f = diagonal fun m => f (d m)

Tactic:
ext

Result:
case a
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
⊢ (diagonal d).map f i✝ j✝ = diagonal (fun m => f (d m)) i✝ j✝

Proof state:
case a
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
⊢ f (if i✝ = j✝ then d i✝ else 0) = if i✝ = j✝ then f (d i✝) else 0

Tactic:
split_ifs <;> simp [h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem repr_symm_single [DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (i : ι) :
    b.repr.symm (lp.single 2 i (1 : 𝕜)) = b i

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq ι
b : HilbertBasis ι 𝕜 E
i : ι
⊢ b.repr.symm (lp.single 2 i 1) = b i

Tactic:
dsimp [instFunLike]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq ι
b : HilbertBasis ι 𝕜 E
i : ι
⊢ b.repr.symm (lp.single 2 i 1) = b.repr.symm (lp.single 2 i 1)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : DecidableEq ι
b : HilbertBasis ι 𝕜 E
i : ι
⊢ b.repr.symm (lp.single 2 i 1) = b.repr.symm (lp.single 2 i 1)

Tactic:
convert rfl

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem leadingCoeff_eq_iff {x : HahnSeries Γ R} : x.leadingCoeff = 0 ↔ x = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x ≠ 0 → x.leadingCoeff ≠ 0

Tactic:
exact fun hx => (leadingCoeff_of_ne hx) ▸ coeff_orderTop_ne (orderTop_of_ne hx)

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.leadingCoeff = 0 ↔ x = 0

Tactic:
refine { mp := ?_, mpr := fun hx => hx ▸ leadingCoeff_zero }

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.leadingCoeff = 0 → x = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.leadingCoeff = 0 → x = 0

Tactic:
contrapose!

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x ≠ 0 → x.leadingCoeff ≠ 0
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem antidiagonal.snd_le {n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) : kl.2 ≤ n

Proof state:
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ kl.2 ≤ n

Tactic:
rw [le_iff_exists_add]

Result:
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.2 + c

Proof state:
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ ∃ c, n = kl.2 + c

Tactic:
use kl.1

Result:
case h
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ n = kl.2 + kl.1

Proof state:
case h
A : Type u_1
inst✝² : OrderedAddCommMonoid A
inst✝¹ : CanonicallyOrderedAdd A
inst✝ : HasAntidiagonal A
n : A
kl : A × A
hlk : kl ∈ antidiagonal n
⊢ n = kl.2 + kl.1

Tactic:
rwa [mem_antidiagonal, eq_comm, add_comm] at hlk

Result:
no goals
-- Mathlib/Topology/Separation/GDelta.lean
theorem IsGδ.singleton [FirstCountableTopology X] [T1Space X] (x : X) :
    IsGδ ({x} : Set X)

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
⊢ IsGδ {x}

Tactic:
rcases (nhds_basis_opens x).exists_antitone_subbasis with ⟨U, hU, h_basis⟩

Result:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i => U i
⊢ IsGδ {x}

Proof state:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i => U i
⊢ IsGδ (⋂ i, ⋂ (_ : True), U i)

Tactic:
exact .biInter (to_countable _) fun n _ => (hU n).2.isGδ

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i => U i
⊢ IsGδ {x}

Tactic:
rw [← biInter_basis_nhds h_basis.toHasBasis]

Result:
case intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
inst✝ : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun i => U i
⊢ IsGδ (⋂ i, ⋂ (_ : True), U i)
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem support_subset [DecidableEq ι] [DecidableEq M] (A : ι → S) (x : DirectSum ι fun i => A i) :
    (Function.support fun i => (x i : M)) ⊆ ↑(DFinsupp.support x)

Proof state:
ι : Type v
M : Type u_1
S : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike S M
inst✝² : AddSubmonoidClass S M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ (support fun i => ↑(x i)) ⊆ ↑(DFinsupp.support x)

Tactic:
intro m

Result:
ι : Type v
M : Type u_1
S : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike S M
inst✝² : AddSubmonoidClass S M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)

Proof state:
ι : Type v
M : Type u_1
S : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : SetLike S M
inst✝² : AddSubmonoidClass S M
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
m : ι
⊢ (m ∈ support fun i => ↑(x i)) → m ∈ ↑(DFinsupp.support x)

Tactic:
simp only [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not,
  ZeroMemClass.coe_eq_zero, imp_self]

Result:
no goals