harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem equiv_between_cg (M_cg : Structure.CG L M) (N_cg : Structure.CG L N)
    (g : L.FGEquiv M N)
    (ext_dom : L.IsExtensionPair M N)
    (ext_cod : L.IsExtensionPair N M) :
    ∃ f : M ≃[L] N, g ≤ f.toEmbedding.toPartialEquiv

Proof state:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
⊢ ∃ f, ↑g ≤ f.toEmbedding.toPartialEquiv

Tactic:
refine ⟨toEquivOfEqTop dom_top cod_top, ?_⟩

Result:
case mk.intro.intro.mk.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝⁵ : Countable ↑X
x✝⁴ : Encodable ↑X
x✝³ : Countable ↑Y
x✝² : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p => Sum.recOn p (fun x => ext_dom.definedAtLeft ↑x) fun y => ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝¹ : X ⊆ ↑F.dom
x✝ : Y ⊆ ↑F.cod
dom_top : F.dom = ⊤
cod_top : F.cod = ⊤
⊢ ↑g ≤ (toEquivOfEqTop dom_top cod_top).toEmbedding.toPartialEquiv
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Array α} :
    l₁ < l₂ ↔
      (l₁ = l₂.take l₁.size ∧ l₁.size < l₂.size) ∨
        (∃ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size),
          (∀ j, (hj : j < i) →
            l₁[j]'(Nat.lt_trans hj h₁) = l₂[j]'(Nat.lt_trans hj h₂)) ∧ l₁[i] < l₂[i])

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : Array α
⊢ l₁ < l₂ ↔
    l₁ = l₂.take l₁.size ∧ l₁.size < l₂.size ∨ ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Array α
toList✝ : List α
⊢ { toList := toList✝ } < l₂ ↔
    { toList := toList✝ } = l₂.take { toList := toList✝ }.size ∧ { toList := toList✝ }.size < l₂.size ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), { toList := toList✝ }[j] = l₂[j]) ∧ { toList := toList✝ }[i] < l₂[i]

Proof state:
case mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } < { toList := toList✝ } ↔
    { toList := toList✝¹ } = { toList := toList✝ }.take { toList := toList✝¹ }.size ∧
        { toList := toList✝¹ }.size < { toList := toList✝ }.size ∨
      ∃ i h₁ h₂,
        (∀ (j : Nat) (hj : j < i), { toList := toList✝¹ }[j] = { toList := toList✝ }[j]) ∧
          { toList := toList✝¹ }[i] < { toList := toList✝ }[i]

