harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
@[ext]
lemma FirstObj.ext (z₁ z₂ : FirstObj P X) (h : ∀ i, (Pi.π _ i : FirstObj P X ⟶ _) z₁ =
    (Pi.π _ i : FirstObj P X ⟶ _) z₂) : z₁ = z₂

Proof state:
case w.mk
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type
X : I → C
z₁ z₂ : FirstObj P X
h : ∀ (i : I), Pi.π (fun i => P.obj (op (X i))) i z₁ = Pi.π (fun i => P.obj (op (X i))) i z₂
i : I
⊢ limit.π (Discrete.functor fun i => P.obj (op (X i))) { as := i } z₁ =
    limit.π (Discrete.functor fun i => P.obj (op (X i))) { as := i } z₂

Tactic:
exact h i

Result:
no goals

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type
X : I → C
z₁ z₂ : FirstObj P X
h : ∀ (i : I), Pi.π (fun i => P.obj (op (X i))) i z₁ = Pi.π (fun i => P.obj (op (X i))) i z₂
⊢ ∀ (j : Discrete I),
    limit.π (Discrete.functor fun i => P.obj (op (X i))) j z₁ =
      limit.π (Discrete.functor fun i => P.obj (op (X i))) j z₂

Tactic:
rintro ⟨i⟩

Result:
case w.mk
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type
X : I → C
z₁ z₂ : FirstObj P X
h : ∀ (i : I), Pi.π (fun i => P.obj (op (X i))) i z₁ = Pi.π (fun i => P.obj (op (X i))) i z₂
i : I
⊢ limit.π (Discrete.functor fun i => P.obj (op (X i))) { as := i } z₁ =
    limit.π (Discrete.functor fun i => P.obj (op (X i))) { as := i } z₂

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type
X : I → C
z₁ z₂ : FirstObj P X
h : ∀ (i : I), Pi.π (fun i => P.obj (op (X i))) i z₁ = Pi.π (fun i => P.obj (op (X i))) i z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
I : Type
X : I → C
z₁ z₂ : FirstObj P X
h : ∀ (i : I), Pi.π (fun i => P.obj (op (X i))) i z₁ = Pi.π (fun i => P.obj (op (X i))) i z₂
⊢ ∀ (j : Discrete I),
    limit.π (Discrete.functor fun i => P.obj (op (X i))) j z₁ =
      limit.π (Discrete.functor fun i => P.obj (op (X i))) j z₂
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sub_lt_of_lt_add {a b c : Ordinal} (h : a < b + c) (hc : 0 < c) : a - b < c

Proof state:
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
⊢ a - b < c

Tactic:
obtain hab | hba := lt_or_le a b

Result:
case inl
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hab : a < b
⊢ a - b < c

case inr
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
⊢ a - b < c

Proof state:
case inr
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hba : b ≤ a
⊢ a - b < c

Tactic:
rwa [sub_lt_of_le hba]

Result:
no goals

Proof state:
case inl
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hab : a < b
⊢ a - b < c

Tactic:
rwa [Ordinal.sub_eq_zero_iff_le.2 hab.le]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem ucs_bot_one : (⊥ : LieSubmodule R L M).ucs 1 = LieModule.maxTrivSubmodule R L M

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ ucs 1 ⊥ = LieModule.maxTrivSubmodule R L M

Tactic:
simp [LieSubmodule.normalizer_bot_eq_maxTrivSubmodule]

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem zipWith_neLocus_eq_left [DecidableEq N] [Zero M] [DecidableEq P] [Zero P] [Zero N]
    {F : M → N → P} (F0 : F 0 0 = 0) (f : α →₀ M) (g₁ g₂ : α →₀ N)
    (hF : ∀ f, Function.Injective fun g => F f g) :
    (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
⊢ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) = g₁.neLocus g₂

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a✝ ∈ g₁.neLocus g₂

Proof state:
case h
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
a✝ : α
⊢ a✝ ∈ (zipWith F F0 f g₁).neLocus (zipWith F F0 f g₂) ↔ a✝ ∈ g₁.neLocus g₂

