harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem bound_of_isBigO_nat_atTop {f : ℕ → E} {g'' : ℕ → E''} (h : f =O[atTop] g'') :
    ∃ C > 0, ∀ ⦃x⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖ :=
  bound_of_isBigO_cofinite <| by rwa [Nat.cofinite_eq_atTop]

Proof state:
E : Type u_3
E'' : Type u_9
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup E''
f : ℕ → E
g'' : ℕ → E''
h : f =O[atTop] g''
⊢ f =O[cofinite] g''

Tactic:
rwa [Nat.cofinite_eq_atTop]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem ModelsBoundedFormula.realize_sentence {φ : L.Sentence} (h : T ⊨ᵇ φ) (M : Type*)
    [L.Structure M] [M ⊨ T] [Nonempty M] : M ⊨ φ

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
h : T ⊨ᵇ φ
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ

Tactic:
rw [models_iff_not_satisfiable] at h

Result:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬(T ∪ {Formula.not φ}).IsSatisfiable
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬(T ∪ {Formula.not φ}).IsSatisfiable
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
⊢ M ⊨ φ

Tactic:
contrapose! h

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ (T ∪ {Formula.not φ}).IsSatisfiable

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T

Tactic:
exact ⟨h, inferInstance⟩

Result:
no goals

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ (T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
exact Model.isSatisfiable M

Result:
no goals

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ M ⊨ T ∪ {Formula.not φ}

Tactic:
simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
  Sentence.realize_not]

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ ∀ a ∈ T, M ⊨ a

Tactic:
rw [← model_iff]

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ ¬M ⊨ φ ∧ M ⊨ T

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
⊢ (T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
have : M ⊨ T ∪ {Formula.not φ} := by
  simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp,
    Sentence.realize_not]
  rw [← model_iff]
  exact ⟨h, inferInstance⟩

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : Type u_1
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Nonempty M
h : ¬M ⊨ φ
this : M ⊨ T ∪ {Formula.not φ}
⊢ (T ∪ {Formula.not φ}).IsSatisfiable
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.not_iff [Decidable b] : ¬(a ↔ b) ↔ (¬a ↔ b) :=
  if h : b then by
    rw [iff_true_right h, iff_true_right h]
  else by
    rw [iff_false_right h, iff_false_right h]

Proof state:
b a : Prop
inst✝ : Decidable b
h : ¬b
⊢ ¬(a ↔ b) ↔ (¬a ↔ b)

Tactic:
rw [iff_false_right h, iff_false_right h]

Result:
no goals

Proof state:
b a : Prop
inst✝ : Decidable b
h : b
⊢ ¬(a ↔ b) ↔ (¬a ↔ b)

Tactic:
rw [iff_true_right h, iff_true_right h]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem isSome_isPrefixOf?_eq_isPrefixOf [BEq α] (xs ys : List α) :
    (xs.isPrefixOf? ys).isSome = xs.isPrefixOf ys

Proof state:
α : Type u_1
inst✝ : BEq α
xs ys : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
⊢ ((head✝¹ :: tail✝¹).isPrefixOf? (head✝ :: tail✝)).isSome = (head✝¹ :: tail✝¹).isPrefixOf (head✝ :: tail✝)

Tactic:
simp only [List.isPrefixOf?, List.isPrefixOf]

Result:
α : Type u_1
inst✝ : BEq α
xs ys : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
⊢ (if (head✝¹ == head✝) = true then tail✝¹.isPrefixOf? tail✝ else none).isSome =
    (head✝¹ == head✝ && tail✝¹.isPrefixOf tail✝)

Proof state:
α : Type u_1
inst✝ : BEq α
xs ys : List α
head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
⊢ (if (head✝¹ == head✝) = true then tail✝¹.isPrefixOf? tail✝ else none).isSome =
    (head✝¹ == head✝ && tail✝¹.isPrefixOf tail✝)

Tactic:
split <;> simp [*, isSome_isPrefixOf?_eq_isPrefixOf]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
xs ys x✝ : List α
⊢ ([].isPrefixOf? x✝).isSome = [].isPrefixOf x✝

