harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Pell.lean
theorem pos_generator_iff_fundamental (a : Solution₁ d) :
    (1 < a.x ∧ 0 < a.y ∧ ∀ b : Solution₁ d, ∃ n : ℤ, b = a ^ n ∨ b = -a ^ n) ↔ IsFundamental a

Proof state:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
⊢ IsFundamental a

Tactic:
have hd := d_nonsquare_of_one_lt_x h.1

Result:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
⊢ IsFundamental a

Proof state:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
⊢ IsFundamental a

Tactic:
have h₀ := d_pos_of_one_lt_x h.1

Result:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
⊢ IsFundamental a

Proof state:
case intro.intro.intro
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
b : Solution₁ d
hb₂ :
  ∀ (y : Solution₁ d), (fun a₁ => 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b
⊢ IsFundamental a

Tactic:
rwa [hb₂ a h, ← hb₂ a₁ ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩]

Result:
no goals

Proof state:
case intro
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
⊢ IsFundamental a

Tactic:
obtain ⟨b, -, hb₂⟩ := existsUnique_pos_generator h₀ hd

Result:
case intro.intro.intro
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
b : Solution₁ d
hb₂ :
  ∀ (y : Solution₁ d), (fun a₁ => 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b
⊢ IsFundamental a

Proof state:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
⊢ IsFundamental a

Tactic:
obtain ⟨a₁, ha₁⟩ := IsFundamental.exists_of_not_isSquare h₀ hd

Result:
case intro
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
⊢ IsFundamental a

Proof state:
d : ℤ
a : Solution₁ d
⊢ (1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n) ↔ IsFundamental a

Tactic:
refine ⟨fun h => ?_, fun H => ⟨H.1, H.2.1, H.eq_zpow_or_neg_zpow⟩⟩

Result:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
⊢ IsFundamental a
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_of_left {α β γ} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
    {f : α × β → γ} {μ : Measure α} {ν : Measure β} {τ : Measure γ} (hf : Measurable f)
    [SFinite μ] [SFinite ν]
    (h2f : ∀ᵐ y ∂ν, QuasiMeasurePreserving (fun x => f (x, y)) μ τ) :
    QuasiMeasurePreserving f (μ.prod ν) τ

Proof state:
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SFinite μ
inst✝ : SFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun x => f (x, y)) μ τ
⊢ QuasiMeasurePreserving f (map Prod.swap (ν.prod μ)) τ

Tactic:
convert (QuasiMeasurePreserving.prod_of_right (hf.comp measurable_swap) h2f).comp
    ((measurable_swap.measurePreserving (ν.prod μ)).symm
        MeasurableEquiv.prodComm).quasiMeasurePreserving

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SFinite μ
inst✝ : SFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun x => f (x, y)) μ τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ

Tactic:
rw [← prod_swap]

Result:
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst✝¹ : SFinite μ
inst✝ : SFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun x => f (x, y)) μ τ
⊢ QuasiMeasurePreserving f (map Prod.swap (ν.prod μ)) τ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_eq' {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x)

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Tactic:
by_cases h : xs.all p

Result:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = true
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.all p = true
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ false = decide (∀ (x : α), x ∈ xs → p x = true)