Tactic:
simpa only [mem_neLocus] using (hF _).ne_iff

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_of_mul_is_mul (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) {x : R}
    (hx : ∀ y : R, f (x * y) = f x * f y) (y : R) :
    seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ seminormFromBounded' f (x * y) = f x * seminormFromBounded' f y

Tactic:
simp only [seminormFromBounded', mul_assoc, hx, mul_div_assoc,
  Real.mul_iSup_of_nonneg (f_nonneg _)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
rw [seminormFromBounded_of_mul_apply f_nonneg f_mul hx]

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ seminormFromBounded' f (x * y) = f x * seminormFromBounded' f y
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
private lemma one_lt_re_one_add {x : ℝ} (hx : 0 < x) (y : ℝ) :
    1 < (1 + x : ℂ).re ∧ 1 < (1 + x + I * y).re ∧ 1 < (1 + x + 2 * I * y).re

Proof state:
x : ℝ
hx : 0 < x
y : ℝ
⊢ 1 < (1 + ↑x).re ∧ 1 < (1 + ↑x + I * ↑y).re ∧ 1 < (1 + ↑x + 2 * I * ↑y).re

Tactic:
simp only [add_re, one_re, ofReal_re, lt_add_iff_pos_right, hx, mul_re, I_re, zero_mul, I_im,
  ofReal_im, mul_zero, sub_self, add_zero, re_ofNat, im_ofNat, mul_one, mul_im, and_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
theorem Real.tsum_exp_neg_mul_int_sq {a : ℝ} (ha : 0 < a) :
    (∑' n : ℤ, exp (-π * a * (n : ℝ) ^ 2)) =
      (1 : ℝ) / a ^ (1 / 2 : ℝ) * (∑' n : ℤ, exp (-π / a * (n : ℝ) ^ 2))

Proof state:
a : ℝ
ha : 0 < a
⊢ ∑' (n : ℤ), rexp (-π * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), rexp (-π / a * ↑n ^ 2)

Tactic:
simpa only [← ofReal_inj, ofReal_tsum, ofReal_exp, ofReal_mul, ofReal_neg, ofReal_pow,
  ofReal_intCast, ofReal_div, ofReal_one, ofReal_cpow ha.le, ofReal_ofNat, mul_zero, zero_mul,
  add_zero] using Complex.tsum_exp_neg_quadratic (by rwa [ofReal_re] : 0 < (a : ℂ).re) 0

Result:
no goals

Proof state:
a : ℝ
ha : 0 < a
⊢ 0 < (↑a).re

Tactic:
rwa [ofReal_re]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_isSome_iff {f : Fin n → Option α} :
    (findSome? f).isSome ↔ ∃ i, (f i).isSome

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
i : Fin n
x : α
hix : f i = some x
h : findSome? f = none
⊢ ∃ a, none = some a

Tactic:
rw [eq_none_of_findSome?_eq_none h i] at hix

Result:
n : Nat
α : Type u_1
f : Fin n → Option α
i : Fin n
x : α
hix : none = some x
h : findSome? f = none
⊢ ∃ a, none = some a

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
x : α
hx : findSome? f = some x
i : Fin n
hi : f i = some x
⊢ ∃ i a, f i = some a

Tactic:
exists i, x

Result:
no goals

Proof state:
case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
i : Fin n
x : α
hix : f i = some x
⊢ ∃ a, findSome? f = some a

Tactic:
match h : findSome? f with
| some x => exists x
| none => rw [eq_none_of_findSome?_eq_none h i] at hix; contradiction

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
i : Fin n
x : α
hix : none = some x
h : findSome? f = none
⊢ ∃ a, none = some a

Tactic:
contradiction

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
i : Fin n
x✝ : α
hix : f i = some x✝
x : α
h : findSome? f = some x
⊢ ∃ a, some x = some a

Tactic:
exists x

Result:
no goals

Proof state:
case mp
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∃ a, findSome? f = some a) → ∃ i a, f i = some a

Tactic:
intro ⟨x, hx⟩

Result:
case mp
n : Nat
α : Type u_1
f : Fin n → Option α
x : α
hx : findSome? f = some x
⊢ ∃ i a, f i = some a

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (findSome? f).isSome = true ↔ ∃ i, (f i).isSome = true

Tactic:
simp only [Option.isSome_iff_exists]

Result:
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∃ a, findSome? f = some a) ↔ ∃ i a, f i = some a

Proof state:
case mp
n : Nat
α : Type u_1
f : Fin n → Option α
x : α
hx : findSome? f = some x
⊢ ∃ i a, f i = some a

Tactic:
match exists_of_findSome?_eq_some hx with
| ⟨i, hi⟩ => exists i, x

Result:
no goals

Proof state:
case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∃ i a, f i = some a) → ∃ a, findSome? f = some a

Tactic:
intro ⟨i, x, hix⟩

Result:
case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
i : Fin n
x : α
hix : f i = some x
⊢ ∃ a, findSome? f = some a

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∃ a, findSome? f = some a) ↔ ∃ i a, f i = some a

