harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfcHom_eq_of_continuous_of_map_id [UniqueHom R A]
    (φ : C(spectrum R a, R) →⋆ₐ[R] A) (hφ₁ : Continuous φ)
    (hφ₂ : φ (.restrict (spectrum R a) <| .id R) = a) : cfcHom ha = φ :=
  (cfcHom ha).ext_continuousMap a φ (cfcHom_isClosedEmbedding ha).continuous hφ₁ <| by
    rw [cfcHom_id ha, hφ₂]

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
φ : C(↑(spectrum R a), R) →⋆ₐ[R] A
hφ₁ : Continuous ⇑φ
hφ₂ : φ (restrict (spectrum R a) (ContinuousMap.id R)) = a
⊢ (cfcHom ha) (restrict (spectrum R a) (ContinuousMap.id R)) = φ (restrict (spectrum R a) (ContinuousMap.id R))

Tactic:
rw [cfcHom_id ha, hφ₂]

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
@[simp] lemma fwdDiff_smul_const {R : Type} [Ring R] [Module R G] (f : M → R) (g : G) :
    Δ_[h] (fun y ↦ f y • g) = Δ_[h] f • fun _ ↦ g

Proof state:
case h
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : G
y : M
⊢ Δ_[h] (fun y => f y • g) y = (Δ_[h] f • fun x => g) y

Tactic:
simp only [fwdDiff, Pi.smul_apply', sub_smul]

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : G
⊢ (Δ_[h] fun y => f y • g) = Δ_[h] f • fun x => g

Tactic:
ext y

Result:
case h
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type
inst✝¹ : Ring R
inst✝ : Module R G
f : M → R
g : G
y : M
⊢ Δ_[h] (fun y => f y • g) y = (Δ_[h] f • fun x => g) y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem splitAt_eq (n : Nat) (l : List α) : splitAt n l = (l.take n, l.drop n)

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ splitAt n l = (take n l, drop n l)

Tactic:
rw [splitAt, splitAt_go, reverse_nil, nil_append]

Result:
α : Type u_1
n : Nat
l : List α
⊢ (if n < l.length then (take n l, drop n l) else (l, [])) = (take n l, drop n l)

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (if n < l.length then (take n l, drop n l) else (l, [])) = (take n l, drop n l)

Tactic:
split <;> simp_all [take_of_length_le, drop_of_length_le]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem negAt_apply_isReal_and_mem (x : mixedSpace K) {w : {w // IsReal w}} (hw : w ∈ s) :
    (negAt s x).1 w = - x.1 w

Proof state:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ ((negAt s) x).1 w = -x.1 w

Tactic:
simp_rw [negAt, ContinuousLinearEquiv.prod_apply, piCongrRight_apply, if_pos hw,
  ContinuousLinearEquiv.neg_apply]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem toList_comp (p : Path a b) : ∀ {c} (q : Path b c), (p.comp q).toList = q.toList ++ p.toList
  | _, nil => by simp
  | _, @cons _ _ _ d _ q _ => by simp [toList_comp]

Proof state:
V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
x✝ d : V
q : Path b d
a✝ : d ⟶ x✝
⊢ (p.comp (q.cons a✝)).toList = (q.cons a✝).toList ++ p.toList

Tactic:
simp [toList_comp]

Result:
no goals

Proof state:
V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (p.comp nil).toList = nil.toList ++ p.toList

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).get? k' = if h : k == k' then
      (cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k)))
    else m.get? k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).get? k' = if h : (k == k') = true then cast ⋯ (f (m.get? k)) else m.get? k'

Tactic:
simp_to_raw using Raw₀.get?_alter

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β}
    (h : m.WF) : Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get!

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
k : α
inst✝ : Inhabited β
f : β → β
h : m.WF
⊢ get! (modify m k f) k = (Option.map f (get? m k)).get!

Tactic:
simp_to_raw using Raw₀.Const.get!_modify_self

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem mul_eq_mul_left {a b c : ℝ≥0} (h : a ≠ 0) : a * b = a * c ↔ b = c

Proof state:
a b c : ℝ≥0
h : a ≠ 0
⊢ a * b = a * c ↔ b = c

