harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem ordConnected_range {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
    OrdConnected (range e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
⊢ (range ⇑e).OrdConnected

Tactic:
simp_rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
⊢ (⇑e '' univ).OrdConnected

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
⊢ (⇑e '' univ).OrdConnected

Tactic:
exact ordConnected_image (e : α ≃o β)

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toReal_le_coe_of_le_coe {a : ℝ≥0∞} {b : ℝ≥0} (h : a ≤ b) : a.toReal ≤ b

Proof state:
case intro
b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ (↑a).toReal ≤ ↑b

Tactic:
simpa using h

Result:
no goals

Proof state:
a : ℝ≥0∞
b : ℝ≥0
h : a ≤ ↑b
⊢ a.toReal ≤ ↑b

Tactic:
lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h

Result:
case intro
b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ (↑a).toReal ≤ ↑b
-- Mathlib/Algebra/MvPolynomial/Comap.lean
theorem comap_rename (f : σ → τ) (x : τ → R) : comap (rename f) x = x ∘ f

Proof state:
case h
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
x✝ : σ
⊢ comap (rename f) x x✝ = (x ∘ f) x✝

Tactic:
simp [rename_X, comap_apply, aeval_X]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
⊢ comap (rename f) x = x ∘ f

Tactic:
funext

Result:
case h
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
x✝ : σ
⊢ comap (rename f) x x✝ = (x ∘ f) x✝
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_mul_gcd_eq_iff_dvd_mul_of_coprime (hcop : Coprime n m) :
    gcd x n * gcd x m = x ↔ x ∣ n * m

Proof state:
case refine_1
x n m : ℕ
hcop : n.Coprime m
h : x.gcd n * x.gcd m = x
⊢ x ∣ n * m

case refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x

Tactic:
refine h ▸ Nat.mul_dvd_mul ?_ ?_ <;> exact x.gcd_dvd_right _

Result:
case refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x

Proof state:
case refine_2
x n m : ℕ
hcop : n.Coprime m
x✝ : x ∣ n * m
⊢ x.gcd n * x.gcd m ∣ x

Tactic:
refine (hcop.gcd_both x x).mul_dvd_of_dvd_of_dvd ?_ ?_ <;> exact x.gcd_dvd_left _

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
theorem MonoidHom.id_grp_comp {G : Type u} [Monoid G] {H : Grp.{u}} (f : G →* H) :
    MonoidHom.comp (Grp.Hom.hom (𝟙 H)) f = f

Proof state:
G : Type u
inst✝ : Monoid G
H : Grp
f : G →* ↑H
⊢ (Grp.Hom.hom (𝟙 H)).comp f = f

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive] lemma IsMulFreimanHom.div {β : Type*} [DivisionCommMonoid β] {B₁ B₂ : Set β}
    {f₁ f₂ : α → β} (h₁ : IsMulFreimanHom n A B₁ f₁) (h₂ : IsMulFreimanHom n A B₂ f₂) :
    IsMulFreimanHom n A (B₁ / B₂) (f₁ / f₂) where
  mapsTo := h₁.mapsTo.div h₂.mapsTo
  map_prod_eq_map_prod s t hsA htA hs ht h

Proof state:
α : Type u_2
inst✝¹ : CommMonoid α
A : Set α
n : ℕ
β : Type u_5
inst✝ : DivisionCommMonoid β
B₁ B₂ : Set β
f₁ f₂ : α → β
h₁ : IsMulFreimanHom n A B₁ f₁
h₂ : IsMulFreimanHom n A B₂ f₂
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h : s.prod = t.prod
⊢ (map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod

Tactic:
rw [Pi.div_def, prod_map_div, prod_map_div, h₁.map_prod_eq_map_prod hsA htA hs ht h,
  h₂.map_prod_eq_map_prod hsA htA hs ht h]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromRows_toRows (A : Matrix (m₁ ⊕ m₂) n R) : fromRows A.toRows₁ A.toRows₂ = A

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
⊢ A.toRows₁.fromRows A.toRows₂ = A

Tactic:
ext (i | i) j <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp]
lemma alternatingMapLinearEquiv_comp_ιMulti (f : M [⋀^Fin n]→ₗ[R] N) :
    (alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n) = f

Proof state:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M [⋀^Fin n]→ₗ[R] N
⊢ (alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n) = f

Tactic:
obtain ⟨φ, rfl⟩ := alternatingMapLinearEquiv.symm.surjective f

Result:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (alternatingMapLinearEquiv (alternatingMapLinearEquiv.symm φ)).compAlternatingMap (ιMulti R n) =
    alternatingMapLinearEquiv.symm φ

Proof state:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ φ.compAlternatingMap (ιMulti R n) = ((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ

Tactic:
rfl

Result:
no goals

Proof state:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯).symm
          (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ)).compAlternatingMap
      (ιMulti R n) =
    ((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ

Tactic:
simp only [LinearEquiv.symm_apply_apply]

Result:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ φ.compAlternatingMap (ιMulti R n) = ((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ

Proof state:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (alternatingMapLinearEquiv (alternatingMapLinearEquiv.symm φ)).compAlternatingMap (ιMulti R n) =
    alternatingMapLinearEquiv.symm φ

Tactic:
dsimp [alternatingMapLinearEquiv]

Result:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯).symm
          (((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ)).compAlternatingMap
      (ιMulti R n) =
    ((⋯.linearMapEquiv.trans presentation.relationsSolutionEquiv).toLinearEquiv ⋯) φ
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem memℓp_infty_iff {f : ∀ i, E i} : Memℓp f ∞ ↔ BddAbove (Set.range fun i => ‖f i‖)

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp f ⊤ ↔ BddAbove (Set.range fun i => ‖f i‖)

Tactic:
simp [Memℓp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_middle {R : α → α → Prop} (s : ∀ {x y}, R x y → R y x) {a : α} {l₁ l₂ : List α} :
    Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂))

Proof state:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
a : α
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)

Tactic:
rw [← append_assoc, pairwise_append, @pairwise_append _ _ ([a] ++ l₁), pairwise_append_comm s]

Result:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
a : α
l₁ l₂ : List α
⊢ (Pairwise (fun {x y} => R x y) ([a] ++ l₁) ∧
      Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ l₁ ++ [a] → ∀ (b : α), b ∈ l₂ → R a_1 b) ↔
    Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ [a] ++ l₁ → ∀ (b : α), b ∈ l₂ → R a_1 b

Proof state:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
a : α
l₁ l₂ : List α
⊢ (Pairwise (fun {x y} => R x y) ([a] ++ l₁) ∧
      Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ l₁ ++ [a] → ∀ (b : α), b ∈ l₂ → R a_1 b) ↔
    Pairwise R ([a] ++ l₁) ∧ Pairwise R l₂ ∧ ∀ (a_1 : α), a_1 ∈ [a] ++ l₁ → ∀ (b : α), b ∈ l₂ → R a_1 b

Tactic:
simp only [mem_append, or_comm]

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
a : α
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ a :: l₂) ↔ Pairwise R (a :: (l₁ ++ l₂))

Tactic:
show Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)

Result:
α : Type u_1
R : α → α → Prop
s : ∀ {x y : α}, R x y → R y x
a : α
l₁ l₂ : List α
⊢ Pairwise R (l₁ ++ ([a] ++ l₂)) ↔ Pairwise R ([a] ++ l₁ ++ l₂)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_mod_left (x z : Nat) : (x + z) % x = z % x

Proof state:
x z : Nat
⊢ (x + z) % x = z % x

Tactic:
rw [Nat.add_comm, add_mod_right]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : A *ᵥ (-v) = - (A *ᵥ v)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ A *ᵥ -v = -(A *ᵥ v)

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ -v) x✝ = (-(A *ᵥ v)) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ -v) x✝ = (-(A *ᵥ v)) x✝