Tactic:
simp [List.isPrefixOf?]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
xs ys : List α
⊢ (xs.isPrefixOf? ys).isSome = xs.isPrefixOf ys

Tactic:
match xs, ys with
| [], _ => simp [List.isPrefixOf?]
| _::_, [] => rfl
| _::_, _::_ =>
  simp only [List.isPrefixOf?, List.isPrefixOf]
  split <;> simp [*, isSome_isPrefixOf?_eq_isPrefixOf]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
xs ys : List α
head✝ : α
tail✝ : List α
⊢ ((head✝ :: tail✝).isPrefixOf? []).isSome = (head✝ :: tail✝).isPrefixOf []

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
@[simp] lemma greatestFib_pos : 0 < greatestFib n ↔ 0 < n

Proof state:
n : ℕ
⊢ 0 < n.greatestFib ↔ 0 < n

Tactic:
simp [pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma antivaryOn_iff_forall_smul_nonpos :
    AntivaryOn f g s ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0 :=
  monovaryOn_toDual_right.symm.trans <| by rw [monovaryOn_iff_forall_smul_nonneg]; rfl

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0

Tactic:
rw [monovaryOn_iff_forall_smul_nonneg]

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ (∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • ((⇑OrderDual.toDual ∘ g) j - (⇑OrderDual.toDual ∘ g) i)) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ (∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • ((⇑OrderDual.toDual ∘ g) j - (⇑OrderDual.toDual ∘ g) i)) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma equiv_chgUniv (L : C ⥤ D) [L.IsLocalization W] {X Y : C}
    [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w''} W X Y]
    (e : SmallHom.{w} W X Y) :
    equiv W L (chgUniv.{w''} e) = equiv W L e

Proof state:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
f : W.Q.obj X ⟶ W.Q.obj Y
⊢ (equiv W L) ((equiv W W.Q).symm ((equiv W W.Q) ((equiv W W.Q).symm f))) = (equiv W L) ((equiv W W.Q).symm f)

Tactic:
simp only [Equiv.apply_symm_apply,
  equiv_equiv_symm W _ _ _ (Localization.compUniqFunctor W.Q L W)]

Result:
no goals

Proof state:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
f : W.Q.obj X ⟶ W.Q.obj Y
⊢ (equiv W L) (chgUniv ((equiv W W.Q).symm f)) = (equiv W L) ((equiv W W.Q).symm f)

Tactic:
dsimp [chgUniv]

Result:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
f : W.Q.obj X ⟶ W.Q.obj Y
⊢ (equiv W L) ((equiv W W.Q).symm ((equiv W W.Q) ((equiv W W.Q).symm f))) = (equiv W L) ((equiv W W.Q).symm f)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
e : SmallHom W X Y
⊢ (equiv W L) (chgUniv e) = (equiv W L) e

Tactic:
obtain ⟨f, rfl⟩ := (equiv W W.Q).symm.surjective e

Result:
case intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
f : W.Q.obj X ⟶ W.Q.obj Y
⊢ (equiv W L) (chgUniv ((equiv W W.Q).symm f)) = (equiv W L) ((equiv W W.Q).symm f)
-- Mathlib/Order/JordanHolder.lean
theorem last_eraseLast_le (s : CompositionSeries X) : s.eraseLast.last ≤ s.last

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ (eraseLast s).last ≤ last s

Tactic:
simp [eraseLast, last, s.strictMono.le_iff_le, Fin.le_iff_val_le_val]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
@[simp]
lemma one_scaleRoots (r : R) :
    (1 : R[X]).scaleRoots r = 1

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
⊢ scaleRoots 1 r = 1

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Semiring R
r : R
n✝ : ℕ
⊢ (scaleRoots 1 r).coeff n✝ = coeff 1 n✝

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
r : R
n✝ : ℕ
⊢ (scaleRoots 1 r).coeff n✝ = coeff 1 n✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_flatten (a : α) (l : Array (Array α)) :
    count a l.flatten = (l.map (count a)).sum

