harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem isIso_arrow_iff_eq_top {Y : C} (P : Subobject Y) : IsIso P.arrow ↔ P = ⊤

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y : C
P : Subobject Y
⊢ IsIso P.arrow ↔ P = ⊤

Tactic:
rw [isIso_iff_mk_eq_top, mk_arrow]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
    W.dblY P / W.dblZ P ^ 3 = W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.dblY P / W.dblZ P ^ 3 =
    (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hx hy,
  dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Action.lean
theorem smul_set_ae_eq (c : G) {s t : Set α} : c • s =ᵐ[μ] c • t ↔ s =ᵐ[μ] t

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ c • s =ᶠ[ae μ] c • t ↔ s =ᶠ[ae μ] t

Tactic:
simp only [Filter.eventuallyLE_antisymm_iff, smul_set_ae_le]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The abscissa of absolute convergence of the L-series of a Dirichlet character mod `N > 0`
is `1`. -/
lemma absicssaOfAbsConv_eq_one {N : ℕ} (hn : N ≠ 0) (χ : DirichletCharacter ℂ N) :
    abscissaOfAbsConv ↗χ = 1

Proof state:
N : ℕ
hn : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ (abscissaOfAbsConv fun n => χ ↑n) = 1

Tactic:
simpa [abscissaOfAbsConv, LSeriesSummable_iff hn χ, Set.Ioi_def, EReal.image_coe_Ioi]
  using csInf_Ioo <| EReal.coe_lt_top 1

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ico_zpow :
    Pairwise (Disjoint on fun n : ℤ => Ico (b ^ n) (b ^ (n + 1)))

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
b : α
⊢ Pairwise (Disjoint on fun n => Ico (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ico_mul_zpow 1 b

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma comap_symm (G : SimpleGraph V) (e : V ≃ W) :
    G.comap e.symm.toEmbedding = G.map e.toEmbedding

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
⊢ SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map e.toEmbedding G

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
x✝¹ x✝ : W
⊢ (SimpleGraph.comap (⇑e.symm.toEmbedding) G).Adj x✝¹ x✝ ↔ (SimpleGraph.map e.toEmbedding G).Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
x✝¹ x✝ : W
⊢ (SimpleGraph.comap (⇑e.symm.toEmbedding) G).Adj x✝¹ x✝ ↔ (SimpleGraph.map e.toEmbedding G).Adj x✝¹ x✝

Tactic:
simp only [Equiv.apply_eq_iff_eq_symm_apply, comap_adj, map_adj, Equiv.toEmbedding_apply,
exists_eq_right_right, exists_eq_right]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem AEEqFun.compMeasurePreserving_mem_Lp {β : Type*} [MeasurableSpace β]
    {μb : MeasureTheory.Measure β} {g : β →ₘ[μb] E} (hg : g ∈ Lp E p μb) {f : α → β}
    (hf : MeasurePreserving f μ μb) :
    g.compMeasurePreserving f hf ∈ Lp E p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : eLpNorm (↑g) p μb < ⊤
f : α → β
hf : MeasurePreserving f μ μb
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ < ⊤

Tactic:
rwa [eLpNorm_compMeasurePreserving]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : g ∈ Lp E p μb
f : α → β
hf : MeasurePreserving f μ μb
⊢ g.compMeasurePreserving f hf ∈ Lp E p μ

Tactic:
rw [Lp.mem_Lp_iff_eLpNorm_lt_top] at hg ⊢

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
β : Type u_7
inst✝ : MeasurableSpace β
μb : Measure β
g : β →ₘ[μb] E
hg : eLpNorm (↑g) p μb < ⊤
f : α → β
hf : MeasurePreserving f μ μb
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ < ⊤
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_apply_eq (x : 𝔸) (n : ℕ) :
    (expSeries 𝕂 𝔸 n fun _ => x) = (n !⁻¹ : 𝕂) • x ^ n

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 => x) = (↑n !)⁻¹ • x ^ n

Tactic:
simp [expSeries]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem sub_one_mul (a b : α) : (a - 1) * b = a * b - b

Proof state:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ (a - 1) * b = a * b - b

Tactic:
rw [sub_mul, one_mul]

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_add_tail (x : 𝕎 R) (n : ℕ) : init n x + tail n x = x

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ init n x + tail n x = x

Tactic:
simp only [init, tail, ← not_lt, select_add_select_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_right_eq_self {x y : List α} : x ++ y = x ↔ y = []

Proof state:
α : Type u_1
x y : List α
⊢ x ++ y = x ↔ y = []

Tactic:
rw [← append_right_inj (t₁ := y), append_nil]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/Lawful/MonadLift.lean
theorem lift_bind (ma : m α) (f : α → m β) :
    OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a))

Proof state:
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u_1
ma : m α
f : α → m β
⊢ OptionT.lift (ma >>= f) = do
    let a ← OptionT.lift ma
    OptionT.lift (f a)

Tactic:
simp only [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
  map_bind]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Lemmas.lean
theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat

Proof state:
n : UInt32
m : Nat
h : m < size
⊢ ofNat m ≤ n → m ≤ n.toNat

Tactic:
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma succAbove_eq_last_iff {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ last _) :
    a.succAbove b = last _ ↔ b = last _

Proof state:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
⊢ a.succAbove b = last (n + 1) ↔ b = last n

Tactic:
simp [← succAbove_ne_last_last ha, succAbove_right_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a) :
    ⟦aig, ⟨start, hstart⟩, assign⟧ = assign a

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    assign a

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧ = assign a

Tactic:
unfold denote denote.go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    assign a
-- Mathlib/Algebra/Regular/Basic.lean
/-- Any power of a left-regular element is left-regular. -/
lemma IsLeftRegular.pow (n : ℕ) (rla : IsLeftRegular a) : IsLeftRegular (a ^ n)

Proof state:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rla : IsLeftRegular a
⊢ IsLeftRegular (a ^ n)

Tactic:
simp only [IsLeftRegular, ← mul_left_iterate, rla.iterate n]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
lemma mono_f₁₂ [Mono sq.f₃₄] : Mono sq.f₁₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
this : Mono sq.flip.f₂₄
⊢ Mono sq.f₁₂

Tactic:
exact h.flip.mono_f₁₃

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
⊢ Mono sq.f₁₂

Tactic:
have : Mono sq.flip.f₂₄ := by dsimp; infer_instance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
this : Mono sq.flip.f₂₄
⊢ Mono sq.f₁₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
⊢ Mono sq.flip.f₂₄

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
⊢ Mono sq.f₃₄

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
sq : Square C
h : sq.IsPullback
inst✝ : Mono sq.f₃₄
⊢ Mono sq.f₃₄

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem monic_mul_leadingCoeff_inv {p : K[X]} (h : p ≠ 0) : Monic (p * C (leadingCoeff p)⁻¹)

Proof state:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
h : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).Monic