Tactic:
apply dotProduct_neg

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_closure₁ : hausdorffDist (closure s) t = hausdorffDist s t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist (closure s) t = hausdorffDist s t

Tactic:
simp [hausdorffDist]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_fst_zip (l₁ : Array α) (l₂ : Array β) (h : l₁.size ≤ l₂.size) :
    map Prod.fst (zip l₁ l₂) = l₁

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size ≤ { toList := toList✝ }.size
⊢ map Prod.fst ({ toList := toList✝¹ }.zip { toList := toList✝ }) = { toList := toList✝¹ }

Tactic:
simp_all [List.map_fst_zip]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : { toList := toList✝ }.size ≤ l₂.size
⊢ map Prod.fst ({ toList := toList✝ }.zip l₂) = { toList := toList✝ }

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
toList✝¹ : List α
toList✝ : List β
h : { toList := toList✝¹ }.size ≤ { toList := toList✝ }.size
⊢ map Prod.fst ({ toList := toList✝¹ }.zip { toList := toList✝ }) = { toList := toList✝¹ }

Proof state:
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₁.size ≤ l₂.size
⊢ map Prod.fst (l₁.zip l₂) = l₁

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
l₂ : Array β
toList✝ : List α
h : { toList := toList✝ }.size ≤ l₂.size
⊢ map Prod.fst ({ toList := toList✝ }.zip l₂) = { toList := toList✝ }
-- Mathlib/RingTheory/FiniteType.lean
theorem isNoetherianRing (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    [h : Algebra.FiniteType R S] [IsNoetherianRing R] : IsNoetherianRing S

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ IsNoetherianRing S

Tactic:
apply
  isNoetherianRing_of_surjective (MvPolynomial s R) S
    (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom

Result:
case intro.hf
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval Subtype.val).toRingHom

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
obtain ⟨s, hs⟩ := h.1

Result:
case intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ IsNoetherianRing S

Proof state:
case intro.hf
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval Subtype.val).toRingHom