Tactic:
constructor

Result:
case mp
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∃ a, findSome? f = some a) → ∃ i a, f i = some a

case mpr
n : Nat
α : Type u_1
f : Fin n → Option α
⊢ (∃ i a, f i = some a) → ∃ a, findSome? f = some a
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_mul_comm (f g : M →ₗ[R] M) : trace R M (f * g) = trace R M (g * f)

Proof state:
case neg
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ ((toMatrix b b) f * (toMatrix b b) g).trace = ((toMatrix b b) g * (toMatrix b b) f).trace

Tactic:
apply Matrix.trace_mul_comm

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)

Result:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

case neg
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Proof state:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
let ⟨s, ⟨b⟩⟩ := H

Result:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Proof state:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]

Result:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ ((toMatrix b b) f * (toMatrix b b) g).trace = ((toMatrix b b) g * (toMatrix b b) f).trace
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/EraseIdx.lean
theorem mem_eraseIdx_iff_get? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l.get? i = x

Proof state:
α : Type u
x : α
l : List α
k : Nat
⊢ x ∈ l.eraseIdx k ↔ ∃ i, i ≠ k ∧ l.get? i = some x

Tactic:
simp [mem_eraseIdx_iff_getElem?]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_set_eq (a : α) (n) (l : List α) : (set l n a).get? n = (fun _ => a) <$> l.get? n

Proof state:
α : Type u_1
a : α
n : Nat
l : List α
⊢ Option.map (Function.const α a) l[n]? = Option.map (fun x => a) l[n]?

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a : α
n : Nat
l : List α
⊢ (l.set n a).get? n = (fun x => a) <$> l.get? n

Tactic:
simp only [get?_eq_getElem?, getElem?_set_self', Option.map_eq_map]

Result:
α : Type u_1
a : α
n : Nat
l : List α
⊢ Option.map (Function.const α a) l[n]? = Option.map (fun x => a) l[n]?
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem inf_eq {u₁ u₂ : UniformSpace γ} :
    𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂)

Proof state:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ 𝔖 = ⨅ b, bif b then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖

Tactic:
refine iInf_congr fun i => ?_

Result:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖

Proof state:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖

Tactic:
cases i <;> rfl

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ uniformSpace α γ 𝔖

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, UniformOnFun.iInf_eq]

Result:
α : Type u_1
γ : Type u_3
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ 𝔖 = ⨅ b, bif b then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_inf {u v : ℕ → ℝ≥0∞} :
    expGrowthInf (u ⊓ v) = expGrowthInf u ⊓ expGrowthInf v

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthInf (u ⊓ v) = expGrowthInf u ⊓ expGrowthInf v

Tactic:
rw [expGrowthInf, expGrowthInf, expGrowthInf, ← liminf_min]

Result:
u v : ℕ → ℝ≥0∞
⊢ liminf (fun n => ((u ⊓ v) n).log / ↑n) atTop = liminf (fun a => (u a).log / ↑a ⊓ (v a).log / ↑a) atTop