Tactic:
rw [Monic, leadingCoeff_mul, leadingCoeff_C,
  mul_inv_cancel₀ (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem mem_sub {a : α} {s t : Multiset α} :
    a ∈ s - t ↔ t.count a < s.count a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ∈ s - t ↔ count a t < count a s

Tactic:
rw [← count_pos, count_sub, Nat.sub_pos_iff_lt]

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
lemma even_iff_mod_of_even {n : ℕ} (hn : Even n) {k : Fin n} : Even k ↔ k.val % 2 = 0

Proof state:
n : ℕ
hn : Even n
k : Fin n
⊢ Even ↑k ↔ ↑k % 2 = 0

Tactic:
exact Nat.even_iff

Result:
no goals

Proof state:
n : ℕ
hn : Even n
k : Fin n
⊢ Even k ↔ ↑k % 2 = 0

Tactic:
rw [even_iff_of_even hn]

Result:
n : ℕ
hn : Even n
k : Fin n
⊢ Even ↑k ↔ ↑k % 2 = 0
-- Mathlib/Data/Set/Image.lean
theorem mem_image_iff_of_inverse {f : α → β} {g : β → α} {b : β} {s : Set α} (h₁ : LeftInverse g f)
    (h₂ : RightInverse g f) : b ∈ f '' s ↔ g b ∈ s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ f '' s ↔ g b ∈ s

Tactic:
rw [image_eq_preimage_of_inverse h₁ h₂]

Result:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ g ⁻¹' s ↔ g b ∈ s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ g ⁻¹' s ↔ g b ∈ s

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem unzip_enum_eq_prod (l : List α) : l.enum.unzip = (range l.length, l)

Proof state:
α : Type u_1
l : List α
⊢ l.enum.unzip = (range l.length, l)

Tactic:
simp only [enum_eq_zip_range, unzip_zip, length_range]

Result:
no goals
-- Mathlib/Order/Category/FinBddDistLat.lean
lemma comp_apply {X Y Z : FinBddDistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : FinBddDistLat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem norm_of_pow (a : α) (n : ℕ) : norm (of a ^ n) = n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (of a ^ n).norm = n

Tactic:
rw [norm, toWord_of_pow, List.length_replicate]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map_pmap {p : α → Prop} (f₁ : β → γ) (f₂ : (a : α) → p a → β) (H : ∀ x ∈ xs.toList, p x):
    map f₁ (pmap f₂ xs H) = pmap (fun x hx => f₁ <| f₂ x hx) xs H

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
p : α → Prop
f₁ : β → γ
f₂ : (a : α) → p a → β
H : ∀ x ∈ xs.toList, p x
⊢ map f₁ (pmap f₂ xs H) = pmap (fun x hx => f₁ (f₂ x hx)) xs H

Tactic:
induction xs <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem eigenspace_restrict_eq_bot {f : End R M} {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p)
    {μ : R} (hμp : Disjoint (f.eigenspace μ) p) : eigenspace (f.restrict hfp) μ = ⊥

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
hμp : Disjoint (f.eigenspace μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥

Tactic:
intro x hx

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
hμp : Disjoint (f.eigenspace μ) p
x : ↥p
hx : x ∈ eigenspace (LinearMap.restrict f hfp) μ
⊢ x ∈ ⊥

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
hμp : Disjoint (f.eigenspace μ) p
x : ↥p
hx : x ∈ eigenspace (LinearMap.restrict f hfp) μ
⊢ x ∈ ⊥

Tactic:
simpa using hμp.le_bot ⟨eigenspace_restrict_le_eigenspace f hfp μ ⟨x, hx, rfl⟩, x.prop⟩

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
hμp : Disjoint (f.eigenspace μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, f x ∈ p
μ : R
hμp : Disjoint (f.eigenspace μ) p
⊢ eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥
-- Mathlib/FieldTheory/Extension.lean
theorem lt_iff : L₁ < L₂ ↔
    ∃ h : L₁.carrier < L₂.carrier, L₂.emb.comp (inclusion h.le) = L₁.emb

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ L₁ < L₂ ↔ ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
rw [lt_iff_le_carrier_ne, le_iff]

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
    ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
L₁ L₂ : Lifts F E K
⊢ (∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (inclusion h) = L₁.emb) ∧ L₁.carrier ≠ L₂.carrier ↔
    ∃ (h : L₁.carrier < L₂.carrier), L₂.emb.comp (inclusion ⋯) = L₁.emb

Tactic:
exact ⟨fun h ↦ ⟨h.1.1.lt_of_ne h.2, h.1.2⟩, fun h ↦ ⟨⟨h.1.le, h.2⟩, h.1.ne⟩⟩

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_of_map_pow_eq_add_int {x : ℝ} {n : ℕ} {m : ℤ} (h : (f ^ n) x = x + m)
    (hn : 0 < n) : τ f = m / n

Proof state:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n

Tactic:
rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this

Result:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : τ f * ↑n = ↑m
⊢ ↑n ≠ 0

Proof state:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
⊢ τ f = ↑m / ↑n

Tactic:
have := (f ^ n).translationNumber_of_eq_add_int h

Result:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n

Proof state:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n) x = x + ↑m
hn : 0 < n
this : τ f * ↑n = ↑m
⊢ ↑n ≠ 0

Tactic:
exact Nat.cast_ne_zero.2 (ne_of_gt hn)

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem ContDiff.dimH_range_le {f : E → F} (h : ContDiff ℝ 1 f) : dimH (range f) ≤ finrank ℝ E :=
  calc
    dimH (range f) = dimH (f '' univ)

Proof state:
E : Type u_4
F : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
h : ContDiff ℝ 1 f
⊢ dimH (range f) = dimH (f '' univ)

Tactic:
rw [image_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem ite_one_mul {P : Prop} [Decidable P] {a b : M} :
    ite P 1 (a * b) = ite P 1 a * ite P 1 b

Proof state:
M : Type u_4
inst✝¹ : MulOneClass M
P : Prop
inst✝ : Decidable P
a b : M
⊢ (if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b

Tactic:
by_cases h : P <;> simp [h]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem range_algebraMap_eq : (valuation A K).integer = (algebraMap A K).range

Proof state:
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
⊢ (valuation A K).integer = (algebraMap A K).range

Tactic:
ext

Result:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ (valuation A K).integer ↔ x✝ ∈ (algebraMap A K).range

Proof state:
case h
A : Type u
inst✝⁵ : CommRing A
K : Type v
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsDomain A
inst✝¹ : ValuationRing A
inst✝ : IsFractionRing A K
x✝ : K
⊢ x✝ ∈ (valuation A K).integer ↔ x✝ ∈ (algebraMap A K).range

Tactic:
exact mem_integer_iff _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toSignedMeasure_neg : (-j).toSignedMeasure = -j.toSignedMeasure

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ ↑(-j).toSignedMeasure i = ↑(-j.toSignedMeasure) i

Tactic:
rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
  toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
⊢ (-j).toSignedMeasure = -j.toSignedMeasure

Tactic:
ext1 i hi

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ ↑(-j).toSignedMeasure i = ↑(-j.toSignedMeasure) i
-- Mathlib/Data/Set/Image.lean
theorem Surjective.nonempty_preimage (hf : Surjective f) {s : Set β} :
    (f ⁻¹' s).Nonempty ↔ s.Nonempty

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ (f ⁻¹' s).Nonempty ↔ s.Nonempty

Tactic:
rw [← image_nonempty, hf.image_preimage]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem exists_sum_eq_one_iff_pairwise_coprime' [Fintype I] [Nonempty I] [DecidableEq I] :
    (∃ μ : I → R, (∑ i : I, μ i * ∏ j ∈ {i}ᶜ, s j) = 1) ↔ Pairwise (IsCoprime on s)

Proof state:
R : Type u
I : Type v
inst✝³ : CommSemiring R
s : I → R
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ (∃ μ, ∑ i : I, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (IsCoprime on s)

Tactic:
convert exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1

Result:
case h.e'_2.a
R : Type u
I : Type v
inst✝³ : CommSemiring R
s : I → R
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on s) ↔ Pairwise (IsCoprime on fun i => s ↑i)

Proof state:
case h.e'_2.a
R : Type u
I : Type v
inst✝³ : CommSemiring R
s : I → R
inst✝² : Fintype I
inst✝¹ : Nonempty I
inst✝ : DecidableEq I
⊢ Pairwise (IsCoprime on s) ↔ Pairwise (IsCoprime on fun i => s ↑i)

Tactic:
simp only [Function.onFun, pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma reindex_isTotallyUnimodular (A : Matrix m n R) (em : m ≃ m') (en : n ≃ n') :
    (A.reindex em en).IsTotallyUnimodular ↔ A.IsTotallyUnimodular :=
  ⟨fun hA => by simpa [Equiv.symm_apply_eq] using hA.reindex em.symm en.symm,
   fun hA => hA.reindex _ _⟩

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
em : m ≃ m'
en : n ≃ n'
hA : ((reindex em en) A).IsTotallyUnimodular
⊢ A.IsTotallyUnimodular

Tactic:
simpa [Equiv.symm_apply_eq] using hA.reindex em.symm en.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashSet/Lemmas.lean
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : HashSet α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
⊢ k ∈ m.insert k

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem comul_assoc_hom (M : Bimon_ C) :
    M.comul.hom ≫ (M.X.X ◁ M.comul.hom) =
      M.comul.hom ≫ (M.comul.hom ▷ M.X.X) ≫ (α_ M.X.X M.X.X M.X.X).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
⊢ M.comul.hom ≫ M.X.X ◁ M.comul.hom = M.comul.hom ≫ M.comul.hom ▷ M.X.X ≫ (α_ M.X.X M.X.X M.X.X).hom

Tactic:
simpa [- Comon_.comul_assoc] using congr_arg Mon_.Hom.hom M.comul_assoc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem ushiftRightRec_zero (x : BitVec w₁) (y : BitVec w₂) :
    ushiftRightRec x y 0 = x >>> (y &&& twoPow w₂ 0)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.ushiftRightRec y 0 = x >>> (y &&& twoPow w₂ 0)

Tactic:
simp [ushiftRightRec]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma SeminormedGroup.disjoint_nhds (x : E) (f : Filter E) :
    Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ y in f, δ ≤ ‖y / x‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
f : Filter E
⊢ Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y / x‖

Tactic:
simp [NormedCommGroup.nhds_basis_norm_lt x |>.disjoint_iff_left, compl_setOf, eventually_iff]

Result:
no goals