Tactic:
rw [mul_eq_mul_left_iff, or_iff_left h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isCharTwoJNeZeroNF_of_char_two : W.c₆ = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -1 ^ 3 - 864 * W.a₆ = 1

Tactic:
linear_combination (-1 - 432 * W.a₆) * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ W.c₆ = 1

Tactic:
rw [c₆_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ -1 ^ 3 - 864 * W.a₆ = 1
-- Mathlib/Data/Finset/Sort.lean
theorem orderEmbOfFin_apply (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) :
    s.orderEmbOfFin h i = (s.sort (· ≤ ·))[i]'(by rw [length_sort, h]; exact i.2) :=
  rfl

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < k

Tactic:
exact i.2

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < (sort (fun x1 x2 => x1 ≤ x2) s).length

Tactic:
rw [length_sort, h]

Result:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
i : Fin k
⊢ ↑i < k
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_apply {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j) :
    v.restrict i j = v (j ∩ i)

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑(v.restrict i) j = ↑v (j ∩ i)

Tactic:
rw [restrict, dif_pos hi]

Result:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (s ∩ i) else 0, empty' := ⋯, not_measurable' := ⋯,
          m_iUnion' := ⋯ }
      j =
    ↑v (j ∩ i)

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ↑v (s ∩ i) else 0, empty' := ⋯, not_measurable' := ⋯,
          m_iUnion' := ⋯ }
      j =
    ↑v (j ∩ i)

Tactic:
exact if_pos hj

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_const (c : ε) (hμ : μ ≠ 0) : eLpNormEssSup (fun _ : α => c) μ = ‖c‖ₑ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ε
hμ : μ ≠ 0
⊢ eLpNormEssSup (fun x => c) μ = ‖c‖ₑ

Tactic:
rw [eLpNormEssSup_eq_essSup_enorm, essSup_const _ hμ]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.mul_div_cancel'` for a stronger version. -/
protected lemma mul_div_cancel (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * (b / a) = b :=
  ENNReal.mul_div_cancel' (by simp [ha₀]) (by simp [ha])

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = ⊤ → b = 0

Tactic:
simp [ha]

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = 0 → b = 0

Tactic:
simp [ha₀]

Result:
no goals
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
**Mahler's theorem**: for any continuous function `f` from `ℤ_[p]` to a `p`-adic Banach space, the
Mahler series with coefficients `n ↦ Δ_[1]^[n] f 0` converges to the original function `f`.
-/
lemma hasSum_mahler (f : C(ℤ_[p], E)) : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] f 0) n) f

Proof state:
case h.e'_6
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n => mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0)
⊢ f = mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0

Tactic:
refine ContinuousMap.coe_injective (PadicInt.denseRange_natCast.equalizer
  (map_continuous f) (map_continuous _) (funext fun n ↦ ?_))

Result:
case h.e'_6
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n => mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0)
n : ℕ
⊢ (⇑f ∘ Nat.cast) n = (⇑(mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0) ∘ Nat.cast) n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n => mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0)
⊢ HasSum (fun n => mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) f

Tactic:
convert this using 1

Result:
case h.e'_6
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n => mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0)
⊢ f = mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0

Proof state:
case h.e'_6
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℚ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
f : C(ℤ_[p], E)
this : HasSum (fun n => mahlerTerm (Δ_[1]^[n] (⇑f) 0) n) (mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0)
n : ℕ
⊢ (⇑f ∘ Nat.cast) n = (⇑(mahlerSeries fun x => Δ_[1]^[x] (⇑f) 0) ∘ Nat.cast) n

Tactic:
simpa only [Function.comp_apply, mahlerSeries_apply_nat (fwdDiff_tendsto_zero f) le_rfl,
  zero_add, sum_apply, Pi.smul_apply, nsmul_one] using (shift_eq_sum_fwdDiff_iter 1 f n 0)

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem pair {f : α → β} {g : α → γ} (hf : Computable f) (hg : Computable g) :
    Computable fun a => (f a, g a) :=
  (hf.pair hg).of_eq fun n => by cases decode (α := α) n <;> simp [Seq.seq]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> (↑(decode n)).bind fun a => map encode (↑f a)) <*> (↑(decode n)).bind fun a => map encode (↑g a)) =
    (↑(decode n)).bind fun a => map encode ((↑fun a => (f a, g a)) a)

Tactic:
cases decode (α := α) n <;> simp [Seq.seq]

Result:
no goals
-- Mathlib/Algebra/Homology/Opposite.lean
@[simp]
lemma quasiIsoAt_opFunctor_map_iff
    {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
    [K.HasHomology i] [L.HasHomology i] :
    QuasiIsoAt ((opFunctor _ _).map φ.op) i ↔ QuasiIsoAt φ i

Proof state:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt ((opFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i

Tactic:
simp only [quasiIsoAt_iff]

Result:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor Vᵒᵖ c.symm i).map ((opFunctor V c).map φ.op)) ↔
    ShortComplex.QuasiIso ((shortComplexFunctor V c i).map φ)

Proof state:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor Vᵒᵖ c.symm i).map ((opFunctor V c).map φ.op)) ↔
    ShortComplex.QuasiIso ((shortComplexFunctor V c i).map φ)