Proof state:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊓ v) n).log / ↑n = (u n).log / ↑n ⊓ (v n).log / ↑n

Tactic:
rw [Pi.inf_apply, log_monotone.map_min]

Result:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u n).log ⊓ (v n).log) / ↑n = (u n).log / ↑n ⊓ (v n).log / ↑n

Proof state:
u v : ℕ → ℝ≥0∞
⊢ liminf (fun n => ((u ⊓ v) n).log / ↑n) atTop = liminf (fun a => (u a).log / ↑a ⊓ (v a).log / ↑a) atTop

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Result:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊓ v) n).log / ↑n = (u n).log / ↑n ⊓ (v n).log / ↑n

Proof state:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u n).log ⊓ (v n).log) / ↑n = (u n).log / ↑n ⊓ (v n).log / ↑n

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_min

Result:
no goals
-- Mathlib/Data/PNat/Interval.lean
theorem card_Icc : #(Icc a b) = b + 1 - a

Proof state:
a b : ℕ+
⊢ #(Icc a b) = ↑b + 1 - ↑a

Tactic:
rw [← Nat.card_Icc, ← map_subtype_embedding_Icc, card_map]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne [T1Space X] {b : Set (Set X)}
    (hb : IsTopologicalBasis b) {x y : X} (h : x ≠ y) : ∃ a ∈ b, x ∈ a ∧ y ∉ a

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
a : Set X
ab : a ∈ b
xa : x ∈ a
ha : a ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a

Tactic:
exact ⟨a, ab, xa, fun h => ha h rfl⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a

Tactic:
rcases hb.isOpen_iff.1 isOpen_ne x h with ⟨a, ab, xa, ha⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
a : Set X
ab : a ∈ b
xa : x ∈ a
ha : a ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_counitInv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
    (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
    f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔
    f ≫ g ≫ h = f' ≫ g' ≫ h'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
W X X' Y Y' Z : D
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
simp only [← Category.assoc, cancel_mono]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
    testBit (Bool.toNat b) i = (decide (i = 0) && b)

Proof state:
b : Bool
i : Nat
⊢ b.toNat.testBit i = (decide (i = 0) && b)

Tactic:
cases b <;> cases i <;>
simp [testBit_to_div_mod, Nat.pow_succ, Nat.mul_comm _ 2,
      ←Nat.div_div_eq_div_mul _ 2, one_div_two,
      Nat.mod_eq_of_lt]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem ThreeGPFree.image' [FunLike F α β] [MulHomClass F α β] (f : F) (hf : (s * s).InjOn f)
    (h : ThreeGPFree s) : ThreeGPFree (f '' s)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f (a * c) = f (b * b)

Tactic:
rwa [map_mul, map_mul]

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
⊢ ThreeGPFree (⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ habc

Result:
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f a = f b

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f a = f b

Tactic:
rw [h ha hb hc (hf (mul_mem_mul ha hc) (mul_mem_mul hb hb) <| by rwa [map_mul, map_mul])]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem nat_omega_rec (f : α → β → σ) {m : α → β → ℕ}
    {l : α → β → List β} {g : α → β × List σ → Option σ}
    (hm : Primrec₂ m) (hl : Primrec₂ l) (hg : Primrec₂ g)
    (Ord : ∀ a b, ∀ b' ∈ l a b, m a b' < m a b)
    (H : ∀ a b, g a (b, (l a b).map (f a)) = some (f a b)) : Primrec₂ f :=
  Primrec₂.uncurry.mp <|
    nat_omega_rec' (Function.uncurry f)
      (Primrec₂.uncurry.mpr hm)
      (list_map (hl.comp fst snd) (Primrec₂.pair.comp₂ (fst.comp₂ .left) .right))
      (hg.comp₂ (fst.comp₂ .left) (Primrec₂.pair.comp₂ (snd.comp₂ .left) .right))
      (by simpa using Ord) (by simpa [Function.comp] using H)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
m : α → β → ℕ
l : α → β → List β
g : α → β × List σ → Option σ
hm : Primrec₂ m
hl : Primrec₂ l
hg : Primrec₂ g
Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b
H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)
⊢ ∀ (b : α × β), g b.1 (b.2, List.map (uncurry f) (List.map (fun b_1 => (b.1, b_1)) (l b.1 b.2))) = some (uncurry f b)

Tactic:
simpa [Function.comp] using H

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
m : α → β → ℕ
l : α → β → List β
g : α → β × List σ → Option σ
hm : Primrec₂ m
hl : Primrec₂ l
hg : Primrec₂ g
Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b
H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)
⊢ ∀ (b b' : α × β), b' ∈ List.map (fun b_1 => (b.1, b_1)) (l b.1 b.2) → uncurry m b' < uncurry m b

Tactic:
simpa using Ord

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred/WithBot.lean
lemma succ_natCast (n : ℕ) : succ (n : WithBot α) = n + 1

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
n : ℕ
⊢ (↑n).succ = ↑n + 1

Tactic:
rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]