Proof state:
case of
α : Type u_1
inst✝ : BEq α
a : α
xss✝ : List (List α)
⊢ count a (List.map List.toArray xss✝).toArray.flatten = (map (count a) (List.map List.toArray xss✝).toArray).sum

Tactic:
simp [List.count_flatten, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : Array (Array α)
⊢ count a l.flatten = (map (count a) l).sum

Tactic:
cases l using array₂_induction

Result:
case of
α : Type u_1
inst✝ : BEq α
a : α
xss✝ : List (List α)
⊢ count a (List.map List.toArray xss✝).toArray.flatten = (map (count a) (List.map List.toArray xss✝).toArray).sum
-- Mathlib/Algebra/Algebra/Operations.lean
lemma restrictScalars_pow {A B C : Type*} [Semiring A] [Semiring B]
    [Semiring C] [SMul A B] [Module A C] [Module B C]
    [IsScalarTower A C C] [IsScalarTower B C C] [IsScalarTower A B C]
    {I : Submodule B C} :
    ∀ {n : ℕ}, (hn : n ≠ 0) → (I ^ n).restrictScalars A = I.restrictScalars A ^ n
  | 1, _ => by simp [Submodule.pow_one]
  | n + 2, _ => by
    simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]

Proof state:
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Semiring C
inst✝⁵ : SMul A B
inst✝⁴ : Module A C
inst✝³ : Module B C
inst✝² : IsScalarTower A C C
inst✝¹ : IsScalarTower B C C
inst✝ : IsScalarTower A B C
I : Submodule B C
x✝ : 1 ≠ 0
⊢ restrictScalars A (I ^ 1) = restrictScalars A I ^ 1

Tactic:
simp [Submodule.pow_one]

Result:
no goals

Proof state:
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Semiring C
inst✝⁵ : SMul A B
inst✝⁴ : Module A C
inst✝³ : Module B C
inst✝² : IsScalarTower A C C
inst✝¹ : IsScalarTower B C C
inst✝ : IsScalarTower A B C
I : Submodule B C
n : ℕ
x✝ : n + 2 ≠ 0
⊢ restrictScalars A (I ^ (n + 2)) = restrictScalars A I ^ (n + 2)

Tactic:
simp [Submodule.pow_succ (n := n + 1), restrictScalars_mul, restrictScalars_pow n.succ_ne_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem map_smul [Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁) :
    f (c • x) = c • f x

Proof state:
R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₁ M₂
f : M₁ →L[R₁] M₂
c : R₁
x : M₁
⊢ f (c • x) = c • f x

Tactic:
simp only [RingHom.id_apply, ContinuousLinearMap.map_smulₛₗ]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem is_real_TFAE (z : K) : TFAE [conj z = z, ∃ r : ℝ, (r : K) = z, ↑(re z) = z, im z = 0]

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Tactic:
tfae_have 1 → 4
| h => by
  rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
    ofReal_zero]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Tactic:
tfae_have 2 → 1 := fun ⟨r, hr⟩ => hr ▸ conj_ofReal _

Result:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Tactic:
tfae_have 4 → 3
| h => by
  conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
x✝ : im z = 0
h : im z = 0 := x✝
⊢ ↑(re z) = z

Tactic:
conv_rhs => rw [← re_add_im z, h, ofReal_zero, zero_mul, add_zero]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Tactic:
tfae_have 3 → 2 := fun h => ⟨_, h⟩

Result:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ im z = 0

Tactic:
rw [← @ofReal_inj K, im_eq_conj_sub, h, sub_self, mul_zero, zero_div,
  ofReal_zero]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
lemma singleton_inter {a : α} {s : Finset α} :
    {a} ∩ s = if a ∈ s then {a} else ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ {a} ∩ s = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem argmax_mem : ∀ {l : List α} {m : α}, m ∈ argmax f l → m ∈ l
  | [], m => by simp
  | hd :: tl, m => by simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x1 x2 => x1 < x2
f : α → β
hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl

Tactic:
simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x1 x2 => x1 < x2
f : α → β
m : α
⊢ m ∈ argmax f [] → m ∈ []

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem _root_.NumberField.adjoin_eq_top_of_infinitePlace_lt {x : 𝓞 K} {w : InfinitePlace K}
    (h₁ : x ≠ 0) (h₂ : ∀ ⦃w'⦄, w' ≠ w → w' x < 1) (h₃ : IsReal w ∨ |(w.embedding x).re| < 1) :
    Algebra.adjoin ℚ {(x : K)} = ⊤

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ℚ⟮↑x⟯.toSubalgebra = ⊤

Tactic:
exact congr_arg IntermediateField.toSubalgebra <|
  NumberField.is_primitive_element_of_infinitePlace_lt h₁ h₂ h₃

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ Algebra.adjoin ℚ {↑x} = ⊤

Tactic:
rw [← IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.of_finite ℚ _)]

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
⊢ ℚ⟮↑x⟯.toSubalgebra = ⊤
-- Mathlib/Data/Nat/Factorization/Induction.lean
theorem multiplicative_factorization' {β : Type*} [CommMonoid β] (f : ℕ → β)
    (h_mult : ∀ x y : ℕ, Coprime x y → f (x * y) = f x * f y) (hf0 : f 0 = 1) (hf1 : f 1 = 1) :
    f n = n.factorization.prod fun p k => f (p ^ k)

Proof state:
case inl
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = (factorization 0).prod fun p k => f (p ^ k)

Tactic:
simpa

Result:
no goals

Proof state:
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f n = n.factorization.prod fun p k => f (p ^ k)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case inl
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
⊢ f 0 = (factorization 0).prod fun p k => f (p ^ k)

case inr
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
hn : n ≠ 0
⊢ f n = n.factorization.prod fun p k => f (p ^ k)

Proof state:
case inr
n : ℕ
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf0 : f 0 = 1
hf1 : f 1 = 1
hn : n ≠ 0
⊢ f n = n.factorization.prod fun p k => f (p ^ k)

Tactic:
exact multiplicative_factorization _ h_mult hf1 hn

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma neg_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.neg P ≈ W'.neg Q

Proof state:
case intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.neg ((fun m => m • Q) u) ≈ W'.neg Q

Tactic:
exact neg_smul_equiv Q u.isUnit

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.neg P ≈ W'.neg Q

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.neg ((fun m => m • Q) u) ≈ W'.neg Q
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc]
lemma leftHomologyMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃)
    (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData) :
    leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫
      leftHomologyMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Tactic:
let γ₁ := leftHomologyMapData φ₁ h₁ h₂

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.leftHomologyMap'_eq, γ₂.leftHomologyMap'_eq, (γ₁.comp γ₂).leftHomologyMap'_eq,
  LeftHomologyMapData.comp_φH]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃

Tactic:
let γ₂ := leftHomologyMapData φ₂ h₂ h₃

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
h₃ : S₃.LeftHomologyData
γ₁ : LeftHomologyMapData φ₁ h₁ h₂ := leftHomologyMapData φ₁ h₁ h₂
γ₂ : LeftHomologyMapData φ₂ h₂ h₃ := leftHomologyMapData φ₂ h₂ h₃
⊢ leftHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = leftHomologyMap' φ₁ h₁ h₂ ≫ leftHomologyMap' φ₂ h₂ h₃
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_zero_add_hom_app (a : A) (X : C) :
    (shiftFunctorAdd' C 0 a a (zero_add a)).hom.app X =
    ((shiftFunctorZero C A).inv.app X)⟦a⟧'

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C 0 a a ⋯).hom.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_zero_add C a)) X

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nat_lt_lift_iff {n : ℕ} {a : Cardinal.{u}} : n < lift.{v} a ↔ n < a

Proof state:
n : ℕ
a : Cardinal.{u}
⊢ ↑n < lift.{v, u} a ↔ ↑n < a

Tactic:
rw [← lift_natCast.{v,u}, lift_lt]

Result:
no goals