Tactic:
simp [List.lt_iff_exists]

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Array α
toList✝ : List α
⊢ { toList := toList✝ } < l₂ ↔
    { toList := toList✝ } = l₂.take { toList := toList✝ }.size ∧ { toList := toList✝ }.size < l₂.size ∨
      ∃ i h₁ h₂, (∀ (j : Nat) (hj : j < i), { toList := toList✝ }[j] = l₂[j]) ∧ { toList := toList✝ }[i] < l₂[i]

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } < { toList := toList✝ } ↔
    { toList := toList✝¹ } = { toList := toList✝ }.take { toList := toList✝¹ }.size ∧
        { toList := toList✝¹ }.size < { toList := toList✝ }.size ∨
      ∃ i h₁ h₂,
        (∀ (j : Nat) (hj : j < i), { toList := toList✝¹ }[j] = { toList := toList✝ }[j]) ∧
          { toList := toList✝¹ }[i] < { toList := toList✝ }[i]
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_dite {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : ∀ x : α, p x → β)
    (g : ∀ x : α, ¬p x → β) :
    ∏ x ∈ s, (if hx : p x then f x hx else g x hx) =
      (∏ x : {x ∈ s | p x}, f x.1 (by simpa using (mem_filter.mp x.2).2)) *
        ∏ x : {x ∈ s | ¬p x}, g x.1 (by simpa using (mem_filter.mp x.2).2)

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
x : { x // x ∈ filter (fun x => p x) s }
⊢ p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
⊢ (∏ x ∈ s, if hx : p x then f x hx else g x hx) =
    (∏ x : { x // x ∈ filter (fun x => p x) s }, f ↑x ⋯) * ∏ x : { x // x ∈ filter (fun x => ¬p x) s }, g ↑x ⋯

Tactic:
simp [prod_apply_dite _ _ fun x => x]

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
p : α → Prop
hp : DecidablePred p
f : (x : α) → p x → β
g : (x : α) → ¬p x → β
x : { x // x ∈ filter (fun x => ¬p x) s }
⊢ ¬p ↑x

Tactic:
simpa using (mem_filter.mp x.2).2

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem embDomain_apply (f : α ↪ β) (v : α →₀ M) (a : α) : embDomain f v (f a) = v a

Proof state:
case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∉ v.support
⊢ 0 = v a

Tactic:
exact (not_mem_support_iff.1 h).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ (if h : f a ∈ map f v.support then v (choose (fun a₁ => f a₁ = f a) v.support ⋯) else 0) = v a

Tactic:
split_ifs with h <;> rw [Finset.mem_map' f] at h

Result:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
h✝ : f a ∈ map f v.support
h : a ∈ v.support
⊢ v (choose (fun a₁ => f a₁ = f a) v.support ⋯) = v a

case neg
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
h : a ∉ v.support
⊢ 0 = v a

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ (embDomain f v) (f a) = v a

Tactic:
change dite _ _ _ = _

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
⊢ (if h : f a ∈ map f v.support then v (choose (fun a₁ => f a₁ = f a) v.support ⋯) else 0) = v a

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
h✝ : f a ∈ map f v.support
h : a ∈ v.support
⊢ f.toFun (choose (fun a₁ => f a₁ = f a) v.support ⋯) = f.toFun a

Tactic:
exact Finset.choose_property (fun a₁ => f a₁ = f a) _ _

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
h✝ : f a ∈ map f v.support
h : a ∈ v.support
⊢ v (choose (fun a₁ => f a₁ = f a) v.support ⋯) = v a

Tactic:
refine congr_arg (v : α → M) (f.inj' ?_)

Result:
case pos
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ↪ β
v : α →₀ M
a : α
h✝ : f a ∈ map f v.support
h : a ∈ v.support
⊢ f.toFun (choose (fun a₁ => f a₁ = f a) v.support ⋯) = f.toFun a
-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_hasDerivAt_of_isBigO_rpow [NormedSpace ℂ E] {a b : ℝ}
    {f : ℝ → E} {s : ℂ} (hfc : LocallyIntegrableOn f (Ioi 0)) (hf_top : f =O[atTop] (· ^ (-a)))
    (hs_top : s.re < a) (hf_bot : f =O[𝓝[>] 0] (· ^ (-b))) (hs_bot : b < s.re) :
    MellinConvergent (fun t => log t • f t) s ∧
      HasDerivAt (mellin f) (mellin (fun t => log t • f t) s) s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
⊢ ‖F' z t‖ ≤ bound t

Tactic:
simp_rw [F', bound, norm_smul, norm_mul, norm_real, mul_assoc]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x => x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x => x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t => ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t => (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t => (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
⊢ ‖↑t ^ (z - 1)‖ * (‖log t‖ * ‖f t‖) ≤ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * (|log t| * ‖f t‖)
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem dist_integralSum_integral_le_of_memBaseSet (h : Integrable I l f vol) (h₀ : 0 < ε)
    (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) (hπp : π.IsPartition) :
    dist (integralSum f vol π) (integral I l f vol) ≤ ε

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (⋯.choose c) π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε

Tactic:
exact (hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.2 c _ hπ hπp

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (h.convergenceR ε c) π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε

Tactic:
rw [convergenceR, dif_pos h₀] at hπ

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ≥0
ε : ℝ
h : Integrable I l f vol
h₀ : 0 < ε
hπ : l.MemBaseSet I c (⋯.choose c) π
hπp : π.IsPartition
⊢ dist (integralSum f vol π) (integral I l f vol) ≤ ε
-- Mathlib/LinearAlgebra/Charpoly/Basic.lean
theorem minpoly_coeff_zero_of_injective [Nontrivial R] (hf : Function.Injective f) :
    (minpoly R f).coeff 0 ≠ 0

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h✝ : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = 0
h : P = 0
⊢ False

Tactic:
exact minpoly.ne_zero (isIntegral f) hP

Result:
no goals

Proof state:
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < (minpoly R f).degree
hPmonic : P.Monic
hzero : (aeval f) (minpoly R f) = 0
⊢ False

Tactic:
simp only [hP, mul_eq_comp, LinearMap.ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp,
  _root_.map_mul, zero_apply, Function.comp_apply] at hzero

Result:
case intro
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Free R M
inst✝¹ : Module.Finite R M
f : M →ₗ[R] M
inst✝ : Nontrivial R
hf : Function.Injective ⇑f
h : (minpoly R f).coeff 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < (minpoly R f).degree
hPmonic : P.Monic
hzero : ∀ (x : M), ((aeval f) P) x = 0
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem foldRev_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
    l.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc = toListModel l.buckets ++ acc

Proof state:
α : Type u
β : α → Type v
l : Raw α β
acc : List ((a : α) × β a)
⊢ Raw.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc l = toListModel l.buckets ++ acc

Tactic:
simp [foldRev_cons_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Equidecomp.lean
theorem toPartialEquiv_injective : Injective <| toPartialEquiv (X := X) (G := G)

Proof state:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
⊢ Injective toPartialEquiv

Tactic:
intro ⟨_, _, _⟩ _ _

Result:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
toPartialEquiv✝ : PartialEquiv X X
w✝ : Finset G
h✝ : IsDecompOn (↑toPartialEquiv✝) toPartialEquiv✝.source w✝
a₂✝ : Equidecomp X G
a✝ : { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ }.toPartialEquiv = a₂✝.toPartialEquiv
⊢ { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ } = a₂✝

Proof state:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
toPartialEquiv✝ : PartialEquiv X X
w✝ : Finset G
h✝ : IsDecompOn (↑toPartialEquiv✝) toPartialEquiv✝.source w✝
a₂✝ : Equidecomp X G
a✝ : { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ }.toPartialEquiv = a₂✝.toPartialEquiv
⊢ { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ } = a₂✝

Tactic:
congr

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem exists_chain_of_relationReflTransGen (h : Relation.ReflTransGen r a b) :
    ∃ l, Chain r a l ∧ getLast (a :: l) (cons_ne_nil _ _) = b

Proof state:
case refine_2.intro.intro
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : (d :: l).getLast ⋯ = b
⊢ ∃ l, Chain r c l ∧ (c :: l).getLast ⋯ = b

Tactic:
refine ⟨d :: l, Chain.cons e hl₁, ?_⟩

Result:
case refine_2.intro.intro
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : (d :: l).getLast ⋯ = b
⊢ (c :: d :: l).getLast ⋯ = b

Proof state:
case refine_2
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
ih : ∃ l, Chain r d l ∧ (d :: l).getLast ⋯ = b
⊢ ∃ l, Chain r c l ∧ (c :: l).getLast ⋯ = b

Tactic:
obtain ⟨l, hl₁, hl₂⟩ := ih

Result:
case refine_2.intro.intro
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : (d :: l).getLast ⋯ = b
⊢ ∃ l, Chain r c l ∧ (c :: l).getLast ⋯ = b

Proof state:
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r a l ∧ (a :: l).getLast ⋯ = b

Tactic:
refine Relation.ReflTransGen.head_induction_on h ?_ ?_

Result:
case refine_1
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r b l ∧ (b :: l).getLast ⋯ = b

case refine_2
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, Chain r c l ∧ (c :: l).getLast ⋯ = b) → ∃ l, Chain r a l ∧ (a :: l).getLast ⋯ = b

Proof state:
case refine_1
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∃ l, Chain r b l ∧ (b :: l).getLast ⋯ = b

Tactic:
exact ⟨[], Chain.nil, rfl⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
l : List α
hl₁ : Chain r d l
hl₂ : (d :: l).getLast ⋯ = b
⊢ (c :: d :: l).getLast ⋯ = b

Tactic:
rwa [getLast_cons_cons]

Result:
no goals

Proof state:
case refine_2
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, Chain r c l ∧ (c :: l).getLast ⋯ = b) → ∃ l, Chain r a l ∧ (a :: l).getLast ⋯ = b

Tactic:
intro c d e _ ih

Result:
case refine_2
α : Type u
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
c d : α
e : r c d
h✝ : Relation.ReflTransGen r d b
ih : ∃ l, Chain r d l ∧ (d :: l).getLast ⋯ = b
⊢ ∃ l, Chain r c l ∧ (c :: l).getLast ⋯ = b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_mapₘ {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
    Perm (toListModel (m.mapₘ f).1.buckets)
      ((toListModel m.1.buckets).map fun p => ⟨p.1, f p.1 p.2⟩) :=
  toListModel_updateAllBuckets AssocList.toList_map (by simp)

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → δ a
⊢ ∀ {l l' : List ((a : α) × β a)},
    List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (l ++ l') ~
      List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l ++ List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l'

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/PerfectClosure.lean
theorem natCast_eq_iff (x y : ℕ) : (x : PerfectClosure K p) = y ↔ (x : K) = y

Proof state:
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
⊢ ↑x = ↑y ↔ ↑x = ↑y

Tactic:
constructor <;> intro H

Result:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

Proof state:
case mpr
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

Tactic:
rw [natCast K p 0, natCast K p 0, H]

Result:
no goals

Proof state:
case mp.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y

Tactic:
simpa only [zero_add, iterate_fixed (frobenius_natCast K p _)] using H

Result:
no goals

Proof state:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ∃ z, (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y

Tactic:
obtain ⟨z, H⟩ := H

Result:
case mp.intro
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y z : ℕ
H : (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y

Proof state:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ↑x = ↑y
⊢ ↑x = ↑y

Tactic:
rw [natCast K p 0, natCast K p 0, mk_eq_iff] at H

Result:
case mp
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x y : ℕ
H : ∃ z, (⇑(frobenius K p))^[(0, ↑y).1 + z] (0, ↑x).2 = (⇑(frobenius K p))^[(0, ↑x).1 + z] (0, ↑y).2
⊢ ↑x = ↑y
-- Mathlib/Analysis/Calculus/Deriv/Star.lean
theorem derivWithin.star :
    derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)

Proof state:
case inr
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
s : Set 𝕜
x : 𝕜
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)

case inr
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
s : Set 𝕜
x : 𝕜
hxs : nhdsWithin x (s \ {x}) = ⊥
⊢ derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)

Proof state:
case inl
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
s : Set 𝕜
x : 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)

Tactic:
exact DFunLike.congr_fun (fderivWithin_star hxs) _

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma dual_eq_mul_inv :
    dual A K I = dual A K 1 * I⁻¹

Proof state:
case neg.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ dual A K I ≤ dual A K 1 * I⁻¹

Tactic:
suffices dual A K I * I ≤ dual A K 1 by
  convert mul_right_mono I⁻¹ this using 1; simp only [mul_inv_cancel₀ hI, mul_one, mul_assoc]

Result:
case neg.a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
⊢ dual A K I * I ≤ dual A K 1

Proof state:
case h.e'_3
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : ¬I = 0
this : dual A K I * I ≤ dual A K 1
⊢ dual A K I = (fun J => J * I⁻¹) (dual A K I * I)

Tactic:
simp only [mul_inv_cancel₀ hI, mul_one, mul_assoc]

Result:
no goals