Result:
no goals
-- Mathlib/Data/NNRat/Floor.lean
theorem intFloor_cast (x : ℚ≥0) : ⌊(x : K)⌋ = ⌊(x : ℚ)⌋

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑(⌊x⌋₊ + 1)

Tactic:
norm_cast

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑⌊x⌋₊ ≤ x ∧ x < ↑(⌊x⌋₊ + 1)

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑⌊x⌋₊ ≤ x ∧ x < ↑(⌊x⌋₊ + 1)

Tactic:
rw [Nat.cast_add_one, ← Nat.floor_eq_iff (zero_le _)]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌊↑x⌋ = ⌊↑x⌋

Tactic:
rw [Int.floor_eq_iff (α := K), ← coe_floor]

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑↑⌊x⌋₊ + 1

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑↑⌊x⌋₊ + 1

Tactic:
norm_cast

Result:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑⌊x⌋₊ ≤ ↑x ∧ ↑x < ↑(⌊x⌋₊ + 1)
-- Mathlib/Algebra/Homology/ShortComplex/Ab.lean
lemma ShortExact.ab_exact_iff_function_exact :
    S.Exact ↔ Function.Exact S.f S.g

Proof state:
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom S.g).ker = (ConcreteCategory.hom S.f).range

Tactic:
tauto

Result:
no goals

Proof state:
S : ShortComplex Ab
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
rw [ab_exact_iff_range_eq_ker, AddMonoidHom.exact_iff]

Result:
S : ShortComplex Ab
⊢ (AddCommGrp.Hom.hom S.f).range = (AddCommGrp.Hom.hom S.g).ker ↔
    (ConcreteCategory.hom S.g).ker = (ConcreteCategory.hom S.f).range
-- Mathlib/Data/ZMod/Basic.lean
lemma isUnit_iff_coprime (m n : ℕ) : IsUnit (m : ZMod n) ↔ m.Coprime n

Proof state:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n

Tactic:
rw [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm, ← H']

Result:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n

Proof state:
m n : ℕ
⊢ IsUnit ↑m ↔ m.Coprime n

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ (unitOfCoprime m H).isUnit⟩

Result:
m n : ℕ
H : IsUnit ↑m
⊢ m.Coprime n

Proof state:
m n : ℕ
H : IsUnit ↑m
H' : (↑H.unit).val.Coprime n
⊢ m.Coprime n

Tactic:
rw [IsUnit.unit_spec, val_natCast m, Nat.coprime_iff_gcd_eq_one] at H'

Result:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ m.Coprime n

Proof state:
m n : ℕ
H : IsUnit ↑m
⊢ m.Coprime n

Tactic:
have H' := val_coe_unit_coprime H.unit

Result:
m n : ℕ
H : IsUnit ↑m
H' : (↑H.unit).val.Coprime n
⊢ m.Coprime n

Proof state:
m n : ℕ
H : IsUnit ↑m
H' : (m % n).gcd n = 1
⊢ n.gcd m = (m % n).gcd n

Tactic:
exact Nat.gcd_rec n m

Result:
no goals