Tactic:
erw [← Set.range_eq_univ, ← AlgHom.coe_range, ←
  Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Finset.setOf_mem, hs]

Result:
case intro.hf
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ

Proof state:
case intro.hf
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/LogDeriv.lean
lemma logDeriv_eq_zero_of_not_differentiableAt (f : 𝕜 → 𝕜') (x : 𝕜) (h : ¬DifferentiableAt 𝕜 f x) :
    logDeriv f x = 0

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
x : 𝕜
h : ¬DifferentiableAt 𝕜 f x
⊢ logDeriv f x = 0

Tactic:
simp only [logDeriv_apply, deriv_zero_of_not_differentiableAt h, zero_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_reverse {l : Array α} {f : (i : Nat) → α → (h : i < l.reverse.size) → β} :
    l.reverse.mapFinIdx f = (l.mapFinIdx (fun i a h => f (l.size - 1 - i) a (by simp; omega))).reverse

Proof state:
α : Type ?u.104478
β : Type ?u.104504
l : Array α
f : (i : Nat) → α → i < l.reverse.size → β
i : Nat
a : α
h : i < l.size
⊢ l.size - 1 - i < l.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.104478
β : Type ?u.104504
l : Array α
f : (i : Nat) → α → i < l.reverse.size → β
i : Nat
a : α
h : i < l.size
⊢ l.size - 1 - i < l.reverse.size

Tactic:
simp

Result:
α : Type ?u.104478
β : Type ?u.104504
l : Array α
f : (i : Nat) → α → i < l.reverse.size → β
i : Nat
a : α
h : i < l.size
⊢ l.size - 1 - i < l.size

Proof state:
case mk
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.reverse.size → β
⊢ { toList := l }.reverse.mapFinIdx f =
    ({ toList := l }.mapFinIdx fun i a h => f ({ toList := l }.size - 1 - i) a ⋯).reverse

Tactic:
simp [List.mapFinIdx_reverse]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.reverse.size → β
⊢ l.reverse.mapFinIdx f = (l.mapFinIdx fun i a h => f (l.size - 1 - i) a ⋯).reverse

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < { toList := l }.reverse.size → β
⊢ { toList := l }.reverse.mapFinIdx f =
    ({ toList := l }.mapFinIdx fun i a h => f ({ toList := l }.size - 1 - i) a ⋯).reverse
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem getElem_toList (n : ℕ) (hn : n < length (toList p x)) :
    (toList p x)[n] = (p ^ n) x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
n : ℕ
hn : n < (p.toList x).length
⊢ (p.toList x)[n] = (p ^ n) x

Tactic:
simp [toList]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_top_right : relfinrank A ⊤ = finrank A E

Proof state:
E : Type v
inst✝ : Field E
A : Subfield E
⊢ A.relfinrank ⊤ = finrank (↥A) E

Tactic:
simp [relfinrank_eq_toNat_relrank, finrank]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma exactAt_of_isLE (n i : ℤ) (hi : n < i) [K.IsLE n] :
    K.ExactAt i :=
  exactAt_of_isSupported K (embeddingUpIntLE n) i
    (by simpa only [not_mem_range_embeddingUpIntLE_iff] using hi)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
n i : ℤ
hi : n < i
inst✝ : K.IsLE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i

Tactic:
simpa only [not_mem_range_embeddingUpIntLE_iff] using hi

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem unitors_inv_equal : (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv

Proof state:
B : Type u
inst✝ : Bicategory B
a : B
⊢ (λ_ (𝟙 a)).inv = (ρ_ (𝟙 a)).inv

Tactic:
simp [Iso.inv_eq_inv]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma isFiniteMeasure {l u : ℝ} (hfl : Tendsto f atBot (𝓝 l)) (hfu : Tendsto f atTop (𝓝 u)) :
    IsFiniteMeasure f.measure := ⟨by simp [f.measure_univ hfl hfu]⟩

Proof state:
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ f.measure univ < ⊤

Tactic:
simp [f.measure_univ hfl hfu]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Unitor.lean
@[reassoc]
lemma mapBifunctorRightUnitor_naturality :
    mapBifunctorMapMap F p φ (𝟙 _) ≫ (mapBifunctorRightUnitor F Y e p hp X').hom =
      (mapBifunctorRightUnitor F Y e p hp X).hom ≫ φ

Proof state:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝² : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
⊢ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) ≫ (mapBifunctorRightUnitor F Y e p hp X').hom =
    (mapBifunctorRightUnitor F Y e p hp X).hom ≫ φ

Tactic:
rw [← cancel_mono (mapBifunctorRightUnitor F Y e p hp X').inv, assoc, assoc, Iso.hom_inv_id,
  comp_id, mapBifunctorRightUnitor_inv_naturality, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem subtypePerm_apply_zpow_of_mem {g : Perm α} {s : Finset α}
    (hs : ∀ x : α, x ∈ s ↔ g x ∈ s) {i : ℤ} {x : α} (hx : x ∈ s) :
    ((g.subtypePerm hs ^ i) (⟨x, hx⟩ : s) : α) = (g ^ i) x

Proof state:
α : Type u_2
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
i : ℤ
x : α
hx : x ∈ s
⊢ ↑((g.subtypePerm hs ^ i) ⟨x, hx⟩) = (g ^ i) x

Tactic:
simp only [subtypePerm_zpow, subtypePerm_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombinationLineMapWeights_apply_right [DecidableEq ι] {i j : ι} (h : i ≠ j) (c : k) :
    affineCombinationLineMapWeights i j c j = c

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c j = c

Tactic:
simp [affineCombinationLineMapWeights, h.symm]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem naturality_2 (α : F ≅ G) (f : X ⟶ Y) : α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ≅ G
f : X ⟶ Y
⊢ α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem DirectedOn.disjoint_sSup_right (h : DirectedOn (· ≤ ·) s) :
    Disjoint a (sSup s) ↔ ∀ ⦃b⦄, b ∈ s → Disjoint a b

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ Disjoint a (sSup s) ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint a b

Tactic:
simp_rw [disjoint_iff, h.inf_sSup_eq, iSup_eq_bot]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem DiscreteTopology.preimage_of_continuous_injective {X Y : Type*} [TopologicalSpace X]
    [TopologicalSpace Y] (s : Set Y) [DiscreteTopology s] {f : X → Y} (hc : Continuous f)
    (hinj : Function.Injective f) : DiscreteTopology (f ⁻¹' s) :=
  DiscreteTopology.of_continuous_injective (β := s) (Continuous.restrict
    (by exact fun _ x ↦ x) hc) ((MapsTo.restrict_inj _).mpr hinj.injOn)

Proof state:
X : Type u_5
Y : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set Y
inst✝ : DiscreteTopology ↑s
f : X → Y
hc : Continuous f
hinj : Injective f
⊢ MapsTo f (f ⁻¹' s) s

Tactic:
exact fun _ x ↦ x

Result:
no goals
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem toEquiv_inclusion_apply {f g : M ≃ₚ[L] N} (h : f ≤ g) (x : f.dom) :
    g.toEquiv (Substructure.inclusion (dom_le_dom h) x) =
      Substructure.inclusion (cod_le_cod h) (f.toEquiv x)

Proof state:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype (g.toEquiv ((inclusion ⋯) x)) = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))

Tactic:
change (subtype _).comp (g.toEquiv.toEmbedding.comp (inclusion _)) x = _

Result:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ (g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))) x = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))

Proof state:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ (g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))) x = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))