Tactic:
exact ShortComplex.quasiIso_opMap_iff ((shortComplexFunctor V c i).map φ)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem coprime_zero_left (n : Nat) : Coprime 0 n ↔ n = 1

Proof state:
n : Nat
⊢ Coprime 0 n ↔ n = 1

Tactic:
simp [Coprime]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_congr' {B : Set ℕ} [DecidablePred (· ∈ B)]
    (h : ∀ n > 0, n ∈ A ↔ n ∈ B) : schnirelmannDensity A = schnirelmannDensity B

Proof state:
case e_s.h.mk.e_a.e_a.e_s
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩) = filter (fun a => a ∈ B) (Ioc 0 ↑⟨n, hn⟩)

Tactic:
ext x

Result:
case e_s.h.mk.e_a.e_a.e_s.h
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
x : ℕ
⊢ x ∈ filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩) ↔ x ∈ filter (fun a => a ∈ B) (Ioc 0 ↑⟨n, hn⟩)

Proof state:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ schnirelmannDensity A = schnirelmannDensity B

Tactic:
rw [schnirelmannDensity, schnirelmannDensity]

Result:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n = ⨅ n, ↑(#(filter (fun a => a ∈ B) (Ioc 0 ↑n))) / ↑↑n

Proof state:
case e_s
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) = fun n => ↑(#(filter (fun a => a ∈ B) (Ioc 0 ↑n))) / ↑↑n

Tactic:
ext ⟨n, hn⟩

Result:
case e_s.h.mk
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩))) / ↑↑⟨n, hn⟩ =
    ↑(#(filter (fun a => a ∈ B) (Ioc 0 ↑⟨n, hn⟩))) / ↑↑⟨n, hn⟩

Proof state:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n = ⨅ n, ↑(#(filter (fun a => a ∈ B) (Ioc 0 ↑n))) / ↑↑n

Tactic:
congr

Result:
case e_s
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) = fun n => ↑(#(filter (fun a => a ∈ B) (Ioc 0 ↑n))) / ↑↑n

Proof state:
case e_s.h.mk.e_a.e_a.e_s.h
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
x : ℕ
⊢ x ∈ filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩) ↔ x ∈ filter (fun a => a ∈ B) (Ioc 0 ↑⟨n, hn⟩)

Tactic:
aesop

Result:
no goals

Proof state:
case e_s.h.mk
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩))) / ↑↑⟨n, hn⟩ =
    ↑(#(filter (fun a => a ∈ B) (Ioc 0 ↑⟨n, hn⟩))) / ↑↑⟨n, hn⟩

Tactic:
congr 3

Result:
case e_s.h.mk.e_a.e_a.e_s
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
n : ℕ
hn : 0 < n
⊢ filter (fun a => a ∈ A) (Ioc 0 ↑⟨n, hn⟩) = filter (fun a => a ∈ B) (Ioc 0 ↑⟨n, hn⟩)
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
lemma natCast_add_one_cpow_ne_zero (n : ℕ) (z : ℂ) : (n + 1 : ℂ) ^ z ≠ 0 :=
  mt (cpow_eq_zero_iff ..).mp fun H ↦ by norm_cast at H; exact H.1

Proof state:
n : ℕ
z : ℂ
H : ↑n + 1 = 0 ∧ z ≠ 0
⊢ False

Tactic:
norm_cast at H

Result:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False

Proof state:
n : ℕ
z : ℂ
H : False ∧ ¬z = 0
⊢ False

Tactic:
exact H.1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sign_mul : ∀ a b, sign (a * b) = sign a * sign b
  | a, 0 | 0, b => by simp [Int.mul_zero, Int.zero_mul]
  | succ _, succ _ | succ _, -[_+1] | -[_+1], succ _ | -[_+1], -[_+1] => rfl

Proof state:
b : Int
⊢ (0 * b).sign = sign 0 * b.sign

Tactic:
simp [Int.mul_zero, Int.zero_mul]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem not_mem_range_coe_iff {x : OnePoint X} : x ∉ range some ↔ x = ∞

Proof state:
X : Type u_1
x : OnePoint X
⊢ x ∉ range some ↔ x = ∞

Tactic:
rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
theorem isOpenImmersion_eq_inf :
    @IsOpenImmersion = (topologically IsOpenEmbedding) ⊓
      stalkwise (fun f ↦ Function.Bijective f)

Proof state:
⊢ @IsOpenImmersion =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsOpenEmbedding) ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsOpenImmersion x✝ ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsOpenEmbedding) ⊓
        stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f)
      x✝

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsOpenImmersion x✝ ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsOpenEmbedding) ⊓
        stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f)
      x✝