Proof state:
case pos
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = true
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Tactic:
simp_all [all_eq_true', -all_eq_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ∃ x, x ∈ xs ∧ ¬p x = true
⊢ false = decide (∀ (x : α), x ∈ xs → p x = true)

Tactic:
simpa using h

Result:
no goals

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ false = decide (∀ (x : α), x ∈ xs → p x = true)

Tactic:
simp only [all_eq_false'] at h

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ∃ x, x ∈ xs ∧ ¬p x = true
⊢ false = decide (∀ (x : α), x ∈ xs → p x = true)

Proof state:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : ¬xs.all p = true
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Tactic:
simp only [Bool.not_eq_true] at h

Result:
case neg
α : Type u_1
xs : Array α
p : α → Bool
h : xs.all p = false
⊢ xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
/-- Geometric progressions of length three are unchanged under `2`-Freiman isomorphisms. -/
@[to_additive
"Arithmetic progressions of length three are unchanged under `2`-Freiman isomorphisms."]
lemma threeGPFree_image (hf : IsMulFreimanIso 2 s t f) (hAs : A ⊆ s) :
    ThreeGPFree (f '' A) ↔ ThreeGPFree A

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ ThreeGPFree (f '' A) ↔ ThreeGPFree A

Tactic:
rw [ThreeGPFree, ThreeGPFree]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
this : BijOn f A (f '' A)
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b

Tactic:
simp +contextual only
  [((hf.bijOn.injOn.mono hAs).bijOn_image (f := f)).forall,
  hf.mul_eq_mul (hAs _) (hAs _) (hAs _) (hAs _), this.injOn.eq_iff]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b

Tactic:
have := (hf.bijOn.injOn.mono hAs).bijOn_image (f := f)

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
this : BijOn f A (f '' A)
⊢ (∀ ⦃a : β⦄, a ∈ f '' A → ∀ ⦃b : β⦄, b ∈ f '' A → ∀ ⦃c : β⦄, c ∈ f '' A → a * c = b * b → a = b) ↔
    ∀ ⦃a : α⦄, a ∈ A → ∀ ⦃b : α⦄, b ∈ A → ∀ ⦃c : α⦄, c ∈ A → a * c = b * b → a = b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
    (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
      | some a, some b => some (f a b) | _, _ => none

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
⊢ (zipWith f as bs)[i]? =
    match as[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
induction as generalizing bs i with
| nil => cases bs with
  | nil => simp
  | cons b bs => simp
| cons a as aih => cases bs with
  | nil => simp
  | cons b bs => cases i <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
as : List α
aih :
  ∀ {bs : List β} {i : Nat},
    (zipWith f as bs)[i]? =
      match as[i]?, bs[i]? with
      | some a, some b => some (f a b)
      | x, x_1 => none
bs : List β
i : Nat
⊢ (zipWith f (a :: as) bs)[i]? =
    match (a :: as)[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
cases bs with
| nil => simp
| cons b bs => cases i <;> simp_all

Result:
no goals

Proof state:
case nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
b : β
bs : List β
⊢ (zipWith f [] (b :: bs))[i]? =
    match [][i]?, (b :: bs)[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
bs : List β
i : Nat
⊢ (zipWith f [] bs)[i]? =
    match [][i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
cases bs with
| nil => simp
| cons b bs => simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
as : List α
aih :
  ∀ {bs : List β} {i : Nat},
    (zipWith f as bs)[i]? =
      match as[i]?, bs[i]? with
      | some a, some b => some (f a b)
      | x, x_1 => none
i : Nat
b : β
bs : List β
⊢ (zipWith f (a :: as) (b :: bs))[i]? =
    match (a :: as)[i]?, (b :: bs)[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
cases i <;> simp_all

Result:
no goals

Proof state:
case nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
⊢ (zipWith f [] [])[i]? =
    match [][i]?, [][i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
simp

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
as : List α
aih :
  ∀ {bs : List β} {i : Nat},
    (zipWith f as bs)[i]? =
      match as[i]?, bs[i]? with
      | some a, some b => some (f a b)
      | x, x_1 => none
i : Nat
⊢ (zipWith f (a :: as) [])[i]? =
    match (a :: as)[i]?, [][i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
lemma biSup_le_eq_iSup {ι : Type*} [Preorder ι] {f : ι → α} :
    ⨆ (i) (j ≤ i), f j = ⨆ i, f i

Proof state:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j ≤ ⨆ i, f i

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j = ⨆ i, f i

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j ≤ ⨆ i, f i

case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j

Proof state:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, f i ≤ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j

Tactic:
exact iSup_le fun j ↦ le_iSup_of_le j (le_iSup₂_of_le j le_rfl le_rfl)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem equalizerCondition_precomp_of_preservesPullback (P : Cᵒᵖ ⥤ D) (F : E ⥤ C)
    [∀ {X B} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F]
    [F.PreservesEffectiveEpis] (hP : EqualizerCondition P) : EqualizerCondition (F.op ⋙ P)

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ c.snd = (Iso.refl c.pt).hom ≫ (PullbackCone.mk c.fst c.snd ⋯).snd

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Category.{u_6, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [inst : EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ c.fst = (Iso.refl c.pt).hom ≫ (PullbackCone.mk c.fst c.snd ⋯).fst

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_pop {f : α → β} {l : Vector α n} : l.pop.map f = (l.map f).pop

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
⊢ map f l.pop = (map f l).pop

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ }.pop =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).pop

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ }.pop =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).pop

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma add_comp
    {a b c : M} (α₁ α₂ : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
    (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Proof state:
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
X Y Z : C
inst✝ : Preadditive C
a b c : M
α₁ α₂ : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Tactic:
rw [comp, comp, comp, Preadditive.add_comp]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp] lemma inner_zero_right {x : E} : ⟪x, 0⟫ = 0

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x : E
⊢ inner x 0 = 0

Tactic:
simp [← innerₛₗ_apply]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_unique [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (h₀ : edist x y ≠ 0)
    (htop : edist x y ≠ ⊤) (hr : edist (f x) (f y) = r * edist x y) : r = ratio f

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
h₀ : edist x y ≠ 0
htop : edist x y ≠ ⊤
hr : edist (f x) (f y) = ↑r * edist x y
⊢ r = ratio f

Tactic:
simpa only [hr, ENNReal.mul_left_inj h₀ htop, ENNReal.coe_inj] using edist_eq f x y

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_span_set_eq_card {s : Set M} [Fintype s] (hs : LinearIndepOn R id s) :
    finrank R (span R s) = s.toFinset.card :=
  finrank_eq_of_rank_eq
    (by
      have : Module.rank R (span R s) = #s := rank_span_set hs
      rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card

Tactic:
have : Module.rank R (span R s) = #s := rank_span_set hs

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndepOn R id s
this : Module.rank R ↥(span R s) = #↑s
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
s : Set M
inst✝ : Fintype ↑s
hs : LinearIndepOn R id s
this : Module.rank R ↥(span R s) = #↑s
⊢ Module.rank R ↥(span R s) = ↑s.toFinset.card

Tactic:
rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isTheta_deriv_rpow_p_mul_one_sub_smoothingFn {p : ℝ} (hp : p ≠ 0) :
    (fun x => ‖deriv (fun z => z ^ p * (1 - ε z)) x‖) =Θ[atTop] fun z => z ^ (p-1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun z => z ^ p * (1 - ε z)) =Θ[atTop] fun z => z ^ (p - 1)

Tactic:
calc (fun x => deriv (fun z => z ^ p * (1 - ε z)) x) =Θ[atTop] fun z => p * z ^ (p-1) :=
          (isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn hp).isTheta
  _ =Θ[atTop] fun z => z ^ (p-1) :=
          IsTheta.const_mul_left hp <| isTheta_refl _ _

Result:
no goals

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (fun x => ‖deriv (fun z => z ^ p * (1 - ε z)) x‖) =Θ[atTop] fun z => z ^ (p - 1)

Tactic:
refine IsTheta.norm_left ?_

Result:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun z => z ^ p * (1 - ε z)) =Θ[atTop] fun z => z ^ (p - 1)
-- Mathlib/CategoryTheory/Functor/ReflectsIso.lean
lemma Functor.balanced_of_preserves (F : C ⥤ D)
    [F.ReflectsIsomorphisms] [F.PreservesEpimorphisms] [F.PreservesMonomorphisms] [Balanced D] :
    Balanced C where
  isIso_of_mono_of_epi f _ _

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.ReflectsIsomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : F.PreservesMonomorphisms
inst✝ : Balanced D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso (F.map f)

Tactic:
exact isIso_of_mono_of_epi _

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.ReflectsIsomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : F.PreservesMonomorphisms
inst✝ : Balanced D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso (F := F)]

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.ReflectsIsomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : F.PreservesMonomorphisms
inst✝ : Balanced D
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso (F.map f)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblXYZ_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.dblXYZ P = P y ^ 4 • ![0, 1, 0]

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'.dblXYZ P = P y ^ 4 • ![0, 1, 0]

Tactic:
erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
  mul_zero, mul_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_insert' (f : α → M) (h : a ∉ s) (hs : (s ∩ mulSupport f).Finite) :
    ∏ᶠ i ∈ insert a s, f i = f a * ∏ᶠ i ∈ s, f i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite

Tactic:
exact (finite_singleton a).inter_of_left _

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ Disjoint {a} s

Tactic:
rwa [disjoint_singleton_left]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ Disjoint {a} s

α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_div {d n : ℕ} (h : d ∣ n) :
    (n / d).factorization = n.factorization - d.factorization

Proof state:
case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Proof state:
d n : ℕ
h : d ∣ n
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Result:
case inl
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

case inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Proof state:
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization

Tactic:
rw [tsub_add_cancel_of_le <| (Nat.factorization_le_iff_dvd hd hn).mpr h, ←
  Nat.factorization_mul (Nat.div_pos (Nat.le_of_dvd hn.bot_lt h) hd.bot_lt).ne' hd,
  Nat.div_mul_cancel h]

Result:
no goals

Proof state:
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (fun x => x + d.factorization) (n / d).factorization =
    (fun x => x + d.factorization) (n.factorization - d.factorization)

Tactic:
simp only

Result:
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization

Proof state:
case inr.inl
d : ℕ
hd : d ≠ 0
h : d ∣ 0
⊢ (0 / d).factorization = factorization 0 - d.factorization

Tactic:
simp [tsub_eq_zero_of_le]

Result:
no goals

Proof state:
case inr.inr
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (n / d).factorization = n.factorization - d.factorization

Tactic:
apply add_left_injective d.factorization

Result:
case inr.inr.a
d n : ℕ
h : d ∣ n
hd : d ≠ 0
hn : n ≠ 0
⊢ (fun x => x + d.factorization) (n / d).factorization =
    (fun x => x + d.factorization) (n.factorization - d.factorization)

Proof state:
case inl
n : ℕ
h : 0 ∣ n
⊢ (n / 0).factorization = n.factorization - factorization 0

Tactic:
simp [zero_dvd_iff.mp h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.div_closedBall (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) :
    s / closedBall x δ = x⁻¹ • cthickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s / closedBall x δ = x⁻¹ • cthickening δ s

Tactic:
simp [div_eq_mul_inv, mul_comm, hs.mul_closedBall hδ]

Result:
no goals