Tactic:
rw [subtype_toEquiv_inclusion h]

Result:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding) x = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))

Proof state:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding) x = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.toEquiv ((inclusion ⋯) x) = (inclusion ⋯) (f.toEquiv x)

Tactic:
apply (subtype _).injective

Result:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype (g.toEquiv ((inclusion ⋯) x)) = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))
-- Mathlib/Data/Set/Function.lean
theorem range_restrictPreimage : range (t.restrictPreimage f) = Subtype.val ⁻¹' range f

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ range (t.restrictPreimage f) = Subtype.val ⁻¹' range f

Tactic:
simp only [← image_univ, ← image_restrictPreimage, preimage_univ]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_filter {p : Box ι → Prop} : J ∈ π.filter p ↔ J ∈ π ∧ p J

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ J ∈ π.filter p ↔ J ∈ π ∧ p J

Tactic:
classical
exact Finset.mem_filter

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
p : Box ι → Prop
⊢ J ∈ π.filter p ↔ J ∈ π ∧ p J

Tactic:
exact Finset.mem_filter

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, `𝓝ˢ t` and `𝓝 x` are
disjoint. -/
lemma IsCompact.disjoint_nhdsSet_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X}
    {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
    Disjoint (𝓝ˢ t) (𝓝 x)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ Disjoint (𝓝ˢ t) (𝓝 x)

Tactic:
simpa using SeparatedNhds.disjoint_nhdsSet <| .of_isCompact_isCompact_isClosed H1
  isCompact_singleton isClosed_singleton <| disjoint_singleton_right.mpr H2

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem exists_subset_card_eq (α : Type*) [Infinite α] (n : ℕ) : ∃ s : Finset α, #s = n :=
  ⟨(range n).map (natEmbedding α), by rw [card_map, card_range]⟩

Proof state:
α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ #(map (natEmbedding α) (range n)) = n

Tactic:
rw [card_map, card_range]

Result:
no goals