Tactic:
exact isOpenImmersion_iff_stalk.trans
  (and_congr Iff.rfl (forall_congr' fun x ↦ ConcreteCategory.isIso_iff_bijective _))

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negY_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.negY P = -P y

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negY P = -P y

Tactic:
rw [negY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, mul_zero, sub_zero, mul_zero, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma d_none_eq_zero (i j : Option ι) (hi : i = none) :
    d K i j = 0

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i j : Option ι
hi : i = none
⊢ d K i j = 0

Tactic:
subst hi

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
j : Option ι
⊢ d K none j = 0

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
j : Option ι
⊢ d K none j = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
lemma nnnorm_commutator_units_sub_one_le (a b : αˣ) :
    ‖(a * b * a⁻¹ * b⁻¹).val - 1‖₊ ≤ 2 * ‖a⁻¹.val‖₊ * ‖b⁻¹.val‖₊ * ‖a.val - 1‖₊ * ‖b.val - 1‖₊

Proof state:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖₊ ≤ 2 * ‖↑a⁻¹‖₊ * ‖↑b⁻¹‖₊ * ‖↑a - 1‖₊ * ‖↑b - 1‖₊

Tactic:
simpa using norm_commutator_units_sub_one_le a b

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Cones.lean
theorem ConeMorphism.ext {c c' : Cone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g

Proof state:
case mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), hom✝ ≫ c'.π.app j = c.π.app j
w : { hom := hom✝, w := w✝ }.hom = g.hom
⊢ { hom := hom✝, w := w✝ } = g

Tactic:
cases g

Result:
case mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), hom✝¹ ≫ c'.π.app j = c.π.app j
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), hom✝ ≫ c'.π.app j = c.π.app j
w : { hom := hom✝¹, w := w✝¹ }.hom = { hom := hom✝, w := w✝ }.hom
⊢ { hom := hom✝¹, w := w✝¹ } = { hom := hom✝, w := w✝ }

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Result:
case mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), hom✝ ≫ c'.π.app j = c.π.app j
w : { hom := hom✝, w := w✝ }.hom = g.hom
⊢ { hom := hom✝, w := w✝ } = g

Proof state:
case mk.mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), hom✝¹ ≫ c'.π.app j = c.π.app j
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), hom✝ ≫ c'.π.app j = c.π.app j
w : { hom := hom✝¹, w := w✝¹ }.hom = { hom := hom✝, w := w✝ }.hom
⊢ { hom := hom✝¹, w := w✝¹ } = { hom := hom✝, w := w✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem qp_eq (hr : u.r = 0) : u.q = u.qp + 1

Proof state:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : u.r + (u.bp + 1) * u.q = u.ap + 1 := rq_eq u
⊢ u.q = u.qp + 1

Tactic:
rw [hr, hq, mul_zero, add_zero] at h

Result:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : 0 = u.ap + 1
⊢ u.q = u.qp + 1

Proof state:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
⊢ u.q = u.qp + 1

Tactic:
let h := u.rq_eq

Result:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : u.r + (u.bp + 1) * u.q = u.ap + 1 := rq_eq u
⊢ u.q = u.qp + 1

Proof state:
case neg
u : XgcdType
hr : u.r = 0
hq : ¬u.q = 0
⊢ u.q = u.qp + 1

Tactic:
exact (Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hq)).symm

Result:
no goals

Proof state:
u : XgcdType
hr : u.r = 0
⊢ u.q = u.qp + 1

Tactic:
by_cases hq : u.q = 0

Result:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
⊢ u.q = u.qp + 1

case neg
u : XgcdType
hr : u.r = 0
hq : ¬u.q = 0
⊢ u.q = u.qp + 1

Proof state:
case pos
u : XgcdType
hr : u.r = 0
hq : u.q = 0
h : 0 = u.ap + 1
⊢ u.q = u.qp + 1

Tactic:
cases h

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
/-- Characterisation of `2`-Freiman homs. -/
@[to_additive "Characterisation of `2`-Freiman isomorphisms."]
lemma isMulFreimanIso_two :
    IsMulFreimanIso 2 A B f ↔ BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A,
      f a * f b = f c * f d ↔ a * b = c * d where
  mp hf := ⟨hf.bijOn, fun _ ha _ hb _ hc _ hd => hf.mul_eq_mul ha hb hc hd⟩
  mpr hf := ⟨hf.1, by aesop (add simp card_eq_two)⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a * f b = f c * f d ↔ a * b = c * d
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 2 → t.card = 2 → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
aesop (add simp card_eq_two)

Result:
no goals